comp.lang.ada
 help / color / mirror / Atom feed
* "functional" programming in Ada
@ 2018-03-06 11:34 Alejandro R. Mosteo
  2018-03-06 13:09 ` Dmitry A. Kazakov
                   ` (4 more replies)
  0 siblings, 5 replies; 39+ messages in thread
From: Alejandro R. Mosteo @ 2018-03-06 11:34 UTC (permalink / raw)


In a recent project I've started using in full if/case expressions and 
expression functions... and I'm a bit scared at the amount of use I have 
for them. I'm using these constantly.

Pros: purely recursive functions are really fun to write. If/case 
expressions, used sparingly, do help a lot in having constant 
declarations in local scopes. I'm writing more code in declarative parts.

Cons: the temptation of writing function bodies in the spec is too big. 
At least I try to keep them in the private part, but I've found myself 
trying to force an expression function just to avoid a package body.

Care to share your experiences?

Álex.


^ permalink raw reply	[flat|nested] 39+ messages in thread

* Re: "functional" programming in Ada
  2018-03-06 11:34 "functional" programming in Ada Alejandro R. Mosteo
@ 2018-03-06 13:09 ` Dmitry A. Kazakov
  2018-03-06 14:35   ` Alejandro R. Mosteo
  2018-03-06 13:29 ` Mehdi Saada
                   ` (3 subsequent siblings)
  4 siblings, 1 reply; 39+ messages in thread
From: Dmitry A. Kazakov @ 2018-03-06 13:09 UTC (permalink / raw)


On 06/03/2018 12:34, Alejandro R. Mosteo wrote:
> In a recent project I've started using in full if/case expressions and 
> expression functions... and I'm a bit scared at the amount of use I have 
> for them. I'm using these constantly.

That is how wrong ideas become most popular ones.

> Pros: purely recursive functions are really fun to write. If/case 
> expressions, used sparingly, do help a lot in having constant 
> declarations in local scopes. I'm writing more code in declarative parts.
> 
> Cons: the temptation of writing function bodies in the spec is too big. 
> At least I try to keep them in the private part, but I've found myself 
> trying to force an expression function just to avoid a package body.
> 
> Care to share your experiences?

Better not to have any.

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

^ permalink raw reply	[flat|nested] 39+ messages in thread

* Re: "functional" programming in Ada
  2018-03-06 11:34 "functional" programming in Ada Alejandro R. Mosteo
  2018-03-06 13:09 ` Dmitry A. Kazakov
@ 2018-03-06 13:29 ` Mehdi Saada
  2018-03-06 14:34   ` Alejandro R. Mosteo
  2018-03-06 15:01 ` Dan'l Miller
                   ` (2 subsequent siblings)
  4 siblings, 1 reply; 39+ messages in thread
From: Mehdi Saada @ 2018-03-06 13:29 UTC (permalink / raw)


I so understand you Alexandro !
But I wonder why they even allowed to write these expression bodies in the specs.


^ permalink raw reply	[flat|nested] 39+ messages in thread

* Re: "functional" programming in Ada
  2018-03-06 13:29 ` Mehdi Saada
@ 2018-03-06 14:34   ` Alejandro R. Mosteo
  2018-03-06 14:36     ` Mehdi Saada
  0 siblings, 1 reply; 39+ messages in thread
From: Alejandro R. Mosteo @ 2018-03-06 14:34 UTC (permalink / raw)


On 06/03/18 14:29, Mehdi Saada wrote:
> I so understand you Alexandro !
> But I wonder why they even allowed to write these expression bodies in the specs.

 From a compiler writer POV I may understand it for the same reasons we 
have the private part in the spec. But I'm kind of wishing that they 
were forcefully confined to the private part.


^ permalink raw reply	[flat|nested] 39+ messages in thread

* Re: "functional" programming in Ada
  2018-03-06 13:09 ` Dmitry A. Kazakov
@ 2018-03-06 14:35   ` Alejandro R. Mosteo
  2018-03-06 15:08     ` Dmitry A. Kazakov
  0 siblings, 1 reply; 39+ messages in thread
From: Alejandro R. Mosteo @ 2018-03-06 14:35 UTC (permalink / raw)


On 06/03/18 14:09, Dmitry A. Kazakov wrote:
> On 06/03/2018 12:34, Alejandro R. Mosteo wrote:
>> In a recent project I've started using in full if/case expressions and 
>> expression functions... and I'm a bit scared at the amount of use I 
>> have for them. I'm using these constantly.
> 
> That is how wrong ideas become most popular ones.

Do you find something inherently wrong, or is this particular 
implementation you object to?

>> Pros: purely recursive functions are really fun to write. If/case 
>> expressions, used sparingly, do help a lot in having constant 
>> declarations in local scopes. I'm writing more code in declarative parts.
>>
>> Cons: the temptation of writing function bodies in the spec is too 
>> big. At least I try to keep them in the private part, but I've found 
>> myself trying to force an expression function just to avoid a package 
>> body.
>>
>> Care to share your experiences?
> 
> Better not to have any.

:-)

^ permalink raw reply	[flat|nested] 39+ messages in thread

* Re: "functional" programming in Ada
  2018-03-06 14:34   ` Alejandro R. Mosteo
@ 2018-03-06 14:36     ` Mehdi Saada
  2018-03-06 15:27       ` Alejandro R. Mosteo
                         ` (2 more replies)
  0 siblings, 3 replies; 39+ messages in thread
From: Mehdi Saada @ 2018-03-06 14:36 UTC (permalink / raw)


> From a compiler writer POV I may understand it for the same reasons we 
> have the private part in the spec.
How come ? Why should the compiler handle those functions differently than normal functions whose body is forbidden to be anywhere else than in the package body ?

^ permalink raw reply	[flat|nested] 39+ messages in thread

* "functional" programming in Ada
  2018-03-06 11:34 "functional" programming in Ada Alejandro R. Mosteo
  2018-03-06 13:09 ` Dmitry A. Kazakov
  2018-03-06 13:29 ` Mehdi Saada
@ 2018-03-06 15:01 ` Dan'l Miller
  2018-03-06 15:25   ` Alejandro R. Mosteo
  2018-03-07 10:07 ` Maciej Sobczak
  2018-03-08 18:24 ` G. B.
  4 siblings, 1 reply; 39+ messages in thread
From: Dan'l Miller @ 2018-03-06 15:01 UTC (permalink / raw)


Alejandro R. Mosteo wrote:
> Pros: purely recursive functions are really fun to write. If/case 
> expressions, used sparingly, do help a lot in having constant 
> declarations in local scopes. I'm writing more code in declarative parts. 

Be careful or else you will be yearning to write in Ada the full-fledged meta-template programming abomination that C++ has become in the past decade and a half.  If the Ada community were to ever want to have functional programming within Ada (as opposed to, say, bolting Ada & Haskell or Ada & OCaml together better), especially compile-time functional programming in Ada, then it should be overtly well-designed to walk in the front door, not sneak in the backdoor as it did in C++ when they/Alexandrescu ‘discovered’ that C++'s templates/generics were (just barely) Turing complete with syntax-as-nearly-unreadable-subtext that is perhaps even more cryptic than infinite-length tapes in a Turing machine.


^ permalink raw reply	[flat|nested] 39+ messages in thread

* Re: "functional" programming in Ada
  2018-03-06 14:35   ` Alejandro R. Mosteo
