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 9EAF881792 for ; Wed, 3 Jul 2013 15:58:33 +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: Ap0AAFMt1FFRZ90wlGdsb2JhbABagzvBfRYOAQEBAQcNCQkUAyWCKggCHQESMRsFFlIjHAEEHgWIAwiaZKATBJNfA452nSo X-IPAS-Result: Ap0AAFMt1FFRZ90wlGdsb2JhbABagzvBfRYOAQEBAQcNCQkUAyWCKggCHQESMRsFFlIjHAEEHgWIAwiaZKATBJNfA452nSo X-IronPort-AV: E=Sophos;i="4.87,988,1363129200"; d="scan'208";a="19879801" Received: from mtaout02-winn.ispmail.ntl.com ([81.103.221.48]) by mail3-smtp-sop.national.inria.fr with ESMTP; 03 Jul 2013 15:58:32 +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 <20130703135831.FHNX23282.mtaout02-winn.ispmail.ntl.com@aamtaout03-winn.ispmail.ntl.com> for ; Wed, 3 Jul 2013 14:58:31 +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 <20130703135831.TRYW2660.aamtaout03-winn.ispmail.ntl.com@romulus.metastack.com> for ; Wed, 3 Jul 2013 14:58:31 +0100 Received: from Altus ([172.16.0.18]) (authenticated bits=0) by romulus.metastack.com (8.14.2/8.14.2) with ESMTP id r63DwTMc018269 (version=TLSv1/SSLv3 cipher=AES128-SHA bits=128 verify=NO) for ; Wed, 3 Jul 2013 14:58:29 +0100 From: "David Allsopp" To: "OCaml List" Date: Wed, 3 Jul 2013 14:59:52 +0100 Organization: MetaStack Solutions Ltd. Message-ID: <001e01ce77f5$96fd0420$c4f70c60$@metastack.com> MIME-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: 7bit X-Mailer: Microsoft Outlook 14.0 Thread-Index: Ac538btJ44hnvAi5QEOKAKixuCTEvw== Content-Language: en-gb 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=cTs9vV391PwA:10 a=RQQLJnld3ZcA:10 a=kj9zAlcOel0A:10 a=ZOzjf2MOAAAA:8 a=IBYVIjbgvryRn6KnClgA:9 a=CjuIK1q_8ugA:10 a=HpAAvcLHHh0Zw7uRqdWCyQ==:117 Subject: [Caml-list] GADTs + Phantom types 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