Re: [Caml-list] phantom types and identity function

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

On 2012/11/27, at 20:00, Ivan Gotovchits <ivg@ieee.org> wrote:

> 
> Hello,
> 
> These simple signature 
> 
>   module type T = sig
>       type 'a t constraint 'a = [< `A | `B ]
>       val init: [`A] t
>       val f: [`A] t -> [`B] t
>   end
> 
> can be used to constrain the following module
> 
>   module T : T = struct
>       type 'a t = unit constraint 'a = [< `A | `B]
>       let init = ()
>       let f x = x
>   end
> 
> where identity function successfully satisfies the constraint
> 
>   [`A] t -> [`B] t
> 
> but in the following module 
> 
>   module T : T = struct
>       type 'a t = {x:int} constraint 'a = [< `A | `B]
>       let init = {x=0}
>       let f x = x
>   end
> 
> the same identity function doesn't satisfy.

In the first case, a type abbreviation is used.
Since ('a t) expands to (unit), the parameter is completely
ignored, so that you can replace it by anything.

In the second case, you define a concrete type,
so that the parameter is not forgotten.
Note that you cannot even use subtyping for that:
  let f x = (x : [`A] t :> [`B] t)
fails too.
But there is an easy workaround, defining in two steps:
  type u = {x:int}
  type 'a t = u constraint 'a = [< `A | `B]

Jacques Garrigue