@ 2018-03-06 15:08     ` Dmitry A. Kazakov
  2018-03-06 16:00       ` Manuel Collado
  0 siblings, 1 reply; 39+ messages in thread
From: Dmitry A. Kazakov @ 2018-03-06 15:08 UTC (permalink / raw)


On 06/03/2018 15:35, Alejandro R. Mosteo wrote:
> On 06/03/18 14:09, Dmitry A. Kazakov wrote:
>> On 06/03/2018 12:34, Alejandro R. Mosteo wrote:
>>> In a recent project I've started using in full if/case expressions 
>>> and expression functions... and I'm a bit scared at the amount of use 
>>> I have for them. I'm using these constantly.
>>
>> That is how wrong ideas become most popular ones.
> 
> Do you find something inherently wrong,

Yes, both functional programming paradigm and ways to break out of it. 
The latter is doubly wrong. If functional programming is so cool why 
would anybody wrap procedural building blocks into functional ones?

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

^ permalink raw reply	[flat|nested] 39+ messages in thread

* Re: "functional" programming in Ada
  2018-03-06 15:01 ` Dan'l Miller
@ 2018-03-06 15:25   ` Alejandro R. Mosteo
  0 siblings, 0 replies; 39+ messages in thread
From: Alejandro R. Mosteo @ 2018-03-06 15:25 UTC (permalink / raw)


On 06/03/18 16:01, Dan'l Miller wrote:
> Alejandro R. Mosteo wrote:
>> Pros: purely recursive functions are really fun to write. If/case
>> expressions, used sparingly, do help a lot in having constant
>> declarations in local scopes. I'm writing more code in declarative parts.
> 
> Be careful or else you will be yearning to write in Ada the full-fledged meta-template programming abomination that C++ has become in the past decade and a half.  If the Ada community were to ever want to have functional programming within Ada (as opposed to, say, bolting Ada & Haskell or Ada & OCaml together better), especially compile-time functional programming in Ada, then it should be overtly well-designed to walk in the front door, not sneak in the backdoor as it did in C++ when they/Alexandrescu ‘discovered’ that C++'s templates/generics were (just barely) Turing complete with syntax-as-nearly-unreadable-subtext that is perhaps even more cryptic than infinite-length tapes in a Turing machine.
> 

There's a reason I quoted the functional in the subject ;-)

I share the feeling nonetheless, I'm no fan (to put it mildly) of C++ 
template metaprogramming,

^ permalink raw reply	[flat|nested] 39+ messages in thread

* Re: "functional" programming in Ada
  2018-03-06 14:36     ` Mehdi Saada
@ 2018-03-06 15:27       ` Alejandro R. Mosteo
  2018-03-06 16:26       ` Jeffrey R. Carter
  2018-03-06 20:17       ` Randy Brukardt
  2 siblings, 0 replies; 39+ messages in thread
From: Alejandro R. Mosteo @ 2018-03-06 15:27 UTC (permalink / raw)


On 06/03/18 15:36, Mehdi Saada wrote:
>>  From a compiler writer POV I may understand it for the same reasons we
>> have the private part in the spec.
> How come ? Why should the compiler handle those functions differently than normal functions whose body is forbidden to be anywhere else than in the package body ?
> 

I suppose they simplify distribution of specs + object code with better 
inlining, but that's just a guess.


^ permalink raw reply	[flat|nested] 39+ messages in thread

* Re: "functional" programming in Ada
  2018-03-06 15:08     ` Dmitry A. Kazakov
@ 2018-03-06 16:00       ` Manuel Collado
  2018-03-06 16:37         ` Dmitry A. Kazakov
  2018-03-07  4:46         ` Paul Rubin
  0 siblings, 2 replies; 39+ messages in thread
From: Manuel Collado @ 2018-03-06 16:00 UTC (permalink / raw)


El 06/03/2018 a las 16:08, Dmitry A. Kazakov escribió:
> On 06/03/2018 15:35, Alejandro R. Mosteo wrote:
>>
>> Do you find something inherently wrong,
>
> Yes, both functional programming paradigm and ways to break out of it.
> The latter is doubly wrong. If functional programming is so cool why
> would anybody wrap procedural building blocks into functional ones?
>

Well, it may sound a bit heterodox, but IMHO functional programming is 
just a subset of imperative (= procedural) programming.

- Functional programming = expressions
- Imperative programming = expressions + variables + procedural actions

So why avoid the power of some functional programming expressions in the 
imperative programming world?

Just my 2c.
-- 
Manuel Collado - http://lml.ls.fi.upm.es/~mcollado

^ permalink raw reply	[flat|nested] 39+ messages in thread

* Re: "functional" programming in Ada
  2018-03-06 14:36     ` Mehdi Saada
  2018-03-06 15:27       ` Alejandro R. Mosteo
@ 2018-03-06 16:26       ` Jeffrey R. Carter
  2018-03-06 20:17       ` Randy Brukardt
  2 siblings, 0 replies; 39+ messages in thread
From: Jeffrey R. Carter @ 2018-03-06 16:26 UTC (permalink / raw)


On 03/06/2018 03:36 PM, Mehdi Saada wrote:
>>  From a compiler writer POV I may understand it for the same reasons we
>> have the private part in the spec.
> How come ? Why should the compiler handle those functions differently than normal functions whose body is forbidden to be anywhere else than in the package body ?

According to the Ada-12 Rationale, expression functions were added to help with 
contracts.

-- 
Jeff Carter
"He that hath no beard is less than a man."
Much Ado About Nothing
132

^ permalink raw reply	[flat|nested] 39+ messages in thread

* Re: "functional" programming in Ada
  2018-03-06 16:00       ` Manuel Collado
@ 2018-03-06 16:37         ` Dmitry A. Kazakov
  2018-03-06 22:16           ` Manuel Collado
  2018-03-07  4:46         ` Paul Rubin
  1 sibling, 1 reply; 39+ messages in thread
From: Dmitry A. Kazakov @ 2018-03-06 16:37 UTC (permalink / raw)


On 06/03/2018 17:00, Manuel Collado wrote:
> El 06/03/2018 a las 16:08, Dmitry A. Kazakov escribió:
>> On 06/03/2018 15:35, Alejandro R. Mosteo wrote:
>>>
>>> Do you find something inherently wrong,
>>
>> Yes, both functional programming paradigm and ways to break out of it.
>> The latter is doubly wrong. If functional programming is so cool why
>> would anybody wrap procedural building blocks into functional ones?
>>
> 
> Well, it may sound a bit heterodox, but IMHO functional programming is 
> just a subset of imperative (= procedural) programming.
> 
> - Functional programming = expressions
> - Imperative programming = expressions + variables + procedural actions

