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 mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by sympa.inria.fr (Postfix) with ESMTPS id 9C0A67EE0C for ; Wed, 28 Nov 2012 09:13:17 +0100 (CET) Received-SPF: None (mail1-smtp-roc.national.inria.fr: no sender authenticity information available from domain of gabriel.scherer@gmail.com) identity=pra; client-ip=209.85.223.182; receiver=mail1-smtp-roc.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail1-smtp-roc.national.inria.fr: domain of gabriel.scherer@gmail.com designates 209.85.223.182 as permitted sender) identity=mailfrom; client-ip=209.85.223.182; receiver=mail1-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 (mail1-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-ie0-f182.google.com) identity=helo; client-ip=209.85.223.182; receiver=mail1-smtp-roc.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="postmaster@mail-ie0-f182.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AkUBAPnGtVDRVd+2mGdsb2JhbAA8CcAcCBYOAQEBAQEICQ0HFCeCHgEBBUABGxYHAQMMBgULAwouIgERAQUBHAYTh3oBAw+gLIwzgnqEdAoZJw1ZiHUBBQyMLhKELwOWAY5kFimEEg X-IronPort-AV: E=Sophos;i="4.84,177,1355094000"; d="scan'208";a="183563131" Received: from mail-ie0-f182.google.com ([209.85.223.182]) by mail1-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 28 Nov 2012 09:13:16 +0100 Received: by mail-ie0-f182.google.com with SMTP id s9so22934875iec.27 for ; Wed, 28 Nov 2012 00:13:16 -0800 (PST) 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=tHk+0CvN9PiZAjVho+/xJnV+jBD1hSbDuc5cmMWoQ8Q=; b=rvEM0WFPj7nEBw+3nyWVhevuHUUwtjNcesUv0pJciB32M1LcvtJ97TaBDojXLfcUZj VuwKc5R9RmaIEtOvTBGblW6fhr+Np82I0OZLJwKnt0k5G5ub+oy5plh1V9IUNagC8dU2 HmngAUXWuglbM5fZT16XJRrJ0mq2A4oCex8laJH2UpDTeJRa1K9LvoJ+3xkcsni9aFzW tAnEXwyDxFR448aBSvFHxscD5jUqcBkF13oG5qvicu2EfK284KE8c3TM9r+YVsPrr7Fo r5evD+ypaM7q1/HnDenx+rohFGWedEmx5WeYx9+Yya34cjcdAU3hz2jj8Zu8V/1Rwf4R f89g== Received: by 10.42.138.74 with SMTP id b10mr16216813icu.33.1354090395952; Wed, 28 Nov 2012 00:13:15 -0800 (PST) MIME-Version: 1.0 Received: by 10.50.184.199 with HTTP; Wed, 28 Nov 2012 00:12:35 -0800 (PST) In-Reply-To: <87fw3uxuja.fsf@golf.niidar.ru> References: <87ip8rwbsc.fsf@golf.niidar.ru> <1F656500-76AC-482F-BA08-A9BB8250D904@math.nagoya-u.ac.jp> <87fw3uxuja.fsf@golf.niidar.ru> From: Gabriel Scherer Date: Wed, 28 Nov 2012 09:12:35 +0100 Message-ID: To: Ivan Gotovchits Cc: Jacques Garrigue , caml-list@inria.fr Content-Type: text/plain; charset=ISO-8859-1 Subject: Re: [Caml-list] phantom types and identity function On Wed, Nov 28, 2012 at 4:42 AM, Ivan Gotovchits wrote: > And now I'm confused much more =). Please, could you explain the > relevance between subtyping and type restriction? I was reacting mostly to Jacques' remark that "you cannot even use subtyping for that". The relation between subtyping and "constraint" is as explained in the manual excerpt I quoted. The following is valid: type 'a t = {x : 'a} ;; let f x = (x : [ `A ] t :> [ `A | `B ] t);; but the following is not: type 'a t = {x : 'a} constraint 'a = [< `A | `B ];; let f x = (x : [ `A ] t :> [ `A | `B ] t);; Error: Type [ `A ] t is not a subtype of [ `A | `B ] t The first variant type does not allow tag(s) `B The reason for this behavior is that in the first case, t was inferred covariant, while the presence of a constraint disables variance inference (in the manual: "otherwise (ie. [...] for non-free parameters) the variance must be given explicitly)"). You can make the constrained version work with an explicit variance annotation: type +'a t = {x : 'a} constraint 'a = [< `A | `B ];; let f x = (x : [ `A ] t :> [ `A | `B ] t);; Finally, while in this example 'a occurs positively in ('a t), in your example 'a did not occur at all. In this case it is correct to coerce from (foo t) to (bar t), whatever the type expression (foo) and (bar) are -- they don't need to be in a subtyping relation. The following works: type 'a t = { x : int };; let f x = (x : [ `A ] t :> [ `B ] t);; I'm calling this form of variance "irrelevant" to highlight that the parameter can simply be ignored when checking for subtyping (some people call it "nonvariant", but it's kind of awkward if you already use "invariant" for the opposite notion of appearing both in positive and negative position). The OCaml type checker can use some restricted form of it (eg. the previous example), but you cannot abstract over it: there is no variance annotation to express that. Jacques' workaround replaces the definition of a new constrained type with a constrained type synonym, that is not checked using variance but direct expansion. But that works because you know what the definition expands to. In general there may be situation when you want to say "type 'a t, where 'a is not used" but not expose a (potentially abstract) non-parametrized type u such that "type 'a t = u". While we're at it: are you sure you need to play with phantom polymorphic variant types now that we have GADTs? I have used phantom types in the past, but my personal use cases would be profitably rewritten using GADTs. They tend to produce hairy error messages, but phantom polymorphic variants are not better in this regard.