Re: [Caml-list] Polymorphic variants

[Jacques Garrigue <garrigue@kurims.kyoto-u.ac.jp>]

From: John Max Skaller <skaller@ozemail.com.au>
> Remi VANICAT wrote:
> 
> >John Max Skaller <skaller@ozemail.com.au> writes:
> >
> >>Unfortunately, this doesn't work out as well as I'd expected
> >>because of recursion:
> >>
> >>type a = [`A of a  | `B]
> >>type b = [`A of  b]
> >>
> >>The second type is a subtype of the first,
> >>but this fails:
> >>
> >>let f (x:a) =
> >>match x with
> >>  #b -> ()
> >>
> >>with the message:
> >>
> >>This pattern matches values of type [< b] = [< `A of b]
> >>but is here used to match values of type a = [ `A of a | `B];;
> >>
> >
> >the problem here is that you intended #b is a non fixed matching rule,
> >I mean, imagine you have :
> >
> >`A (`A ( `A ( `A ( `A ( `A `B)))))
> >
> >to check that this is not in #b, one have to look deep in the
> >structure of the value. 
> >
> Yes. But high level programming languages are *meant* to do
> high level things, aren't they?

The only problem is that you're asking for potentially non-terminating
computation to be done during pattern-matching. No, Caml is not
Haskell.
By the way, you can of course do that with a when clause.
Unfortunately, if you want to coerce the value to be a "b", this will
force you to rebuild your value, but anyway you have to access all
leaves of your value before knowing whether it is actually a "b" or
not.
Note that it might be simpler to have most of your functions defined
for "a" rather than for "b", and coerce from "b" to "a":
  (_ : b :> a)
Note the double coercion here, (_ :> a) wouldn't work.

> Here's another example that fails, which is very annoying:
> 
> type a = [`A of e | `B]
> and e = [a  | `C]
> 
> "The type constructor a is not yet completely defined"

But your example is not recursive.
You can just write
  type e = [a | `C]
and it will work fine.

> Almost all interesting cases of variants (for compiler writers anyhow)
> involve type recursion. It shouldn't matter if the type is completely
> defined, only that the definition is finally completed :)

Yes, it matters. Because a variant is a flat type, and the definition
of a variant type depends on the definition of its parts.
Of course it would be possible to do a topological sort to search where
there is no recursion, and remove the recursion automatically.
But this doesn't seem to be the ML approach for values either, and it
wouldn't add any expressive power.

> 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

> >pattern matching only look at the firsts
> >levels of the structure. This must be done otherwise.
> >
> 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.

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

> Now you say that the type information is lost at run time,
> but that is NOT immediately apparent from the documentation.
> Indeed, it need not be the case: the implementation *could*
> mangle the constructor name with the argument type
> so that
> 
>   `A_int
>   `A_float
> 
> are treated as distinct constructors. Then the following:
> 
> fun x = match x with
> | `A a -> ..
> 
> would give an error, since the compiler cannot know
> which `A it is

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.

Sorry, but the feature you are asking for is not polymorphic variants.
This looks more like tree automata types, like they have for XML
typing. This indeed allows for all strange inclusions and unions, but
you can forget about type inference. These are interesting for
themselves, but how to mix them with languages with type inference is
still an open problem.

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

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

> To come back to the examples: the type
> 
> [`A of int | `A of float | `B]
> 
> is perfectly legitimate. The actual error is only on matching.
> If the client never matches on `A, there is no error:
> 
> match x with | `B -> .. | _ -> ...
> 
> this match would be OK, `A isn't refered to.
> It isn't clear why the compiler writer chose to allow
> any argument of `A, but disallows specifying a name for
> a type containing two distinct `A constructors instead
> of simply reporting an ambiguity on use: they're
> called "polymorphic variants" but they aren't actually polymorphic,
> at least in this sense :-)

Polymorphism being a subtle thing...
The polymorphism in variants only describes the fact they can be built
from a bunch of constraints, rather than being defined in advance.

Also, the type you are talking about is

  [< `A of int | `A of float | `B]

which is perfectly legitimate (in the current theory).
You can even name it:

  type 'a t = 'a constraint 'a = [< `A of int | `A of float | `B]

This type being polymorphic, you need to leave a variable to expose
this polymorphism.

On the other hand,
  [`A of int | `A of float | `B]
is the intersection of the above type and
  [> `A of int | `A of float | `B]
This last type is illegal, because you wouldn't be able to match such
a type.

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.

> >it's not type in pattern matching, it's pattern. It is not, at all,
> >the same thing, even if their is link between the two.
> >
> Sure, I know that. (Actually, the sum constructor tags really ARE
> run time type information, they tell which case of the sum
> is represented, and hence the type of the constructor argument)

They tell more: you may have several cases with the same type.

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

Cheers,

Jacques
-------------------
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