Imperative is in opposition to declarative. Another axis is stateless 
vs. stateful. Procedural is usually attributed to the method of 
decomposition: procedural vs. object vs. functional vs. data/event 
driven etc.

Ada used to strictly separate imperative from declarative and took care 
about the states, especially about the correspondence between the 
program state and problem domain. Then Ada supported both procedural and 
object decomposition, even Ada 83 with its abstract data types.

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

^ permalink raw reply	[flat|nested] 39+ messages in thread

* Re: "functional" programming in Ada
  2018-03-06 14:36     ` Mehdi Saada
  2018-03-06 15:27       ` Alejandro R. Mosteo
  2018-03-06 16:26       ` Jeffrey R. Carter
@ 2018-03-06 20:17       ` Randy Brukardt
  2018-03-07 14:30         ` Alejandro R. Mosteo
  2 siblings, 1 reply; 39+ messages in thread
From: Randy Brukardt @ 2018-03-06 20:17 UTC (permalink / raw)


"Mehdi Saada" <00120260a@gmail.com> wrote in message 
news:cd48925d-5cac-465c-96c3-a392f0ce4079@googlegroups.com...
>> From a compiler writer POV I may understand it for the same reasons we
>> have the private part in the spec.
> How come ? Why should the compiler handle those functions differently
> than normal functions whose body is forbidden to be anywhere else than in 
> the package body ?

It helps other (non-Ada) tools; in particular proof and analysis tools, if 
the entire details of a precondition/postcondition are available to the 
tools (and without depending on contents of bodies). This literally led to 
preconditions that were many pages long. Expression functions were 
introduced in part to allow some abstraction in contracts without hiding the 
details of thosee contracts from the tools.

Secondarily, a compiler can take advantage of these for better inlining and 
better optimization of contracts. [The real reason I was interested.] They 
also open up some other possibilities (not all taken advantage of yet): 
user-defined static expressions; default implementation of functions for 
interfaces; anonymous functions to pass for one-time use parameters.

Generally, I'd expect them to appear mainly in private parts, because the 
visible spec shouldn't include enough info to be able to usefully implement 
much -- you usually need access to the components of the central private 
type in order to write such a function.

They *are* tempting to use, especially in quick-and-dirty code (like ACATS 
tests). I've found myself having to remove them from tests that are supposed 
to work on Ada 95 or Ada 2005.

                             Randy.



^ permalink raw reply	[flat|nested] 39+ messages in thread

* Re: "functional" programming in Ada
  2018-03-06 16:37         ` Dmitry A. Kazakov
@ 2018-03-06 22:16           ` Manuel Collado
  2018-03-07  8:41             ` Dmitry A. Kazakov
  0 siblings, 1 reply; 39+ messages in thread
From: Manuel Collado @ 2018-03-06 22:16 UTC (permalink / raw)


El 06/03/2018 a las 17:37, Dmitry A. Kazakov escribió:
> On 06/03/2018 17:00, Manuel Collado wrote:
>>
>> Well, it may sound a bit heterodox, but IMHO functional programming is
>> just a subset of imperative (= procedural) programming.
>>
>> - Functional programming = expressions
>> - Imperative programming = expressions + variables + procedural actions
>
> Imperative is in opposition to declarative. Another axis is stateless
> vs. stateful. Procedural is usually attributed to the method of
> decomposition: procedural vs. object vs. functional vs. data/event
> driven etc.
>
> Ada used to strictly separate imperative from declarative and took care
> about the states, especially about the correspondence between the
> program state and problem domain. Then Ada supported both procedural and
> object decomposition, even Ada 83 with its abstract data types.

Did I mentioned the word "declarative"?

Functional and declarative are different axis. Fans of functional 
programming claim it is declarative "per se". Not me.

Expressions without side-effects are functional, and not necessarily 
declarative. Prolog is declarative, and not functional.

Regards.
-- 
Manuel Collado - http://lml.ls.fi.upm.es/~mcollado

^ permalink raw reply	[flat|nested] 39+ messages in thread

* Re: "functional" programming in Ada
  2018-03-06 16:00       ` Manuel Collado
  2018-03-06 16:37         ` Dmitry A. Kazakov
@ 2018-03-07  4:46         ` Paul Rubin
  1 sibling, 0 replies; 39+ messages in thread
From: Paul Rubin @ 2018-03-07  4:46 UTC (permalink / raw)


Manuel Collado <m-collado@users.sourceforge.net> writes:
> Well, it may sound a bit heterodox, but IMHO functional programming is
> just a subset of imperative (= procedural) programming.
>
> - Functional programming = expressions
> - Imperative programming = expressions + variables + procedural actions

By that logic, typed programming is just a subset of untyped
programming.

 - (sufficiently) typed programming = expressions with well-defined values
   
 - untyped programming: expressions with well-defined values +
   expressions with undefined values + arbitrary pointers and memory
   corruption
    
> So why avoid the power of some functional programming expressions in
> the imperative programming world?

Because eliminating dangerous features from a language can increase its
safety, predicability, etc.  Whether that applies to functional vs Ada
depends on a lot of things, but the generalization you seem to suppose
(that adding more power never does harm) makes no sense.

^ permalink raw reply	[flat|nested] 39+ messages in thread

* Re: "functional" programming in Ada
  2018-03-06 22:16           ` Manuel Collado
