From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00
	autolearn=unavailable autolearn_force=no version=3.4.4
Path: 
 eternal-september.org!reader01.eternal-september.org!.POSTED!not-for-mail
From: Paul Rubin <no.email@nospam.invalid>
Newsgroups: comp.lang.ada
Subject: Re: Implicit actions & program correctness
Date: Tue, 26 May 2020 02:55:14 -0700
Organization: A noiseless patient Spider
Message-ID: <87pnar9g1p.fsf@nightsong.com>
References: <d4cc5c66-b82a-4ef7-8e69-2fa9b7bd99a6@googlegroups.com>
	<r9mp29$6nd$1@dont-email.me>
	<3c545096-d000-4d09-b3fe-ad8530632457@googlegroups.com>
	<871rnk97ew.fsf@nightsong.com>
	<14afb70d-cb70-4ca2-bd24-f9d9664ee103@googlegroups.com>
	<87o8qb7ikc.fsf@nightsong.com> <hj43d9F2cl7U1@mid.individual.net>
Mime-Version: 1.0
Content-Type: text/plain
Injection-Info: reader02.eternal-september.org;
 posting-host="72b8d7bf960c0199ae80654d23ca070b";
	logging-data="30957"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX1/LDe0kYZ9FJJUb3oWWgOJd"
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/26.1 (gnu/linux)
Cancel-Lock: sha1:ky7016PTztd+z1RtE9eqdqd5gyM=
	sha1:gzTJjsIzZB+zi48y5zV7Kj6DRlk=
Xref: reader01.eternal-september.org comp.lang.ada:58791
Date: 2020-05-26T02:55:14-07:00
List-Id: <comp.lang.ada>

Niklas Holsti <niklas.holsti@tidorum.invalid> writes:
>> and return three maybe-empty wrapper objects containing the new state.
> That, of course, is basically a run-time check

I thought about it a little bit more and got rid of the wrappers, which
were ugly.  I'll post some Haskell code illustrating the idea if anyone
wants to see it.  But, even with the wrappers, it is a compile time
check in the sense that you have to extract the suitably typed board
state from the wrapper, before you can call the API function that
requires an arg of that type.  Thus, there is a compile time guarantee
that you can't call the API function with an illegal state.  That is
all that was asked for.