Re: polymorphic variant oddity

[Pierre Weis <Pierre.Weis@inria.fr>]

Julian Assange played with polymorphic variants:

> let `F x = x;;   
> Unbound value x
> # let `F x = 1;;
> This expression has type int but is here used with type [< `F of 'a | ..]
> # let `F x = `F 1;;
> val x : int = 1
> # `F 4;;
> - : [> `F of int] = `F 4
> 
> What exactly is the meaning this?

This is not specific to polymorphic variants, you may observe the same
behaviour with regular concrete data types. Since, it is simpler with
usual types and constructors, let's explain with a simple type with F
as single constructor:

type 'a t = F of 'a;;

# let F x = x;;
            ^
Unbound value x

Explanation: when defining let pattern = expr, the compiler
verifies that the expr can be computed; it is not the case here, since
x is unknown (as not been previously defined). Is there something
surprising here ?

# let F x = 1;;
            ^
This expression has type int but is here used with type 'a t

When writing let pattern = expr with a complex pattern such that F x,
your using a ``destructuring let'', which means that the value of expr
will be matched against pattern, and the variables in pattern will be
bound to the corresponding parts in (the computed value of)
expr. Hence expr should have the same type as pattern. Hence the type
checking error since F x has type 'a t and 1 has type int.

# let F x = F 1;;
val x : int = 1

One successful destructurig let, that bounds x (the variable of the
left-hand pattern) to 1 (the value corresponding to that variable in
the right-hand expression).

# F 4;;
- : int t = F 4

Nothing strange: we just build a value of type t.

Is there some more magic to explain ?

Pierre Weis

INRIA, Projet Cristal, Pierre.Weis@inria.fr, http://cristal.inria.fr/~weis/