@ 2018-03-07  8:41             ` Dmitry A. Kazakov
  0 siblings, 0 replies; 39+ messages in thread
From: Dmitry A. Kazakov @ 2018-03-07  8:41 UTC (permalink / raw)


On 06/03/2018 23:16, Manuel Collado wrote:
> El 06/03/2018 a las 17:37, Dmitry A. Kazakov escribió:
>> On 06/03/2018 17:00, Manuel Collado wrote:
>>>
>>> Well, it may sound a bit heterodox, but IMHO functional programming is
>>> just a subset of imperative (= procedural) programming.
>>>
>>> - Functional programming = expressions
>>> - Imperative programming = expressions + variables + procedural actions
>>
>> Imperative is in opposition to declarative. Another axis is stateless
>> vs. stateful. Procedural is usually attributed to the method of
>> decomposition: procedural vs. object vs. functional vs. data/event
>> driven etc.
>>
>> Ada used to strictly separate imperative from declarative and took care
>> about the states, especially about the correspondence between the
>> program state and problem domain. Then Ada supported both procedural and
>> object decomposition, even Ada 83 with its abstract data types.
> 
> Did I mentioned the word "declarative"?
> 
> Functional and declarative are different axis. Fans of functional 
> programming claim it is declarative "per se". Not me.
> 
> Expressions without side-effects are functional, and not necessarily 
> declarative.

Absence of side-effects does not make it functional:

    procedure Swap (X, Y : in out Integer);

is imperative and has no side-effects.

Stateless constructs, if that fiction exists, are functional and 
necessarily declarative.

But I would attribute "functional" rather to the decomposition method. 
Other attributes are more of less consequences of choice. Standing on 
your head, changes the gait... (:-))

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


^ permalink raw reply	[flat|nested] 39+ messages in thread

* Re: "functional" programming in Ada
  2018-03-06 11:34 "functional" programming in Ada Alejandro R. Mosteo
                   ` (2 preceding siblings ...)
  2018-03-06 15:01 ` Dan'l Miller
@ 2018-03-07 10:07 ` Maciej Sobczak
  2018-03-07 10:52   ` Mehdi Saada
  2018-03-07 15:03   ` Alejandro R. Mosteo
  2018-03-08 18:24 ` G. B.
  4 siblings, 2 replies; 39+ messages in thread
From: Maciej Sobczak @ 2018-03-07 10:07 UTC (permalink / raw)


On Tuesday, March 6, 2018 at 12:34:32 PM UTC+1, Alejandro R. Mosteo wrote:

> I'm writing more code in declarative parts.

It is interesting how language evolution leads to mixing of ideas or even dropping of original values.
If you write code in declarative parts (which also includes calling functions and using complex expressions to initialize variables at the point of declaration), then Ada might as well abandon the whole concept of dividing the code into declarative and imperative parts. If you can implement your whole system in the declarative part, then this division does not make sense any longer.

The argument about tools using these expressions (in contracts, for example) is interesting as well, because tools also benefit from simpler grammar and strict code structure. Apparently there is no single formula for a perfect language!

My (current[*]) own preference is to avoid mixing programming styles in a single language and instead mix languages in a single system. In addition to forcing me to put more thought into the design, it also makes language purists happy. :-) If you find it funny to write in functional style, why not compose your system from parts written in Ada with parts written in [put your *other* favorite language here]? Why abuse a single language to do what it was not originally supposed to do?

[*] Disclaimer: current preferences become obsolete with time. I reserve full rights to change my mind in the next post.

-- 
Maciej Sobczak * http://www.inspirel.com


^ permalink raw reply	[flat|nested] 39+ messages in thread

* Re: "functional" programming in Ada
  2018-03-07 10:07 ` Maciej Sobczak
@ 2018-03-07 10:52   ` Mehdi Saada
  2018-03-07 13:11     ` Pascal Obry
  2018-03-07 15:03   ` Alejandro R. Mosteo
  1 sibling, 1 reply; 39+ messages in thread
From: Mehdi Saada @ 2018-03-07 10:52 UTC (permalink / raw)


I am myself a purist in becoming, but I'm curious as to the statement of Randy, that such constructions that mix bodies and specs, like expression functions, allow better analysis from tools.
Why not writing everything in the specs then ? Maybe the original separation of specs and bodies is a mistake, in the light of recent tools requirements.
... I'm just playing devil's advocate, don't shoot.


^ permalink raw reply	[flat|nested] 39+ messages in thread

* Re: "functional" programming in Ada
  2018-03-07 10:52   ` Mehdi Saada
@ 2018-03-07 13:11     ` Pascal Obry
  2018-03-07 13:53       ` Dmitry A. Kazakov
                         ` (2 more replies)
  0 siblings, 3 replies; 39+ messages in thread
From: Pascal Obry @ 2018-03-07 13:11 UTC (permalink / raw)


Le mercredi 07 mars 2018 à 02:52 -0800, Mehdi Saada a écrit :
> Why not writing everything in the specs then ? Maybe the original
> separation of specs and bodies is a mistake, in the light of recent
> tools requirements.

The spec is what is exposed to other units.

The body is implementation details.

The separation is to me one of the most important point in Ada. I think
that all languages should have done that. It is an welcomed separation
for software engineer.

My 2 cents,

-- 
  Pascal Obry /  Magny Les Hameaux (78)

  The best way to travel is by means of imagination

  http://www.obry.net

  gpg --keyserver keys.gnupg.net --recv-key F949BD3B


^ permalink raw reply	[flat|nested] 39+ messages in thread

* Re: "functional" programming in Ada
  2018-03-07 13:11     ` Pascal Obry
@ 2018-03-07 13:53       ` Dmitry A. Kazakov
  2018-03-07 16:13       ` Dan'l Miller
  2018-03-08  3:34       ` Randy Brukardt
  2 siblings, 0 replies; 39+ messages in thread
From: Dmitry A. Kazakov @ 2018-03-07 13:53 UTC (permalink / raw)


On 07/03/2018 14:11, Pascal Obry wrote:
> Le mercredi 07 mars 2018 à 02:52 -0800, Mehdi Saada a écrit :
>> Why not writing everything in the specs then ? Maybe the original
>> separation of specs and bodies is a mistake, in the light of recent
>> tools requirements.
> 
> The spec is what is exposed to other units.
> 
> The body is implementation details.

Specification can be an implementation detail for some clients. That is 
why Ada has public and private parts.

> The separation is to me one of the most important point in Ada. I think
> that all languages should have done that. It is an welcomed separation
> for software engineer.

Yes. The principle is reducing coupling. Therefore anything the client 
does not need should be hidden from it. A related principle is having 
weakest possible preconditions. All things a client can see become 
precondition and thus strengthen it.

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

^ permalink raw reply	[flat|nested] 39+ messages in thread

* Re: "functional" programming in Ada
  2018-03-06 20:17       ` Randy Brukardt
@ 2018-03-07 14:30         ` Alejandro R. Mosteo
  0 siblings, 0 replies; 39+ messages in thread
From: Alejandro R. Mosteo @ 2018-03-07 14:30 UTC (permalink / raw)


On 06/03/18 21:17, Randy Brukardt wrote:

> Generally, I'd expect them to appear mainly in private parts, because the
> visible spec shouldn't include enough info to be able to usefully implement
> much -- you usually need access to the components of the central private
> type in order to write such a function.

Unless you find yourself writing functions that depend on other 
functions (possibly even from other packages), and then you are no 
longer restricted by private components...

At least that's what's happening to me.

Álex.


^ permalink raw reply	[flat|nested] 39+ messages in thread

* Re: "functional" programming in Ada
  2018-03-07 10:07 ` Maciej Sobczak
  2018-03-07 10:52   ` Mehdi Saada
@ 2018-03-07 15:03   ` Alejandro R. Mosteo
  2018-03-07 15:16     ` Alejandro R. Mosteo
                       ` (4 more replies)
  1 sibling, 5 replies; 39+ messages in thread
From: Alejandro R. Mosteo @ 2018-03-07 15:03 UTC (permalink / raw)


