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 3253181792 for ; Wed, 3 Jul 2013 19:11:10 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of dra-news@metastack.com) identity=pra; client-ip=81.103.221.48; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="dra-news@metastack.com"; x-sender="dra-news@metastack.com"; x-conformance=sidf_compatible Received-SPF: Neutral (mail3-smtp-sop.national.inria.fr: domain of dra-news@metastack.com does not assert whether or not 81.103.221.48 is permitted sender) identity=mailfrom; client-ip=81.103.221.48; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="dra-news@metastack.com"; x-sender="dra-news@metastack.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@mtaout02-winn.ispmail.ntl.com) identity=helo; client-ip=81.103.221.48; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="dra-news@metastack.com"; x-sender="postmaster@mtaout02-winn.ispmail.ntl.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ap4AANlZ1FFRZ90wlGdsb2JhbABagmiBHMA1gQQWDgEBAQEHDQkJFAMlgiMBAQEDAScTRAsCAQgYChQQMiUBAQQbiAEHA7sAjzo4gwRpA5dJlFaCKA X-IPAS-Result: Ap4AANlZ1FFRZ90wlGdsb2JhbABagmiBHMA1gQQWDgEBAQEHDQkJFAMlgiMBAQEDAScTRAsCAQgYChQQMiUBAQQbiAEHA7sAjzo4gwRpA5dJlFaCKA X-IronPort-AV: E=Sophos;i="4.87,989,1363129200"; d="scan'208";a="19903571" Received: from mtaout02-winn.ispmail.ntl.com ([81.103.221.48]) by mail3-smtp-sop.national.inria.fr with ESMTP; 03 Jul 2013 19:11:09 +0200 Received: from aamtaout03-winn.ispmail.ntl.com ([81.103.221.35]) by mtaout02-winn.ispmail.ntl.com (InterMail vM.7.08.04.00 201-2186-134-20080326) with ESMTP id <20130703171108.HEQX23282.mtaout02-winn.ispmail.ntl.com@aamtaout03-winn.ispmail.ntl.com> for ; Wed, 3 Jul 2013 18:11:08 +0100 Received: from romulus.metastack.com ([81.102.132.77]) by aamtaout03-winn.ispmail.ntl.com (InterMail vG.3.00.04.00 201-2196-133-20080908) with ESMTP id <20130703171108.VIPO2660.aamtaout03-winn.ispmail.ntl.com@romulus.metastack.com> for ; Wed, 3 Jul 2013 18:11:08 +0100 Received: from remus.metastack.local (remus.metastack.com [172.16.0.1]) by romulus.metastack.com (8.14.2/8.14.2) with ESMTP id r63HB5Fc021597 (version=TLSv1/SSLv3 cipher=AES128-SHA bits=128 verify=FAIL) for ; Wed, 3 Jul 2013 18:11:05 +0100 Received: from Remus.metastack.local ([fe80::547c:3c42:e1da:eda2]) by Remus.metastack.local ([fe80::547c:3c42:e1da:eda2%10]) with mapi id 14.03.0123.003; Wed, 3 Jul 2013 18:11:04 +0100 From: David Allsopp To: OCaml List Thread-Topic: [Caml-list] GADTs + Phantom types Thread-Index: Ac538btJ44hnvAi5QEOKAKixuCTEvwAAhvSAAAKcd7A= Date: Wed, 3 Jul 2013 17:11:02 +0000 Message-ID: References: <001e01ce77f5$96fd0420$c4f70c60$@metastack.com> In-Reply-To: Accept-Language: en-GB, en-US Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: x-originating-ip: [172.16.0.18] Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 Organization: MetaStack Solutions Ltd. X-Scanned-By: MIMEDefang 2.65 on 172.16.0.20 X-Cloudmark-Analysis: v=1.1 cv=AUhbpHVS+xhHrj9wLCYAQoYnFLYUZdbP8UM0GmH2jwk= c=1 sm=0 a=IXlcok0kcmcA:10 a=XN9IVK3gdqcA:10 a=cTs9vV391PwA:10 a=kj9zAlcOel0A:10 a=xqWC_Br6kY4A:10 a=O5odOB4xYAatkDFxeQAA:9 a=CjuIK1q_8ugA:10 a=HpAAvcLHHh0Zw7uRqdWCyQ==:117 Subject: RE: [Caml-list] GADTs + Phantom types Thanks for looking at this... Gabriel Scherer wrote: > In fact, you can write a coercion function by hand (because in fact it is > sound to declare the parameter covariant in your type-declaration, but the > type-checker doesn't see that): >=20 > # let coerce : type a . (a, [ `Before ]) t -> (a, [ `Before | `After > ]) t =3D function A -> A | C -> C;; > val coerce : ('a, [ `Before ]) t -> ('a, [ `After | `Before ]) t =3D The problem with that in my actual use case the type is buried inside a lis= t - so that effectively requires the list to be copied just to coerce each = value to the other type. There are also a large number of constructors and = other options in addition to `Before and `After! It's a lot of code just fo= r a type coercion... When you say that the type checker can't see that the covariant declaration= is sound, is it one of those instances from your previous thread where you= 'd reckoned that the type-checker *could* be altered to see it, but the cur= rent implementation doesn't or is it not possible in general for it to dete= ct that kind of declaration? > I personally try to avoid using polymorphic variants as phantom types when > I use GADTs. The two features are subtle enough in isolation to become a > potential nightmare when put together. Actually, I think that's the best lesson here, thanks! :o) While the initia= l functions are straightforward, it seems complexity is always lurking arou= nd the corner as soon as you try to combine them. > Given that GADTs allow a cleaner > approach than phantom types, I would encourage you to try GADT-using, > polymorphic-variant-free approaches. >=20 > (Of course that doesn't negate the usefulness of polymorphic variants when > actually used as values, instead of weird type-level stuff only.) >=20 > type tag_b =3D TagB > type tag_a =3D TagA > type tag_c =3D TagC >=20 > type (_, _) t =3D > | A : (bool, tag_a) t > | B : (int, tag_b) t > | C : (string, tag_c) t >=20 > type _ before =3D > | BA : tag_a before > | BC : tag_c before >=20 > type _ after =3D > | AA : tag_a after > | AB : tag_b after >=20 > let f1 : type s tag . (s, tag) t * s -> unit =3D function > | A, b -> if b then () > | B, i -> if i =3D 0 then () > | C, s -> if s =3D "" then () >=20 > let f2 : type s tag . tag before * (s, tag) t * s -> string =3D function > | BA, A, b -> string_of_bool b > | BC, C, s -> s I don't follow here the equivalence to my original example - this requires = that BA or BC in the call which kind of negates the point that all of the c= hecking is embedded in the type system. However, what it did show me was th= at I was missing an obvious trick to allow for tagging both `Before and `Af= ter which is to have the tags: type 'a connect type before =3D A type after =3D B and then the GADT can be written: type (_, _) t =3D A : (bool, _ connect) t | B : (int, after connect) t | C : (string, before connect) t and then with a few more type variables in [f1] and [f2] you can have: let f1 : type s a . (s, a connect) t -> s -> unit =3D fun attr value -> match attr with A -> Printf.printf "Bool given: %b\n" value | B -> Printf.printf "Int given: %d\n" value | C -> Printf.printf "String given: %S\n" value let f2 : type s . (s, before connect) t -> s -> unit =3D fun attr value -> f1 attr value David