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 mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 41E7E81792 for ; Thu, 4 Jul 2013 02:42:40 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of garrigue@math.nagoya-u.ac.jp) identity=pra; client-ip=133.6.130.5; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="garrigue@math.nagoya-u.ac.jp"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of garrigue@math.nagoya-u.ac.jp) identity=mailfrom; client-ip=133.6.130.5; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="garrigue@math.nagoya-u.ac.jp"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mailhost.math.nagoya-u.ac.jp) identity=helo; client-ip=133.6.130.5; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="postmaster@mailhost.math.nagoya-u.ac.jp"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AnABAHfE1FGFBoIFnGdsb2JhbABaxECBHw4BAQEBAQgUCTyCIwEBBScTCQE1Ag4LDgouVwYTGod0qCiERwKFPod/B484MweDBGmJJI4olGUt X-IPAS-Result: AnABAHfE1FGFBoIFnGdsb2JhbABaxECBHw4BAQEBAQgUCTyCIwEBBScTCQE1Ag4LDgouVwYTGod0qCiERwKFPod/B484MweDBGmJJI4olGUt X-IronPort-AV: E=Sophos;i="4.87,992,1363129200"; d="scan'208";a="24501371" Received: from rabbit.math.nagoya-u.ac.jp (HELO mailhost.math.nagoya-u.ac.jp) ([133.6.130.5]) by mail2-smtp-roc.national.inria.fr with ESMTP; 04 Jul 2013 02:42:36 +0200 Received: from mailhost.math.nagoya-u.ac.jp (localhost [127.0.0.1]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id CF68D6391; Thu, 4 Jul 2013 09:42:33 +0900 (JST) Received: from mailhost.math.nagoya-u.ac.jp (localhost [127.0.0.1]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id 64690396F; Thu, 4 Jul 2013 09:42:33 +0900 (JST) DomainKey-Signature: h=Received:Content-Type:Mime-Version:Subject:From:In-Reply-To:Date:Cc:Content-Transfer-Encoding:Message-Id:References:To:X-Mailer; b=; c=nofws; d=math.nagoya-u.ac.jp; q=; s=alpha Received: from garrigue-mini.math.nagoya-u.ac.jp (garrigue-mini.math.nagoya-u.ac.jp [172.16.30.37]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id 58ECE396E; Thu, 4 Jul 2013 09:42:33 +0900 (JST) Content-Type: text/plain; charset=us-ascii Mime-Version: 1.0 (Mac OS X Mail 6.5 \(1508\)) From: Jacques Garrigue In-Reply-To: Date: Thu, 4 Jul 2013 09:42:33 +0900 Cc: OCaml List Content-Transfer-Encoding: quoted-printable Message-Id: <6542400B-3221-4784-8A40-3BA917D451A3@math.nagoya-u.ac.jp> References: <001e01ce77f5$96fd0420$c4f70c60$@metastack.com> To: David Allsopp X-Mailer: Apple Mail (2.1508) Subject: Re: [Caml-list] GADTs + Phantom types On 2013/07/04, at 2:11, David Allsopp wrote: > type (_, _) t =3D A : (bool, [< `Before | `After ]) t > | B : (int, [> `After ]) t > | C : (string, [> `Before ]) t >=20 > 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 t= he >> 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 >=20 > When you say that the type checker can't see that the covariant declarati= on is sound, is it one of those instances from your previous thread where y= ou'd reckoned that the type-checker *could* be altered to see it, but the c= urrent implementation doesn't or is it not possible in general for it to de= tect that kind of declaration? Actually, this coercion shows something else: that your phantom parameter d= oesn't work like a phantom parameter anymore. Now it is a constraint associ= ated with the constructor, and you can change the parameter by copying the = constructor. This may be what you want (it guarantees some invariant), or t= his may be not (all the properties must be expressed by the constraint, oth= erwise they will be lost on copying). As for the soundness, this only comes from the fact the constructors have n= o value arguments, so anything would be sound anyway. And if you allow mark= ing the second parameter as covariant, you would actually get a behavior di= fferent from what to expect: pattern matching (a,b) t against A would only = tell you that b must be a supertype of [< `Before | `After], whose meaning = is not very clear to me. Last, as Gabriel mentioned, GADTs and polymorphic variants do not play very= well together. In particular, incremental refinement is not guaranteed to work as expected. But, if what you want is a combination of GADT and phantom types, you can s= till do it by exporting t as private: module T : sig type (_, +_) t =3D private | A : (bool, _) t | B : (int, _) t | C : (string, _) t val a : (bool, [< `Before | `After]) t val b : (int, [> `After]) t val c : (string, [> `Before]) t end =3D struct type (_, +_) t =3D | A : (bool, _) t | B : (int, _) t | C : (string, _) t let a =3D A let b =3D B let c =3D C end open T let f x =3D (x : (_, [`After]) t :> (_, [>`After]) t) let f1 : type s . (s, _) 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 This way you get GADT refinement for the first parameter, and subtyping for= the second one. Jacques Garrigue=