On 07/03/18 11:07, Maciej Sobczak wrote:
> On Tuesday, March 6, 2018 at 12:34:32 PM UTC+1, Alejandro R. Mosteo wrote:
> 
>> I'm writing more code in declarative parts.
> 
> It is interesting how language evolution leads to mixing of ideas or even dropping of original values.
> If you write code in declarative parts (which also includes calling functions and using complex expressions to initialize variables at the point of declaration), then Ada might as well abandon the whole concept of dividing the code into declarative and imperative parts. If you can implement your whole system in the declarative part, then this division does not make sense any longer.

That's an interesting point. I'm not sure the declare - begin part is 
that critical, since scopes are defined between begin - end anyway 
(which is frustrating for exceptions sometimes, when you want to ensure 
a subprogram won't raise from its declarative part).

Yet I wouldn't say that the new features are fundamentally tipping the 
scales; as you say you could always use functions in initializations, 
and I don't like writing complex expressions anyway (a single 
if/then/else or case at most; once nesting is needed it usually is 
reason enough to stop to think about what I'm doing).

At the moment my personal opinion is that the discussed features make 
writing Ada considerably more comfortable [*], with only a small 
additional risk of bad style, but not inherently unsafer code.

My only reservation, as I said, is allowing expression function bodies 
(not pre/post conditions) in public parts. Could this restriction have 
been enforced, or was it even on the table at some point? Probably I'm 
missing some reason for why it is not.

[*] Then only exception is that current gnat won't warn you about a 
missing body in a spec, when there is no body file yet. So you write a 
declaration for a function that you know is going to be an expression, 
forget to write it in the private part, and when compilation fails you 
have no idea of what function is missing, unless you create an empty 
body just to check. In files with many declarations it's bitten me a 
couple of times.

> The argument about tools using these expressions (in contracts, for example) is interesting as well, because tools also benefit from simpler grammar and strict code structure. Apparently there is no single formula for a perfect language!
> 
> My (current[*]) own preference is to avoid mixing programming styles in a single language and instead mix languages in a single system. In addition to forcing me to put more thought into the design, it also makes language purists happy. :-) If you find it funny to write in functional style, why not compose your system from parts written in Ada with parts written in [put your *other* favorite language here]? Why abuse a single language to do what it was not originally supposed to do?

He, I'm not a purist so I'll take what I'm given. That said, my old and 
limited experience with Lisp was that its easier to do some 
functional-like things in an imperative language, whereas when going 
fully functional you sorely miss some imperative facilities sooner than 
later. But this is probably that my first languages were imperative so 
I'm biased.

Recommendations for current functional languages? I know only of Haskell 
(and only by name).

> [*] Disclaimer: current preferences become obsolete with time. I reserve full rights to change my mind in the next post.

Duly noted ;)

^ permalink raw reply	[flat|nested] 39+ messages in thread

* Re: "functional" programming in Ada
  2018-03-07 15:03   ` Alejandro R. Mosteo
@ 2018-03-07 15:16     ` Alejandro R. Mosteo
  2018-03-07 20:34     ` Robert A Duff
                       ` (3 subsequent siblings)
  4 siblings, 0 replies; 39+ messages in thread
From: Alejandro R. Mosteo @ 2018-03-07 15:16 UTC (permalink / raw)


On 07/03/18 16:03, Alejandro R. Mosteo wrote:
> On 07/03/18 11:07, Maciej Sobczak wrote:
>> On Tuesday, March 6, 2018 at 12:34:32 PM UTC+1, Alejandro R. Mosteo 
>> wrote:
>>
>>> I'm writing more code in declarative parts.
>>
>> It is interesting how language evolution leads to mixing of ideas or 
>> even dropping of original values.
>> If you write code in declarative parts (which also includes calling 
>> functions and using complex expressions to initialize variables at the 
>> point of declaration), then Ada might as well abandon the whole 
>> concept of dividing the code into declarative and imperative parts. If 
>> you can implement your whole system in the declarative part, then this 
>> division does not make sense any longer.
> 
> That's an interesting point. I'm not sure the declare - begin part is 
> that critical, since scopes are defined between begin - end anyway 
> (which is frustrating for exceptions sometimes, when you want to ensure 
> a subprogram won't raise from its declarative part).

I when to write some code and quickly realized why the declare-begin is 
so handy for proper scoping ;)

^ permalink raw reply	[flat|nested] 39+ messages in thread

* Re: "functional" programming in Ada
  2018-03-07 13:11     ` Pascal Obry
  2018-03-07 13:53       ` Dmitry A. Kazakov
@ 2018-03-07 16:13       ` Dan'l Miller
  2018-03-12  0:13         ` Robert I. Eachus
  2018-03-08  3:34       ` Randy Brukardt
  2 siblings, 1 reply; 39+ messages in thread
From: Dan'l Miller @ 2018-03-07 16:13 UTC (permalink / raw)


Pascal Obry wrote:
> The •spec• is what is ••exposed to other units••. 
>
> The •body• is ••implementation•• details. 
>
> The separation is to me one of the most important point in Ada.

The separation is important in •modern Ada•.  Historically, {Rational's, Sun Microsystems'} Verdix Ada Development System (VADS) compiler had a #-prefixed compile-time subset of Ada 1) that played some role as a superduper extrapolation of what C or C++ use their preprocessor for and 2) that played some role as a source-code-reflective compile-time code generator à la OCaml's camlp4 does nowadays for OCaml.  In this alternative view, conversely:

The •spec• is what is the ••compiler•• is fully cognizant of at strictly compile-time.

The •body• is what only the ••hardware processor•• is fully cognizant of at run-time, most especially execution-time accumulated-state behaviors based on one or more execution-time inputs.

(And there might exist people who say that Pascal Obry's and Dan'l Miller's different wording there means exactly the same thing in the end.  On even-numbered days, I am one of those people.  Conversely, on odd-numbered days, I vociferously object!)

>  I think that all languages should have done that.

Some people (e.g., the Boost community over in C++ world; the users of camlp4 as a code generator in OCaml world; the a.app people in a prior Ada era; to some degree, the aspect-oriented programming [AOP] people) believe that compiled languages should have a compiler-internal compile-time ‘language’ in which poor-man's code generation/tweaking/trait-based-selection or full-fledged code generation can be expressed as imperative and/or functional code that the compiler invokes at compile-time to tailor/weave the source code to be automatedly different than what  a human being submitted as input to the compiler.  The burning question of our era is, ‘who gets to author code:  human or (multistage-)compiler or both’?  The school of thought that fully embraces this (with perhaps even more than 2 stages:  compile-time & run-time mentioned so far here) is multi-stage programming, where an app's source code may beget source-code generation may beget source-code generation may beget ... may beget source-code generation may beget compiled machine code.  (In some variants, replace at least some of those “source-code generation” phrases with ‘intermediate-representation generation’ phrases there.)

Because C++, OCaml, AOP aspect weavers for various languages, and an earlier a.app era of Ada keep reinventing this wheel (differently), apparently there exist people spanning several decades who “think all languages should have done that”, where “that” is having a compile-time language of some sort governing/tuning/tweaking/extending the compiler's ability to generate machine code from human-authored/non-generated source code.  (To varying degrees, Seed7, 1970's era Alphard ,and the ‘little languages’ subset of the OCaml community even go so far as to say that the human-being author of an app should be able to declare fresh novel syntax & semantics of the app's source code to the compiler, instead of having, say, Ada's syntax & semantics chiseled in stone by a committee.)

> It is an welcomed separation for software engineer. 

The existence of the (highly impaired) C preprocessor, Ocaml's camlp4, VADS's a.app, AOP's aspect weavers, and C++'s Boost metatemplate programming all point that compile-time-invoked source code versus run-time-invoked source code in compilers is “a[] welcomed separation for [some] software engineer[s].”

Rather than advocating all this, I am merely pointing out extant facts.  I am quite appalled at what this compile-time-code school of thought has done to C++'s readability (and perhaps a few other software-architectural -abilities regarding C++) by sneaking it in the back door via their ‘discovery’ that C++'s templates are (just barely) Turing complete.  Conversely, I am quite an admirer of full-fledged much-more-readable walk-in-the-front-door multi-stage programming's 1 or more stages of source-code generation then machine-code generation, preferably within the same language with immense amounts of reflection and self-reflection-based analysis and grinding; OCaml world (and perhaps some of the Java-based aspect weavers of AOP-of-Java) perform this much more admirably than, say, poor-man MTP in C++ does.

I mention all of this, so that Ada community is aware of slopes that they might be standing on, so as to not make them slippery, as C++ did.


^ permalink raw reply	[flat|nested] 39+ messages in thread

* Re: "functional" programming in Ada
  2018-03-07 15:03   ` Alejandro R. Mosteo
  2018-03-07 15:16     ` Alejandro R. Mosteo
@ 2018-03-07 20:34     ` Robert A Duff
  2018-03-07 22:47     ` Jeffrey R. Carter
                       ` (2 subsequent siblings)
  4 siblings, 0 replies; 39+ messages in thread
