Re: Phantom types

[Dawid Toton <d0@wp.pl>]

> type 'a t = {l: float}
>
> Any thoughts ?

I think the crucial question is when new record types are born. Here is
my opinion:

The "=" sign in the above type mapping definition is what I would call
"delayed binding". "Early binding" would be equivalent to

type tmp = {lab : float}
type 'a s = tmp

(evaluate the right-hand side first, then define the mapping).

The "early binding" creates only one record type, so lab becomes
ordinary record label.
In the given example of the "delayed binding" the t becomes a machine
producing new record types.
Hence, the identifier l is not an ordinary record label. It is shared by
whole family of record types. We can see it this way:

# type 'a t = { la : float } ;;
type 'a t = { la : float; }
# {la = 0.};;
- : 'a t = {la = 0.}

So OCaml interpreter doesn't know the exact type of the last expression,
but it is clever enough to give it a generalized type.
We can use la to construct records of incompatible types:

# type 'a t = { la : float } ;;
type 'a t = { la : float; }
# let yy = ({la = 0.} : int t) ;;
val yy : int t = {la = 0.}
# let xx = ({la = 0.} : string t);;
val xx : string t = {la = 0.}
# xx = yy;;
Error: This expression has type int t but an expression was expected of type
         string t


I suppose my jargon may be not mainstream, apologies.

Dawid