From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id 459FA7FACB for ; Fri, 22 Aug 2014 21:50:25 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of philippe.veber@gmail.com) identity=pra; client-ip=74.125.82.175; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="philippe.veber@gmail.com"; x-sender="philippe.veber@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of philippe.veber@gmail.com designates 74.125.82.175 as permitted sender) identity=mailfrom; client-ip=74.125.82.175; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="philippe.veber@gmail.com"; x-sender="philippe.veber@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-we0-f175.google.com) identity=helo; client-ip=74.125.82.175; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="philippe.veber@gmail.com"; x-sender="postmaster@mail-we0-f175.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AsYBALSe91NKfVKvm2dsb2JhbABZg2BXBLIjhDSUIIFjh00BgQgIFhABAQEBAQYLCwkUKYQEAQEDARIVGQEbEgsBAwELBgULGiEiAREBBQEKEgYTEhCICwEDCQgNo1lrjR2DEIoTChknAwpmhDMRAQUOjzoEB4RMBYUEBYoKgxGDK4Z6gViRQhgphRE7L4JPAQEB X-IPAS-Result: AsYBALSe91NKfVKvm2dsb2JhbABZg2BXBLIjhDSUIIFjh00BgQgIFhABAQEBAQYLCwkUKYQEAQEDARIVGQEbEgsBAwELBgULGiEiAREBBQEKEgYTEhCICwEDCQgNo1lrjR2DEIoTChknAwpmhDMRAQUOjzoEB4RMBYUEBYoKgxGDK4Z6gViRQhgphRE7L4JPAQEB X-IronPort-AV: E=Sophos;i="5.04,383,1406584800"; d="scan'208";a="75976903" Received: from mail-we0-f175.google.com ([74.125.82.175]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 22 Aug 2014 21:50:06 +0200 Received: by mail-we0-f175.google.com with SMTP id t60so11109203wes.34 for ; Fri, 22 Aug 2014 12:50:06 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type; bh=NTKxZ7qSAurUoENfbOglvF305J2ch50eRl2mq0YoMs4=; b=ZBebqnYPsQtuDFwAbpybFnRNhFszxXjWcBtRzvqyaIGhRKVVVWavoXfB0DR8b/P80z 63XipXl1I4XsfKiC7jwhfB1Es0h4Zv8ktIY9rrEnNg/zIQE0rWNifLxl1jAN1+1ZsuYr UD2Qe8+LDAKYdgucjBS5KZtP/UZ88iNOmXSL4EIGoudDAtoKQykdRPnEXM942xvtvcg3 LkZDLPiKUXvGZcuS7Xy/lv0uymZ58l9rWo54W6xNshIk0g4SL6FFf7qiRynbKWt4d05t AqTc+p2hGCnENSNfDKVWuxYjq/FT6dktBuiS9zr/OST5ej0O5sq8ybMxtUT181SiWuNV J6bQ== X-Received: by 10.194.95.66 with SMTP id di2mr6988476wjb.47.1408737006199; Fri, 22 Aug 2014 12:50:06 -0700 (PDT) MIME-Version: 1.0 Received: by 10.194.166.132 with HTTP; Fri, 22 Aug 2014 12:49:46 -0700 (PDT) In-Reply-To: <83ADBE14262643EA9519BBE719987901@erratique.ch> References: <4060AF3441F149839C46804E64E2B9CE@erratique.ch> <83ADBE14262643EA9519BBE719987901@erratique.ch> From: Philippe Veber Date: Fri, 22 Aug 2014 21:49:46 +0200 Message-ID: To: =?ISO-8859-1?Q?Daniel_B=FCnzli?= Cc: Caml-list Content-Type: multipart/alternative; boundary=047d7bb0498ed6361605013d24b5 X-Validation-by: philippe.veber@gmail.com Subject: Re: [Caml-list] Phantom types and variants --047d7bb0498ed6361605013d24b5 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable Hi Daniel, I really don't see how this could work, since with the definition of coerce: let coerce k v =3D 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 =3D [ `A | `B ] type +'a t constraint 'a =3D [< kind] val a : unit -> [> `A] t val b : unit -> [> `B] t val coerce : ([< kind] as 'a) -> [< kind] t -> 'a t end =3D struct type kind =3D [ `A | `B ] type +'a t =3D { kind : 'a } constraint 'a =3D [< kind] let a () =3D { kind =3D `A } let b () =3D { kind =3D `B } let eq x y =3D match x, y with `A, `A | `B, `B -> true | `A, `B | `B, `A = -> false let coerce k v =3D if eq v.kind k then invalid_arg "" else { v with kind = =3D 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=FCnzli : > Sorry the coerce function type was wrong in my preceding message. Here is > the example: > > ----- > module M : sig > type kind =3D [ `A | `B ] > type +'a t constraint 'a =3D [< kind ] > > val a : unit -> [> `A] t > val b : unit -> [> `B] t > val coerce : ([< kind] as 'a) -> 'b t -> 'a t > end =3D struct > type kind =3D [ `A | `B ] > type +'a t =3D > { kind : kind } > constraint 'a =3D [< kind] > > let a () =3D { kind =3D `A } > let b () =3D { kind =3D `B } > let coerce k v =3D if v.kind <> k then invalid_arg "" else v > end > > let (vl : [`A | `B ] M.t list) =3D [M.a (); M.b ()] > let (v : [`A] M.t) =3D 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 > --047d7bb0498ed6361605013d24b5 Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable
Hi Daniel,

I really don&#= 39;t see how this could work, since with the definition of coerce:

<= span style=3D"font-family:courier new,monospace">let coerce k v =3D if v.ki= nd <> 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
=A0= type kind =3D [ `A | `B ]
=A0 type +'a t constraint 'a =3D [<= ; kind]
=A0 val a : unit -> [> `A] t
=A0 val b : unit -> [&= gt; `B] t
=A0 val coerce : ([< kind] as 'a) -> [< kind] t -> 'a t=
end =3D struct
=A0 type kind =3D [ `A | `B ]
=A0 type +'a t = =3D
=A0=A0=A0 { kind : 'a } constraint 'a =3D [< kind]
=A0 let a () =3D { kind =3D `A }
=A0 let b () =3D { kind =3D `B }
=A0 let eq x y =3D match x, y with `A, = `A | `B, `B -> true | `A, `B | `B, `A -> false
=A0 let coerce k v = =3D if eq v.kind k then invalid_arg "" else { v with kind =3D 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 no= t type with [< ... ] types as its domains. Maybe using GADTs here would = be more appropriate?


Cheers,
=A0 Philippe.



2014-08-22 5:17 GMT+02:00 Daniel B=FCnzli <daniel.buenzli@er= ratique.ch>:
Sorry the coerce function type was wrong in = my preceding message. Here is the example:

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

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

=A0 let a () =3D { kind =3D `A }
=A0 let b () =3D { kind =3D `B }
=A0 let coerce k v =3D if v.kind <> k then invalid_arg "" e= lse v
end

let (vl : [`A | `B ] M.t list) =3D [M.a (); M.b ()]
let (v : [`A] M.t) =3D 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.=A0 Subscription management and archives:
ht= tps://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

--047d7bb0498ed6361605013d24b5--