[Caml-list] Phantom types and variants

[Caml-list] Phantom types and variants

[Daniel Bünzli]

Hello,  

I'm pretty sure I have used the following pattern in the past. But the `coerce` function doesn't type. It's quite strange since the type variable is a phantom type so it should not enforce anything. Any hints ? 

--------
module M : sig
  type kind = [ `A | `B ]
  type +'a t constraint 'a = [< kind ]

  val a : unit -> [> `A] t
  val b : unit -> [> `B] t
  val coerce : ([> kind] as 'a) -> 'b t -> 'a t
end = struct                                                                                         
  type kind = [ `A | `B ]                                                                            
  type +'a t =                                                                                       
    { kind : kind }                                                                                  
    constraint 'a = [< kind]                                                                         
                                                                                                     
  let a () = { kind = `A }                                                                           
  let b () = { kind = `B }                                                                           
  let coerce k v = if v.kind <> k then invalid_arg "" else v                                         
end


let (vl : [`A | `B ] M.t list) = [M.a (); M.b ()]
let (v : [`A] M.t) = M.coerce `A (List.hd vl)


--------

Fails with:

Values do not match:
val coerce : kind -> ([< kind ] as 'a) t -> 'a t
is not included in
val coerce : kind -> [< kind ] t -> kind t



Best,

Daniel 

Re: [Caml-list] Phantom types and variants

[Daniel Bünzli]

Sorry the coerce function type was wrong in my preceding message. Here is the example: 

-----
module M : sig
  type kind = [ `A | `B ]
  type +'a t constraint 'a = [< kind ]

  val a : unit -> [> `A] t
  val b : unit -> [> `B] t
  val coerce : ([< kind] as 'a) -> 'b t -> 'a t
end = struct
  type kind = [ `A | `B ]
  type +'a t =
    { kind : kind }
    constraint 'a = [< kind]

  let a () = { kind = `A }
  let b () = { kind = `B }
  let coerce k v = if v.kind <> k then invalid_arg "" else v
end

let (vl : [`A | `B ] M.t list) = [M.a (); M.b ()]
let (v : [`A] M.t) = M.coerce `A (List.hd vl)

------

and the error:

Values do not match:
val coerce : kind -> ([< kind ] as 'a) t -> 'a t
is not included in
val coerce : ([< kind ] as 'a) -> [< kind ] t -> 'a t

Re: [Caml-list] Phantom types and variants

[Philippe Veber]

[-- Attachment #1: Type: text/plain, Size: 2374 bytes --]

Hi Daniel,

I really don't see how this could work, since with the definition of coerce:

let coerce k v = if v.kind <> k then invalid_arg "" else v

the expressions [v] and [coerce k v] must have the same type. So the type
of [coerce] necessarily is of the form [kind -> 'a t -> 'a t]. You'd have
to return a [t] made from [k] instead to capture its type. Here is another
proposal:

module M : sig
  type kind = [ `A | `B ]
  type +'a t constraint 'a = [< kind]
  val a : unit -> [> `A] t
  val b : unit -> [> `B] t
  val coerce : ([< kind] as 'a) -> [< kind] t -> 'a t
end = struct
  type kind = [ `A | `B ]
  type +'a t =
    { kind : 'a } constraint 'a = [< kind]

  let a () = { kind = `A }
  let b () = { kind = `B }
  let eq x y = match x, y with `A, `A | `B, `B -> true | `A, `B | `B, `A ->
false
  let coerce k v = if eq v.kind k then invalid_arg "" else { v with kind =
k }
end

Not sure though, that this can be used in practice because of the [eq]
function: you can't write it with a catch-all case otherwise it does not
type with [< ... ] types as its domains. Maybe using GADTs here would be
more appropriate?


Cheers,
  Philippe.



2014-08-22 5:17 GMT+02:00 Daniel Bünzli <daniel.buenzli@erratique.ch>:

> Sorry the coerce function type was wrong in my preceding message. Here is
> the example:
>
> -----
> module M : sig
>   type kind = [ `A | `B ]
>   type +'a t constraint 'a = [< kind ]
>
>   val a : unit -> [> `A] t
>   val b : unit -> [> `B] t
>   val coerce : ([< kind] as 'a) -> 'b t -> 'a t
> end = struct
>   type kind = [ `A | `B ]
>   type +'a t =
>     { kind : kind }
>     constraint 'a = [< kind]
>
>   let a () = { kind = `A }
>   let b () = { kind = `B }
>   let coerce k v = if v.kind <> k then invalid_arg "" else v
> end
>
> let (vl : [`A | `B ] M.t list) = [M.a (); M.b ()]
> let (v : [`A] M.t) = M.coerce `A (List.hd vl)
>
> ------
>
> and the error:
>
> Values do not match:
> val coerce : kind -> ([< kind ] as 'a) t -> 'a t
> is not included in
> val coerce : ([< kind ] as 'a) -> [< kind ] t -> 'a t
>
>
>
>
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa.inria.fr/sympa/arc/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>

[-- Attachment #2: Type: text/html, Size: 3571 bytes --]

Re: [Caml-list] Phantom types and variants

[Daniel Bünzli]

Le vendredi, 22 août 2014 à 20:49, Philippe Veber a écrit :
> Here is another proposal:

Thanks Philippe. I also thought about this solution but I wanted to avoid the new allocation. Note that you can actually write that solution without having to write that eq function. This makes the trick:

let coerce kind v = match kind with
| kind when (kind :> kind) = (v.kind :> kind) -> { v with kind = kind }
| _ -> invalid_arg ""


Pierre Chambart also responded to me privately (thanks), suggesting that I do not try to use variants themselves as the coercion specification but another more structured value. His solution (at the end of this email) works. But since I'm a little bit stubborn and that I would really like to use the variant for the coercion specification I tried to adapt its solution as follows. But it fails with a type error that I fail to understand:

Error: This definition has type ([< kind ] as 'a) -> 'a t
which is less general than 'b. ([< kind ] as 'b) -> 'b t



-------------
module M : sig
  type kind = [ `A | `B ]
  type +'a t constraint 'a = [< kind ]
  val a : unit -> [> `A] t
  val b : unit -> [> `B] t
  val coerce : ([< kind] as 'a) -> 'b t -> 'a t
end = struct
  type kind = [ `A | `B ]

  type +'a t =
    { kind : kind;
      coerce : 'b. ([< kind] as 'b) -> 'b t }
    constraint 'a = [< kind ]

  let a () =
    let rec v = { kind = `A; coerce }
    and coerce : 'b. ([< kind] as 'b) -> 'b t = function
    | `A -> v | `B -> invalid_arg ""
    in
    v

  let b () =
    let rec v = { kind = `B; coerce }
    and coerce : 'b. ([< kind] as 'b) ->'b t = function
    | `A -> v | `B -> invalid_arg ""
    in
    v

  let coerce kind v = v.coerce kind
end

-----------

Any hints ?  

Best,

Daniel

Pierre Chambart's solution:

module M : sig
  type kind = [ `A | `B ]
  type +'a t constraint 'a = [< kind ]
  type 'a coercer constraint 'a = [< kind]
                                   
  val a : unit -> [> `A] t
  val b : unit -> [> `B] t       

  val ac : [`A] coercer
  val coerce : 'a coercer -> 'b t -> 'a t       
end = struct
  type kind = [ `A | `B ]
  type +'a t =
    { kind : kind }
    constraint 'a = [< kind]
                     
  type 'a coercer =
    { f : 'b. 'b t -> 'a t option }
    constraint 'a = [< kind]
                 
  let a () = { kind = `A }
  let b () = { kind = `B }
              
  let ac = { f = (function ({ kind = `A } as v) -> Some v
                         | _ -> None) }
     
  let coerce k v =
    match k.f v with
    | None -> invalid_arg ""
    | Some v -> v
end

Re: [Caml-list] Phantom types and variants

[Jeremy Yallop]

On 22 August 2014 04:17, Daniel Bünzli <daniel.buenzli@erratique.ch> wrote:
> Sorry the coerce function type was wrong in my preceding message. Here is the example:
>
> -----
> module M : sig
>   type kind = [ `A | `B ]
>   type +'a t constraint 'a = [< kind ]
>
>   val a : unit -> [> `A] t
>   val b : unit -> [> `B] t
>   val coerce : ([< kind] as 'a) -> 'b t -> 'a t
> end = struct
>   type kind = [ `A | `B ]
>   type +'a t =
>     { kind : kind }
>     constraint 'a = [< kind]
>
>   let a () = { kind = `A }
>   let b () = { kind = `B }
>   let coerce k v = if v.kind <> k then invalid_arg "" else v
> end

The following definition does the trick (and avoids the allocation):

  let coerce (#kind as k) ({kind} as v) = if v.kind <> k then
invalid_arg "" else v

Re: [Caml-list] Phantom types and variants

[Daniel Bünzli]

Le samedi, 23 août 2014 à 16:40, Jeremy Yallop a écrit :
> let coerce (#kind as k) ({kind} as v) = if v.kind <> k then
> invalid_arg "" else v

Wonderful. Thanks !  

Daniel