Re: [Caml-list] Polymorphic variants

[John Max Skaller <skaller@ozemail.com.au>]

Jacques Garrigue wrote:

>>BTW: I can't write  "t as x" in a type expression. Why not?
>>I'm forced to name it in a type binding .. that means that inductive types,
>>for example, can not be specified anonymously:
>>
>>  [`Cons of list | `Empty] as list
>>
>>should work. [Can I use a 'constraint' here? I've never used
>>a constraint before]
>>
>
>Yes you can. Wasn't it in the tutorial:
>
>    [`Cons of 'list | `Empty] as 'list
>
Argg. Sorry. Of course, I used a plain identifier instead of a type 
variable.

>>It doesn't "must" be done. I think you mean, there are advantages
>>only handling the easy cases: easy to write the compiler,
>>easy to optimise, easy for the end user to monitor
>>code complexity .. and easy for the programmer to handle
>>the more difficult cases manually ..
>>
>
>Not only that: easily understandable properties. This is the most
>important part.
>
Yes, but it is an amorphous thing. The specification
of an 'integer' is easily understandable. Only, the greatest
minds in mathematics struggle to know what a prime
number is.

>>I certainly can write them both:
>>
>>`A 1; `A 1.1;
>>type int_t = [`A of int];
>>type float_t = [`A of float];;
>>
>>No problem doing this. Perhaps there should be.
>>
>
>There is no problem as long as these cases are used independently.
>But you cannot mix them in the same variant type.
>
Yeah, I know .. but it isn't clear from the manual,
perhaps because this very example is not included in it.

>
>How are we going to build a model of [`A of int | `A of float].
>Basically this suppose that we are able to build the union set of
>ints and floats. All the type theory theory of ML is based on the fact
>that there is no such set/type.
>
Not at all. Felix does this, just fine. And I'm no type theorist.
But the algorithms work. I'm not saying ocaml should do
what I did in Felix, but there is no problem at all building
a model, `A is just a function, and in Felix functions
can be overloaded. Including variant constructors.
[These are classic ML style unions, not open ones
like polymorphic variants: they have to be declared
or it wouldn't work]

In Felix, it is fine to duplicate not just constructors,
but any function type:

fun f:x->y = ..
fun f:x->y= ..

No problem. But here:

print (f x);

there is a problem: which f to use?

Is this a good design decision? I don't know: I *could*
report a duplicate definition (and I *do* for duplicate
things other than than functions).

But there is evidence that this IS a good design
decision, it comes from overloading templates
in C++. Since a template basically models a family
of functions, two tempates often model the same
type .. and it would be really silly to ban the templates
because of this. Instead, an error is reported only
when a particular instantiation is ambiguous.

I'm not criticizing the decisions made for polymorphic
variants, just pointing out that a lot of alternatives
do exist, and it would be useful to see an explanation
of why the various interesting nasty cases are
handled the way they are.

>
>What this basically means is that any use of `A without type
>annotation should generate an error. The whole point of polymorphic
>variants being that they are independent from definitions, I really
>cannot follow you here.
>
Nor I you. When the compiler sees:

    `A 1

in an expression then it silently replaces it with


    `A_int 1

so that the actual constructor name is distinct for every argument type.
This is called 'name mangling' and C++ compilers do it all the time
to every external function symbol in a program.

In a pattern match, there is a problem because the mangling
cannot be done when the expression being decoded
is of a type with two constructor of the same unmangled name.
So in this case ONLY, the client must disambiguate by
specifying which type is meant:

    `A (x:int)


is replaced by

  `A_int x

>
>Sorry, but the feature you are asking for is not polymorphic variants.
>

I am NOT asking for it. I am merely critiquing it from the point
of view of a user. Remember, I am using them: the whole of my
compiler uses polymorphic variants extensively and almost
exclusively (only a few of the traditional sum types remain
in a couple of places because there is no point replacing them).
So you could say I'm a fairly heavy user of them :-)

>>Things "must be so" if they are a consequence of theory, but it
>>isn't always evident which theory is used, and why that one is best
>>:-)
>>
>
>Read the papers :-)
>There is a whole literature about lambda-calculus, type systems,
>models...
>One trouble is that it is hard to explain all this theory in a few
>lines.
>
And the other is that there are a LOT of theories.

Furthermore, the theory upon which an implementation
is based doesn't determine all the technical design decisions:
like, for example, whether to report that a type with duplicate
constructors is an error even if it isn't used, or whether
to defer the error to the point of use .. and provide a disambiguation
mechanism.

C++ for example, adopts BOTH of these philosophies in different
places, which is one reason it is a mess.

>>Perhaps one consequence of this is that the documentation
>>needs to be more specific and have more examples:
>>the author knowing the chosen theory and implementation
>>believes only lightweight coverage is necessary, not seeing
>>the many alternatives someone less involved might.
>>
>
>You're probably right. But your remark also describes the basic
>problem: as long as the author is the only one to document a feature,
>his description will only be partial.
>
So add in the example I gave? I can't do that, I don't have access to the
document source. But I have 'documented' it in the email :-)

>
>Note that one could think of ways to make the above legal, using
>intersection rather than union, but I don't see how it would be
>useful, because you would have no way to access the value anyway.
>Like throwing data into a black hole.
>
The pragmatics of programming often require useless things.
For example, unreachable code .. because the programmer
has commented something out. Empty types (why was []
removed??) because they're yet to be filled in with cases,
but we want to name the type anyhow, perhaps to write
a function signature ..

The unit type. It is theoretically useless in a (purely) functional
programming language. Why is it there?

>>Well, having looked at the English translation of the 
>>Ocaml book by Emmanuel Chailloux, Pascal
>>Manoury and Bruno Pagano, I think a big hole is going
>>to be plugged. This book covers quite advanced topics,
>>I might learn something here!
>>
>
>This is indeed a nice book, but written before the introduction of
>polymorphic variants. So almost nothing about them in it.
>
>Actually, this is one reason I would want to say: now polymorphic
>variants are finished, let's work with them, and try to describe what
>they can do. This is too hard to do that on a moving target.
>

Well, I'm doing my part: I'm using them all the time,
and I'm relating my experience so you can get some feeling
for how someone else views them that is. I was hoping
to get much stronger static typing using them. In fact,
I have better typing, but nowhere near as strong as I
either expected initially, or would like.

Some of the typing I'd like is plain impossible.
And some is inconvenient to implement, or too quirky
to bother with. And some is desirable but not implemented
or not understood. And I don't really know the distinction
between all these cases.

-- 
John Max Skaller, mailto:skaller@ozemail.com.au
snail:10/1 Toxteth Rd, Glebe, NSW 2037, Australia.
voice:61-2-9660-0850




-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners