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 EC33F817AF for ; Wed, 3 Jul 2013 16:48:02 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of gabriel.scherer@gmail.com) identity=pra; client-ip=209.85.214.41; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of gabriel.scherer@gmail.com designates 209.85.214.41 as permitted sender) identity=mailfrom; client-ip=209.85.214.41; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-bk0-f41.google.com) identity=helo; client-ip=209.85.214.41; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="postmaster@mail-bk0-f41.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AiQBAIs41FHRVdYpjmdsb2JhbABagztJrheSG3sIFg4BAQEBBw0JCRIGJIIjAQEFJxkBGw8DCwEDDAYFCwMKDSEiAREBBQEKEgYTEgiHYgEDDwyda4xNgn+EJQoZJwMKWId0AQUMj18Hg20Dl0mBKY43FimEOTo X-IPAS-Result: AiQBAIs41FHRVdYpjmdsb2JhbABagztJrheSG3sIFg4BAQEBBw0JCRIGJIIjAQEFJxkBGw8DCwEDDAYFCwMKDSEiAREBBQEKEgYTEgiHYgEDDwyda4xNgn+EJQoZJwMKWId0AQUMj18Hg20Dl0mBKY43FimEOTo X-IronPort-AV: E=Sophos;i="4.87,988,1363129200"; d="scan'208";a="24448038" Received: from mail-bk0-f41.google.com ([209.85.214.41]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 03 Jul 2013 16:48:02 +0200 Received: by mail-bk0-f41.google.com with SMTP id jc3so128262bkc.0 for ; Wed, 03 Jul 2013 07:48:02 -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=AMpryHrW2LmXRdbfPCeMYkm8HbngcmpgxSBH3Y8g6ww=; b=OM3+oYbbesfJVeBUDUsV+cyqVa55NbPrhkNp4uJ9gvtsY/VxC9vWXOc+nxFWLzY7Fv eHnVmEqcZ5c7w0UBBBikzOkUXxdoJE5Jal/1AsWdHfnE8Al/7ZwethR3IQdqd3piOQfm 5GbhoKJAW5ZJntA2huNDe1oV2dBx4zsTej++4ayrFSyIDRu4Qpyy0IQhnQcPHQnoERMK C8J0MmFynzfWMNvqZX0cIReSPBwvNJGWsQPOB66K7mD91vGA66K0gfyY9OMcdaWXeXRG IpKbA7X5csw8f9c9Z1tl7rStSlWZ6om7/4seUfhHu29WjLt0o4Sh8WbwYvuk/WJ8RDDl hxOw== X-Received: by 10.204.76.141 with SMTP id c13mr226053bkk.42.1372862882127; Wed, 03 Jul 2013 07:48:02 -0700 (PDT) MIME-Version: 1.0 Received: by 10.204.20.131 with HTTP; Wed, 3 Jul 2013 07:47:21 -0700 (PDT) In-Reply-To: <001e01ce77f5$96fd0420$c4f70c60$@metastack.com> References: <001e01ce77f5$96fd0420$c4f70c60$@metastack.com> From: Gabriel Scherer Date: Wed, 3 Jul 2013 16:47:21 +0200 Message-ID: To: David Allsopp Cc: OCaml List Content-Type: text/plain; charset=ISO-8859-1 Subject: Re: [Caml-list] GADTs + Phantom types 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): # let coerce : type a . (a, [ `Before ]) t -> (a, [ `Before | `After ]) t = function A -> A | C -> C;; val coerce : ('a, [ `Before ]) t -> ('a, [ `After | `Before ]) t = 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. Given that GADTs allow a cleaner approach than phantom types, I would encourage you to try GADT-using, polymorphic-variant-free approaches. (Of course that doesn't negate the usefulness of polymorphic variants when actually used as values, instead of weird type-level stuff only.) type tag_b = TagB type tag_a = TagA type tag_c = TagC type (_, _) t = | A : (bool, tag_a) t | B : (int, tag_b) t | C : (string, tag_c) t type _ before = | BA : tag_a before | BC : tag_c before type _ after = | AA : tag_a after | AB : tag_b after let f1 : type s tag . (s, tag) t * s -> unit = function | A, b -> if b then () | B, i -> if i = 0 then () | C, s -> if s = "" then () let f2 : type s tag . tag before * (s, tag) t * s -> string = function | BA, A, b -> string_of_bool b | BC, C, s -> s On Wed, Jul 3, 2013 at 3:59 PM, David Allsopp wrote: > The premise here is that I've been trying to use polymorphic variants as > phantom types to create subsets of a GADT for certain function calls. It's > working fine - in fact, it's really quite elegant being able to have a GADT > listing a whole load of properties and being able to tag each one as > read-only, write-only or read+write and then have the type checker able to > report whether the wrong constructor is passed to a [get] or [set] function. > > The snag is that I've hit a problem when composing these functions - say > trying to call a function that accepts all the constructors using a > parameter which is restricted to a subset of them. > > I've tried to play with a few simplified versions to understand the problem > and perhaps be able to explain it in a small example. My first attempt > (without GADTs) looks like this. I define an abstract type T.t allowing me > to tag integer values: > > module T : > sig > type +'a t > val create : int -> 'a t > val get : 'a t -> int > end = > struct > type 'a t = int > let create x = x > let get x = x > end > > I then define a function f1: > > let f1 : [ `After | `Before ] T.t -> unit = > fun value -> Printf.printf "Value given: %d\n" (T.get value) > > and can pass values to it: > > let (dummy : [> `After ] T.t) = T.create 42 > in > f1 dummy > > Furthermore, because of the variance annotation, I can define a function f2: > > let f2 : [ `After ] T.t -> unit = > f1 (param : [ `After ] T.t :> [> `After ] T.t) > > which allows me to have f2 accepting [ `After ] T.t only but still using f1 > (which accepts [ `After ] T.t, [ `Before ] T.t and [ `After | `Before ] T.t > values) as a utility function. > > So then I tried applying this to my original problem with GADTs: > > type (_, _) t = A : (bool, [< `Before | `After ]) t > | B : (int, [> `After ]) t > | C : (string, [> `Before ]) t > > let f1 : type s . (s, [ `After | `Before ]) t -> s -> unit = 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 ]) t -> s -> unit = fun attr value -> > f1 attr value > > As this code stands, I get a typing error in [f2] because [attr] does not > allow the constructor [ `After ] so it's not a valid parameter for [f1]. > > So, having scratched my head for a bit as to why (s, [ `Before ]) t was not > a subtype of (s, [ `After | `Before ]) t I remembered variance annotations > and tried changing [t] to be: > > type (_, +_) t = ... > > But the type checker said "In this GADT definition, the variance of some > parameter cannot be checked". > > At which point, rather out my depth, I felt thoroughly morose and deflated > and decided it was time to ask the lovely type experts on this list whether > I'm just being stupid or whether what I'm trying to do is in fact > impossible. > > I'd tried not using polymorphic variants as the phantom type, but the > problem is that unlike the classic "readonly/readwrite" example, these > things may readonly, writeonly or readwrite and I couldn't see how you could > code that requirement without using polymorphic variants. I also came across > this thread https://sympa.inria.fr/sympa/arc/caml-list/2012-02/msg00059.html > from last year which means I think I understand why I'm getting that > variance error message - what I couldn't tell is whether the proposed > changes would make the above type work or not. > > > David > > > -- > 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