From: Robert A Duff @ 2018-03-07 20:34 UTC (permalink / raw)


"Alejandro R. Mosteo" <alejandro@mosteo.com> writes:

> Recommendations for current functional languages? I know only of Haskell
> (and only by name).

OCaml

- Bob


^ permalink raw reply	[flat|nested] 39+ messages in thread

* Re: "functional" programming in Ada
  2018-03-07 15:03   ` Alejandro R. Mosteo
  2018-03-07 15:16     ` Alejandro R. Mosteo
  2018-03-07 20:34     ` Robert A Duff
@ 2018-03-07 22:47     ` Jeffrey R. Carter
  2018-03-08  0:26     ` Shark8
  2018-03-08  0:45     ` Paul Rubin
  4 siblings, 0 replies; 39+ messages in thread
From: Jeffrey R. Carter @ 2018-03-07 22:47 UTC (permalink / raw)


On 03/07/2018 04:03 PM, Alejandro R. Mosteo wrote:
> 
> Recommendations for current functional languages? I know only of Haskell (and 
> only by name).

Erlang is interesting for an Ada person because it has concurrency in the 
language. Elixir is a similar language that targets the Erlang VM, IIRC.

-- 
Jeff Carter
"I snapped my chin down onto some guy's fist and
hit another one in the knee with my nose."
Play It Again, Sam
129


^ permalink raw reply	[flat|nested] 39+ messages in thread

* Re: "functional" programming in Ada
  2018-03-07 15:03   ` Alejandro R. Mosteo
                       ` (2 preceding siblings ...)
  2018-03-07 22:47     ` Jeffrey R. Carter
@ 2018-03-08  0:26     ` Shark8
  2018-03-08  0:45     ` Paul Rubin
  4 siblings, 0 replies; 39+ messages in thread
From: Shark8 @ 2018-03-08  0:26 UTC (permalink / raw)


On Wednesday, March 7, 2018 at 8:03:29 AM UTC-7, Alejandro R. Mosteo wrote:
> 
> Recommendations for current functional languages? I know only of Haskell 
> (and only by name).

Erlang.


^ permalink raw reply	[flat|nested] 39+ messages in thread

* Re: "functional" programming in Ada
  2018-03-07 15:03   ` Alejandro R. Mosteo
                       ` (3 preceding siblings ...)
  2018-03-08  0:26     ` Shark8
@ 2018-03-08  0:45     ` Paul Rubin
  2018-03-08 11:07       ` Alejandro R. Mosteo
  4 siblings, 1 reply; 39+ messages in thread
From: Paul Rubin @ 2018-03-08  0:45 UTC (permalink / raw)


"Alejandro R. Mosteo" <alejandro@mosteo.com> writes:
> Recommendations for current functional languages? I know only of
> Haskell (and only by name).

If you want to get a deep understanding of what FP is about as a
programming language topic, I'd go with Haskell.  Be aware that Haskell
does things the way mathematicians do things: very rigorous and precise
at the actual logical level, but more casual and relaxed at the
organizational level.

If you want something more like Ada, i.e. designed with attention to
large-scale engineering features like separating spec from
implementation, try Standard ML or the somewhat looser OCaml.  Either of
these will be a less mathematically rigorous than Haskell at the value
and expression level, but have a much more serious module system,
something like Ada's.

Erlang and Elixir are more like Lisp or Python: they give a very quick
and productive way to get simple things done, without much help for
larger-scale rigor.  The interesting thing about them is their
concurrency system implements what the programmer sees as isolated
lightweight processes communicating by message passing.  That means you
can split a big problem into smaller ones, so you can use low-tech
methods on the small problems, letting the process isolation keep the
subproblem solutions from interfering with each other too much.

FWIW you can think of Erlang as a concurrent Lisp system with a front
end for a funky Prolog-like syntax.  Elixir is the same thing except the
surface syntax is designed to look like Ruby.  There's also LFE
(Lisp-flavored Erlang), same idea except it looks like actual Lisp.

^ permalink raw reply	[flat|nested] 39+ messages in thread

