Re: Discriminated records are not the most efficient, but ...

["Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr>]

Le Sat, 21 Aug 2010 23:57:19 +0200, Yannick Duchêne (Hibou57)  
<yannick_duchene@yahoo.fr> a écrit:
> An opportunity to notice how Ada provides the concept to map this  
> element of functional programming to its imperative language. And there  
> may be others which can be easily mapped to Ada. Model in ML or SML  
> (prototyping at a very abstract level) and implement in Ada (get safety  
> and efficiency) ? May be an option for *some* applications.

A new episode in the great series “Beyond The Type” :)

Let me first give you a short (S)ML excerpt:

    datatype Tree =
       Leaf of int
     | Node of Tree * Tree;

Think of it as an Ada discriminated record, like

    type Tree_Kind is (A_Leaf, A_Node);

    type Tree_Type (Kind : Tree_Kind);
    type Tree_Access is access all Tree_Type;

    type Tree_Type (Kind : Tree_Kind) is record
       case Kind is
          when A_Leaf => Leaf : Integer;
          when A_Node => Left, Right : Tree_Access;
       end case;
    end record;

In
    datatype Tree =
       Leaf of int
     | Node of Tree * Tree;

“Tree” is an SML type, “Leaf” and “Node” are SML constructors. Think of  
these latters as two primitives functions returning each a subtype of  
Tree_Type:

Now, an SML function defined as

    fun
       Foo (Leaf (Value)) = Value
     | Foo (Node (Leaf (_), Leaf (Value))) = Value;

(here, the underscore “_” has the same meaning as with Prolog)

Think of it as the equivalent Ada function:

    function Foo (Tree : Tree_Type) return Integer
    is
    begin
       case Tree.Kind is
          when A_Leaf => return Tree.Leaf;
          when A_Node => return Tree.Left.Leaf;
       end case;
    end Foo;

OK. You will enjoy one more the awesome Ada case statement and its heavy  
reliability which will help you avoid most errors. But things might go  
wrong as you may guess. What if Tree.Left is not actually a “Tree_Type  
(A_Leaf)” ? Bam!, Run-Time Error! Eh, logic error, compiler cannot  
statically catch it.

I may guess you may like to say “where does it drive us, his silly  
'untyped' interpreted language will be far more worst”.

Wait a minute boys and girls, and let the magic play.

First of all, I know you already have a Janus or GNAT (aren't you ?), so I  
will not bother about it. But you may not already have either an SML-SJ or  
MLTon. Here are links (we will resume right after, don't go away right  
now):
http://www.smlnj.org/ (dated as far as October 2000, but still works as  
much fine as it was doing ten years ago)
http://mlton.org/ (more like an alive app, dated as near as 2008)

Open SML-NJ (an interactive interpreter, MLTon on the other side is a  
native code optimizing with global analysis compiler)

first, at the SML-NJ prompt, type:

    datatype Tree = Leaf of (int) | Node of (Tree * Tree);

(same as the one at the message opening, except standing on a single line)

Now, type

    fun Foo (Leaf (Value)) = Value | Foo (Node (Leaf (_), Leaf (Value))) =  
Value;

What happens ?

You should get a

    stdIn:28.1-28.77 Warning: match nonexhaustive
              Leaf Value => ...
              Node (Leaf _,Leaf Value) => ...

“Warning: match nonexhaustive”. This one is as cool as an error message  
 from an Ada compiler. What does it means ? You will see (or you may guess  
straight away). Now, type the following:

    fun Foo (Leaf (Value)) = Value | Foo (Node (_, Right)) = Foo (Right);

Now you should get.... no warning any more.

What Foo is supposed to stand for ? I give you the name of the function I  
was playing with : Last_Leaf. Now, you see why the first one was wrong,  
and why the second one is OK. The first one exactly match the one defined  
in Ada above, which would have passed compilation stage without hearing a  
fly bzzz. But this same, did not avoided a warning from SML-NJ.

So, what is the difference ? Abstraction : SML sees the constructors as  
part of the structure definition, while an Ada compiler would be unlikely  
so attempt such an analysis (the construction is a function for an Ada  
compiler, not part of of any type definition). Types and constructors are  
tied to each others.

Time to say also, SML is not “untyped”, its type-inference oriented. I had  
an adventure with such a thing, needless to say it is unmaintainable with  
an application as soon as it goes beyond 5_000 or 10_000 lines of source  
(Ada is really nicer there and even above, it will keep going nice). But  
this is nice at smaller level, as it is terse, which is mostly welcome  
some time, just like when you are writing down something on a paper.

So my purpose is not to say it is like Ada, not at all: it is different,  
while also formal enough to be usable. It has a different point of view,  
which makes it able to see what an Ada compiler will not see in an  
algorithm, simply because type and constructors are not opaque to each  
others.

What would be the best here, with the possibility of an human error in  
mind ? Abstraction designed in SML (caught the algorithmic design error)  
and implementation design in Ada which is the only one which can handle  
things in the large (and efficiently with sharper designed types) as it is  
unlikely your application will be such a tiny thing.


What about that last episode of “Beyond The Type” ? Did you liked it ?



P.S. I really did have this error while playing with SML-NJ. And when I  
understood what the error standed for and how I could fix it, I said “Was,  
great, I love this waring message”.