Re: [Caml-list] typer strangeness (3.12.0)

[Guillaume Yziquel <guillaume.yziquel@citycable.ch>]

Le Sunday 14 Aug 2011 à 08:19:59 (+0200), rixed@happyleptic.org a écrit :
> Thank you for your answers, but you aimed too high above my
> understanding :-)
> 
> -[ Sat, Aug 06, 2011 at 02:58:49PM +0200, Fabrice Le Fessant ]----
> > The type constraint that you specified does not constraint the
> > polymorphism of the type. To declare a polymorphic constraint, you must
> > use (with OCaml >= 3.12.0) :
> > 
> > let pipe : 'a 'b 'c. ('a, 'b) parzer -> ('c, 'a) parzer -> ('c, 'b) parzer =
> 
> Never saw this notation before. I checked in the manual but beside in
> the language grammar (in the definition of a poly-typexpr) I could find
> more explanation.
> Is it explained somewhere why this notation was required and why this:
> 
> let pipe : ('a, 'b) parzer -> ('c, 'a) parzer -> ('c, 'b) parzer =
> 
> is not enough? What's adding the "'a 'b 'c. " exactly ?

It does explicit universal quantification on the type. So you create a
monomorphic type out of that. \forall 'a. 'a -> 'a is a type for
functions that can be used as int -> int, float -> float, string ->
string, etc...

\forall 'a. 'a -> 'a is not a polymorphic type as 'a is bound.

By contrast, 'a -> 'a is polymorphic in the sense that is does depend on
the 'a to form a monomorphic type.

> I understand
> that it forbids ocaml to consider that the various 'a (for instance) may
> be differents 'a, but I don't understand why ocaml migh do that in the
> first place (especially to produce a _less general_ type than the one
> given) ? If it's not a bug, then what's the purpose ?

Allowing universal quantification of types allows you to have a richer
type system. Such as system F or ML^F. Typical issues it helps to solve
are existential types or polymorphic recursion.

It does more than simply force the various 'a to be distinct. It also
binds them to form a monomorphic type. If you just want the types to be
different, but not bound, you have the (type s) syntax to introduce
types explicitely.

> As for my second question, I received no answer (was: why changing the
> pattern match for something that should be equivalent changes the infered
> type). If you suspect this can be a bug then I can look for a simple
> reproductible case.

It's likely not a bug.

What you did is replace | Fail -> Fail | Wait -> Wait by | x -> x. If
you take into consideration the fact that Fail and Wait are constructors
for a polymorphic type, what you have in the clauses and what is
returned may have different types because you have not unified the type
parameters of this datatype. However, when you write | x -> x, you unify
x and x, and hence unify the type parameters.

That likely explains what you observe.

-- 
     Guillaume Yziquel