* Re: "functional" programming in Ada
  2018-03-07 13:11     ` Pascal Obry
  2018-03-07 13:53       ` Dmitry A. Kazakov
  2018-03-07 16:13       ` Dan'l Miller
@ 2018-03-08  3:34       ` Randy Brukardt
  2018-03-08  8:23         ` Dmitry A. Kazakov
  2 siblings, 1 reply; 39+ messages in thread
From: Randy Brukardt @ 2018-03-08  3:34 UTC (permalink / raw)


[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain, Size: 1785 bytes --]


"Pascal Obry" <pascal@obry.net> wrote in message 
news:1520428274.2488.155.camel@obry.net...
Le mercredi 07 mars 2018 à 02:52 -0800, Mehdi Saada a écrit :
>> Why not writing everything in the specs then ? Maybe the original
>> separation of specs and bodies is a mistake, in the light of recent
>> tools requirements.
>
>The spec is what is exposed to other units.
>
>The body is implementation details.
>
>The separation is to me one of the most important point in Ada. I think
>that all languages should have done that. It is an welcomed separation
>for software engineer.

Right. And note that the specification has always contained elements which 
are determined at runtime (that is, executed). For instance, even in Ada 83 
you could have a subtype like:

      subtype Dyn is Natural range 1 .. Some_Function;

and to properly export Dyn, one has to execute code.

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.

While the line separating the specification and the implementation is very 
important, it is also a blurry line (and always has been). Also note that 
the private part is effectively part of the body (that is, the 
implementation part), and that is where 95% of expression functions end up. 
So while they are physically in the source code of the specification, they 
still belong to the body. (The private part, after all, is a hack to ease 
implementation. Expression functions are similar in a way, although it is 
not the Ada implementation that they are intended to help.)

                                          Randy.



^ permalink raw reply	[flat|nested] 39+ messages in thread

* Re: "functional" programming in Ada
  2018-03-08  3:34       ` Randy Brukardt
@ 2018-03-08  8:23         ` Dmitry A. Kazakov
  2018-03-08 22:49           ` G. B.
  2018-03-09  8:40           ` Simon Wright
  0 siblings, 2 replies; 39+ messages in thread
From: Dmitry A. Kazakov @ 2018-03-08  8:23 UTC (permalink / raw)


On 08/03/2018 04:34, Randy Brukardt wrote:
> "Pascal Obry" <pascal@obry.net> wrote in message
> news:1520428274.2488.155.camel@obry.net...
> Le mercredi 07 mars 2018 à 02:52 -0800, Mehdi Saada a écrit :
>>> Why not writing everything in the specs then ? Maybe the original
>>> separation of specs and bodies is a mistake, in the light of recent
>>> tools requirements.
>>
>> The spec is what is exposed to other units.
>>
>> The body is implementation details.
>>
>> The separation is to me one of the most important point in Ada. I think
>> that all languages should have done that. It is an welcomed separation
>> for software engineer.
> 
> Right. And note that the specification has always contained elements which
> are determined at runtime (that is, executed). For instance, even in Ada 83
> you could have a subtype like:
> 
>        subtype Dyn is Natural range 1 .. Some_Function;
> 
> and to properly export Dyn, one has to execute code.

Determined at run-time /= determined in a specific way. Even if 
evaluation of an expression is static, when that expression is an 
implementation, that thing has *nothing* to seek in the specifications. 
Specifications must be only specifications regardless when and how 
evaluated.

> 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).

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


^ permalink raw reply	[flat|nested] 39+ messages in thread

* Re: "functional" programming in Ada
  2018-03-08  0:45     ` Paul Rubin
@ 2018-03-08 11:07       ` Alejandro R. Mosteo
  0 siblings, 0 replies; 39+ messages in thread
From: Alejandro R. Mosteo @ 2018-03-08 11:07 UTC (permalink / raw)


On 08/03/18 01:45, Paul Rubin wrote:
> "Alejandro R. Mosteo" <alejandro@mosteo.com> writes:
>> Recommendations for current functional languages? I know only of
>> Haskell (and only by name).

Wow, thank you everybody for the suggestions and explanations. That's a 
bunch of interesting possibilities.

In another life I was proficient in Lisp and Prolog, but now I'm doing 
Ada when not scripting... so there's something attractive in every choice.

I guess I'll wait for some outward influence to push me in an avoidable 
direction ;-)

Álex.

> 
> If you want to get a deep understanding of what FP is about as a
> programming language topic, I'd go with Haskell.  Be aware that Haskell
> does things the way mathematicians do things: very rigorous and precise
> at the actual logical level, but more casual and relaxed at the
> organizational level.
> 
> If you want something more like Ada, i.e. designed with attention to
> large-scale engineering features like separating spec from
> implementation, try Standard ML or the somewhat looser OCaml.  Either of
> these will be a less mathematically rigorous than Haskell at the value
> and expression level, but have a much more serious module system,
> something like Ada's.
> 
> Erlang and Elixir are more like Lisp or Python: they give a very quick
> and productive way to get simple things done, without much help for
> larger-scale rigor.  The interesting thing about them is their
> concurrency system implements what the programmer sees as isolated
> lightweight processes communicating by message passing.  That means you
> can split a big problem into smaller ones, so you can use low-tech
> methods on the small problems, letting the process isolation keep the
> subproblem solutions from interfering with each other too much.
> 
> FWIW you can think of Erlang as a concurrent Lisp system with a front
> end for a funky Prolog-like syntax.  Elixir is the same thing except the
> surface syntax is designed to look like Ruby.  There's also LFE
> (Lisp-flavored Erlang), same idea except it looks like actual Lisp.
> 


^ permalink raw reply	[flat|nested] 39+ messages in thread

* Re: "functional" programming in Ada
  2018-03-06 11:34 "functional" programming in Ada Alejandro R. Mosteo
                   ` (3 preceding siblings ...)
  2018-03-07 10:07 ` Maciej Sobczak
@ 2018-03-08 18:24 ` G. B.
  2018-03-09 14:41   ` Alejandro R. Mosteo
  4 siblings, 1 reply; 39+ messages in thread
From: G. B. @ 2018-03-08 18:24 UTC (permalink / raw)


Alejandro R. Mosteo <alejandro@mosteo.com> wrote:
> I've found myself 
> trying to force an expression function just to avoid a package body.
> 
> Care to share your experiences?

It all breaks down when I need to “see”
the computation, like when tracing.


^ permalink raw reply	[flat|nested] 39+ messages in thread

* Re: "functional" programming in Ada
  2018-03-08  8:23         ` Dmitry A. Kazakov
@ 2018-03-08 22:49           ` G. B.
  2018-03-09  8:38             ` Dmitry A. Kazakov
  2018-03-09  8:40           ` Simon Wright
  1 sibling, 1 reply; 39+ messages in thread
From: G. B. @ 2018-03-08 22:49 UTC (permalink / raw)


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.

^ permalink raw reply	[flat|nested] 39+ messages in thread

* Re: "functional" programming in Ada
  2018-03-08 22:49           ` G. B.
@ 2018-03-09  8:38             ` Dmitry A. Kazakov
  0 siblings, 0 replies; 39+ messages in thread
From: Dmitry A. Kazakov @ 2018-03-09  8:38 UTC (permalink / raw)


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

^ permalink raw reply	[flat|nested] 39+ messages in thread

* Re: "functional" programming in Ada
  2018-03-08  8:23         ` Dmitry A. Kazakov
  2018-03-08 22:49           ` G. B.
@ 2018-03-09  8:40           ` Simon Wright
  2018-03-09 13:39             ` Dmitry A. Kazakov
  1 sibling, 1 reply; 39+ messages in thread
From: Simon Wright @ 2018-03-09  8:40 UTC (permalink / raw)


"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:
> 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).

When I was taught VDM (a long time ago, and never put to actual project
use) we wrote what are essentially contracts. You'd be left to implement
the corresponding code following the contracts.

Pre/postconditions etc correspond to these contracts, in a potentially
executable form, and I'm going to call them contracts as a convenient
shorthand (as in the Rationale).

As you know, the meaning of the program mustn't depend on actually
executing the contracts, and the default GNAT behaviour is not to
generate executable code for them (I don't know whether expression
functions which are only involved in contracts actually generate object
code, but one would hope they'd be eliminated by compiler analysis).

An expression function in the spec has to help in understanding what the
contract says. I wondered whether it might correspond to a lemma? ("a
subsidiary proposition , proved for use in the proof of another
proposition").

^ permalink raw reply	[flat|nested] 39+ messages in thread

* Re: "functional" programming in Ada
  2018-03-09  8:40           ` Simon Wright
