Re: "functional" programming in Ada

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

On 08/03/2018 23:49, G. B. wrote:
> Dmitry A. Kazakov <mailbox@dmitry-kazakov.de> wrote:
>> On 08/03/2018 04:34, Randy Brukardt wrote:
>>> The various contracts (preconditions, postconditions, predicates, etc.) all
>>> contain some executable code, and it is necessary for callers to be able to
>>> understand those contracts. Expression functions help in this, while the
>>> bulk of the implementation should remain in the body.
>>
>> These are not contracts if have any executable code, and more
>> importantly, understanding cannot be achieved by exposing
>> implementation/code.
>>
>> P.S. Contracts exist prior the program (programs, actuall) and surely
>> prior to any execution of (any implementation of any programs under the
>> contract).
>>
> 
> If there is nothing that ever assigns a value to a contract’s
> clause, then there id none. So, in order make it something,
> an evaluation of clauses needs to be performed. Somewhere,
> somehow. My brain is operating when doing this, or so I hope,
> and whenever it does following discipline, then it is executing
> a program.
> 
> The troublesome idea is to think that the program
> and its contract are like “x ε x”, or like recursive types.

Yes, unless the types algebra is clearly separated from the language 
enough for the recursion to start and end before it comes to any use of 
the type.

Anyway, since type contracts are most important ones, it is difficult to 
accept recursive definitions of types (as well as pattern matched types 
or templates beyond trivial) because they make it for the reader to 
understand the meaning of the contract.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de