Re: [Caml-list] Phantom types and variants

[Philippe Veber <philippe.veber@gmail.com>]

[-- 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 --]