@ 2018-03-09 13:39             ` Dmitry A. Kazakov
  0 siblings, 0 replies; 39+ messages in thread
From: Dmitry A. Kazakov @ 2018-03-09 13:39 UTC (permalink / raw)


On 09/03/2018 09:40, Simon Wright wrote:
> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:
>> 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).
> 
> When I was taught VDM (a long time ago, and never put to actual project
> use) we wrote what are essentially contracts. You'd be left to implement
> the corresponding code following the contracts.
> 
> Pre/postconditions etc correspond to these contracts, in a potentially
> executable form, and I'm going to call them contracts as a convenient
> shorthand (as in the Rationale).

Proper pre/post conditions are propositions to be used ("executed") in 
the logical inference/proof. They define the contract.

If an expression is used to define a contract, that contract is 
obviously undefined until the expression evaluated.

> As you know, the meaning of the program mustn't depend on actually
> executing the contracts, and the default GNAT behaviour is not to
> generate executable code for them (I don't know whether expression
> functions which are only involved in contracts actually generate object
> code, but one would hope they'd be eliminated by compiler analysis).

And if not?

> An expression function in the spec has to help in understanding what the
> contract says. I wondered whether it might correspond to a lemma? ("a
> subsidiary proposition , proved for use in the proof of another
> proposition").

There are propositions, theorems, lemmas. And there are algorithms, 
instructions etc. The former are never the latter and conversely. 
Expression-function can be either. That depends on the language we are 
talking about: #1 an expression of the meta-language of contracts or #2 
an expression of the object language Ada.

Now the point is that even if an expression-function were a part of the 
language of contracts, then that is still bad idea because the language 
design principles should hold for both languages. If the meta language 
of contracts becomes so complex that it would require procedural 
decomposition, then that must be done in a sane way, with separating 
interfaces and implementations. The contract-function would have bodies 
defined elsewhere rather than clumped together with specification.

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

^ permalink raw reply	[flat|nested] 39+ messages in thread

* Re: "functional" programming in Ada
  2018-03-08 18:24 ` G. B.
@ 2018-03-09 14:41   ` Alejandro R. Mosteo
  0 siblings, 0 replies; 39+ messages in thread
From: Alejandro R. Mosteo @ 2018-03-09 14:41 UTC (permalink / raw)


On 08/03/18 19:24, G. B. wrote:
> Alejandro R. Mosteo <alejandro@mosteo.com> wrote:
>> I've found myself
>> trying to force an expression function just to avoid a package body.
>>
>> Care to share your experiences?
> 
> It all breaks down when I need to “see”
> the computation, like when tracing.

This is something I've experienced too.

^ permalink raw reply	[flat|nested] 39+ messages in thread

* Re: "functional" programming in Ada
  2018-03-07 16:13       ` Dan'l Miller
@ 2018-03-12  0:13         ` Robert I. Eachus
  0 siblings, 0 replies; 39+ messages in thread
From: Robert I. Eachus @ 2018-03-12  0:13 UTC (permalink / raw)


On 3/7/2018 11:13 AM, Dan'l Miller wrote:

> I mention all of this, so that Ada community is aware of slopes that they might be standing on, so as to not make them slippery, as C++ did.
> 

There was a time when this was well accepted by the Ada community.  If 
you are designing a languages where ease of reading is considered much 
more important than ease of writing, it is obvious that having two 
distinct languages not only mixed on the page, but even on the same 
lines, and requiring the reader to parse potentially many lines to 
assign tokens to languages is not the way to go.

Yes, Ada does have modes, but they can usually be determined by looking 
at a single reserved word. A sequence of statements begins with begin, 
and a sequence of declarations begins with declare or is.


^ permalink raw reply	[flat|nested] 39+ messages in thread

end of thread, other threads:[~2018-03-12  0:13 UTC | newest]

Thread overview: 39+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2018-03-06 11:34 "functional" programming in Ada Alejandro R. Mosteo
2018-03-06 13:09 ` Dmitry A. Kazakov
2018-03-06 14:35   ` Alejandro R. Mosteo
2018-03-06 15:08     ` Dmitry A. Kazakov
2018-03-06 16:00       ` Manuel Collado
2018-03-06 16:37         ` Dmitry A. Kazakov
2018-03-06 22:16           ` Manuel Collado
2018-03-07  8:41             ` Dmitry A. Kazakov
2018-03-07  4:46         ` Paul Rubin
2018-03-06 13:29 ` Mehdi Saada
2018-03-06 14:34   ` Alejandro R. Mosteo
2018-03-06 14:36     ` Mehdi Saada
2018-03-06 15:27       ` Alejandro R. Mosteo
2018-03-06 16:26       ` Jeffrey R. Carter
2018-03-06 20:17       ` Randy Brukardt
2018-03-07 14:30         ` Alejandro R. Mosteo
2018-03-06 15:01 ` Dan'l Miller
2018-03-06 15:25   ` Alejandro R. Mosteo
2018-03-07 10:07 ` Maciej Sobczak
2018-03-07 10:52   ` Mehdi Saada
2018-03-07 13:11     ` Pascal Obry
2018-03-07 13:53       ` Dmitry A. Kazakov
2018-03-07 16:13       ` Dan'l Miller
2018-03-12  0:13         ` Robert I. Eachus
2018-03-08  3:34       ` Randy Brukardt
2018-03-08  8:23         ` Dmitry A. Kazakov
2018-03-08 22:49           ` G. B.
2018-03-09  8:38             ` Dmitry A. Kazakov
2018-03-09  8:40           ` Simon Wright
2018-03-09 13:39             ` Dmitry A. Kazakov
2018-03-07 15:03   ` Alejandro R. Mosteo
2018-03-07 15:16     ` Alejandro R. Mosteo
2018-03-07 20:34     ` Robert A Duff
2018-03-07 22:47     ` Jeffrey R. Carter
2018-03-08  0:26     ` Shark8
2018-03-08  0:45     ` Paul Rubin
2018-03-08 11:07       ` Alejandro R. Mosteo
2018-03-08 18:24 ` G. B.
2018-03-09 14:41   ` Alejandro R. Mosteo

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox