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 mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by sympa.inria.fr (Postfix) with ESMTPS id CFF927F1C3 for ; Tue, 27 Nov 2012 17:00:25 +0100 (CET) Received-SPF: None (mail4-smtp-sop.national.inria.fr: no sender authenticity information available from domain of gabriel.scherer@gmail.com) identity=pra; client-ip=209.85.223.182; receiver=mail4-smtp-sop.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail4-smtp-sop.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=mail4-smtp-sop.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 (mail4-smtp-sop.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=mail4-smtp-sop.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: Ai0BAPThtFDRVd+2mGdsb2JhbAA7CQ6tS5I9CCQBAQEBAQgJDQcUJ4IeAQEFJxkBGxILAQMMBgULDQ0hIgERAQUBChIGExKHaAEDDwyiGowzgXCBCoUWChknAwpZiHUBBQyMLhKELwOWAYEcjUgWKYNUPg X-IronPort-AV: E=Sophos;i="4.83,328,1352070000"; d="scan'208";a="163984476" Received: from mail-ie0-f182.google.com ([209.85.223.182]) by mail4-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 27 Nov 2012 17:00:24 +0100 Received: by mail-ie0-f182.google.com with SMTP id s9so20931978iec.27 for ; Tue, 27 Nov 2012 08:00:23 -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=LDkxn8Y3l4Y3mIM5i8jEq74OebSXJqlbqzPr6QToFjk=; b=iTma9bJDho6v0rGIYLCeAJ04uZHqNWL8ZnUXZvXUhXU4fQMq5ohXTXfpBao9x+rHaz fLUHNEtjj9sTZH6AkCcdtJ2ggBomGtegyYYcipmVX5zNU7BmZHjU6b9sx2Zr88TCNgcA 5YRSLj0g6MSYyAgpRwpIPEw/womzJDvla7/SdOOjVWRjMh0RYTPM5ti7Pk/u4tHdvXyL vQUS+uXwD6rewSh1jugFi9ZbATj4j5ipcp71FMqqM3aOuFFGEOY3Q8ftvhvJgf+7z87R I5yY0czxVtlau4UfFFU2+EeSOT4CSPkIl5bey71bFZZ4b+a0ODhW1w0fhN2PK592ONKx NeFg== Received: by 10.50.108.145 with SMTP id hk17mr16101550igb.51.1354032023780; Tue, 27 Nov 2012 08:00:23 -0800 (PST) MIME-Version: 1.0 Received: by 10.50.184.199 with HTTP; Tue, 27 Nov 2012 07:59:43 -0800 (PST) In-Reply-To: <1F656500-76AC-482F-BA08-A9BB8250D904@math.nagoya-u.ac.jp> References: <87ip8rwbsc.fsf@golf.niidar.ru> <1F656500-76AC-482F-BA08-A9BB8250D904@math.nagoya-u.ac.jp> From: Gabriel Scherer Date: Tue, 27 Nov 2012 16:59:43 +0100 Message-ID: To: Jacques Garrigue Cc: Ivan Gotovchits , caml-list@inria.fr Content-Type: text/plain; charset=ISO-8859-1 Subject: Re: [Caml-list] phantom types and identity function I have been a bit confused by this discussion, and found the relevant part of the manual that may enlighten other list readers: The OCaml Language, Type and exception definitions http://caml.inria.fr/pub/docs/manual-ocaml/manual016.html#toc54 "If the type has either a representation or an equation, and the parameter is free (i.e. not bound via a type constraint to a constructed type), its variance constraint is checked but subtyping etc. will use the inferred variance of the parameter, which may be better; otherwise (i.e. for abstract types or non-free parameters), the variance must be given explicitly, and the parameter is invariant if no variance was given." Note that this would not be needed if we had an explicit way to express the variance of invariant (the variable appears in both positive and negative positions) and irrelevant (the variable doesn't appear except in irrelevant positions) explicitly. We could then write, say: type 0'a t = {x : int} constraint 'a = [< `A | `B ] The absence of such a variance marker means that some OCaml code is hard to abstract through a module boundary: in presence of the explicit definition, the type-checker will accept to subtype between any instances of the type (by simple expansion), but if you abstract over its definition you cannot express this property anymore. Your workaround corresponds to statically expressing this irrelevance through an exported equation, but there are (arguably somewhat unnatural) scenarios where this isn't convenient. On Tue, Nov 27, 2012 at 3:08 PM, Jacques Garrigue wrote: > > On 2012/11/27, at 20:00, Ivan Gotovchits wrote: > > > > > Hello, > > > > These simple signature > > > > module type T = sig > > type 'a t constraint 'a = [< `A | `B ] > > val init: [`A] t > > val f: [`A] t -> [`B] t > > end > > > > can be used to constrain the following module > > > > module T : T = struct > > type 'a t = unit constraint 'a = [< `A | `B] > > let init = () > > let f x = x > > end > > > > where identity function successfully satisfies the constraint > > > > [`A] t -> [`B] t > > > > but in the following module > > > > module T : T = struct > > type 'a t = {x:int} constraint 'a = [< `A | `B] > > let init = {x=0} > > let f x = x > > end > > > > the same identity function doesn't satisfy. > > In the first case, a type abbreviation is used. > Since ('a t) expands to (unit), the parameter is completely > ignored, so that you can replace it by anything. > > In the second case, you define a concrete type, > so that the parameter is not forgotten. > Note that you cannot even use subtyping for that: > let f x = (x : [`A] t :> [`B] t) > fails too. > But there is an easy workaround, defining in two steps: > type u = {x:int} > type 'a t = u constraint 'a = [< `A | `B] > > Jacques Garrigue > > -- > 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