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 00E3C7EE25 for ; Tue, 29 Oct 2013 15:47:51 +0100 (CET) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of gabriel.scherer@gmail.com) identity=pra; client-ip=209.85.214.41; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.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=mail3-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 (mail3-smtp-sop.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=mail3-smtp-sop.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: Ar4BAEfJb1LRVdYpm2dsb2JhbABZhBODE7wigSEIFg4BAQEBAQYLCwkUKIIlAQEFIwQZARsWBwEDDAYFCw0CAiYCAiIBEQEFARwGE4d0AQMPmxqMBFODCoRPChknDWSJAQEFDIEdjWszB4JqgUIDmAqQHBgphFI7 X-IPAS-Result: Ar4BAEfJb1LRVdYpm2dsb2JhbABZhBODE7wigSEIFg4BAQEBAQYLCwkUKIIlAQEFIwQZARsWBwEDDAYFCw0CAiYCAiIBEQEFARwGE4d0AQMPmxqMBFODCoRPChknDWSJAQEFDIEdjWszB4JqgUIDmAqQHBgphFI7 X-IronPort-AV: E=Sophos;i="4.93,593,1378850400"; d="scan'208";a="32442229" Received: from mail-bk0-f41.google.com ([209.85.214.41]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 29 Oct 2013 15:47:51 +0100 Received: by mail-bk0-f41.google.com with SMTP id na10so2460406bkb.14 for ; Tue, 29 Oct 2013 07:47:50 -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:content-transfer-encoding; bh=9gaNBSNpjzyWjG/WuCXQoEVMmEZpfe3sZQ8md/Idd3M=; b=P9jPcfFQB9bAgRVHz3JwmZ8JM4ylaioL8ozsTpsTxj1d81j4SS6b/OHz3l1OaM+ZdS +VUQ9JkyW4aehHEbMpTTmRg4d5SDADH5F6s/YFHW2zTLArzvTGM/RF7AerAF9tPrwS/R NdARm4xei49EY6Xyw2qskvPI1tUVPyTAXPjQwDaja8JnTeRJAi9ByBT2wWS4G+xc6n4i klbLSm4HQ6Ln3ORv+FOiAwdThnOMKtOrY/tu8DQSXHpmAqSyzJ2zeQ5pDEtUWXhQ+1i7 XyliSJowXhET9qXyC0Yw/z8cxOhMQ+widjNu0jOvbVBuds9+3nP2rVH0F7pw9aL2rU2h qUGQ== X-Received: by 10.204.98.68 with SMTP id p4mr165757bkn.147.1383058070545; Tue, 29 Oct 2013 07:47:50 -0700 (PDT) MIME-Version: 1.0 Received: by 10.204.122.72 with HTTP; Tue, 29 Oct 2013 07:47:10 -0700 (PDT) In-Reply-To: <526FC379.30506@labri.fr> References: <526A5F2A.6060904@labri.fr> <526FC379.30506@labri.fr> From: Gabriel Scherer Date: Tue, 29 Oct 2013 15:47:10 +0100 Message-ID: To: David RENAULT Cc: caml users Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Subject: Re: [Caml-list] GADTs : a type variable cannot be deduced The equality we're talking about the following: two types are equal if they are exactly exchangeable from the type-checking point of view. =46rom this point of view, (int t) and (bool t) may be equal or different depending on how (t) is defined. Consider: type 'a u =3D int in this case (int u) and (bool u) are equal (to int), but consider an algebraic datatype (sum or record) type 'a t =3D Foo of bool in this case (int t) and (bool t) are considered distinct by the type-check= er, even if 'a does not actually appear in the definition of the algebraic datatype. To wit: # type 'a t =3D Foo of bool;; type 'a t =3D Foo of bool # let (x : int t) =3D Foo true;; val x : int t =3D Foo true # let (y : bool t) =3D Foo false;; val y : bool t =3D Foo false # [x; y];; Error: This expression has type bool t but an expression was expected of type int t Type bool is not compatible with type int So "new" types like variants or records are always injective in all their parameters, but type synonyms may not be. (Note: the notion of "equality" we're talking about is distinct from, and stricter than, the symmetric closure of OCaml's subtyping relation: here we have (int t =E2=89=A4 bool t) and conversely) Now if you have module Foo : sig type 'a t end =3D struct ... end You cannot know (without looking at the implementation) if the abstract declaration of ('a t) here is more like the (type 'a u =3D int) example, or the (type 'a t =3D Foo of bool) example. So OCaml must conservatively assume that ('a t) may fail to be injective. Then consider the definition type _ nat =3D Succ : 'a nat -> ('a succ nat) OCaml will accept this definition if it can prove that, for any type foo, if (Succ blah : foo succ nat) holds for any OCaml type (foo), then (blah : foo) also holds. (Because this implication will then be used to type-check code that pattern-matches on this type.) This implication is only true if ('a succ) is injective. Hence, the definition is rejected when ('a succ) is defined as ('a u) above, or abstract. On Tue, Oct 29, 2013 at 3:17 PM, David RENAULT wrote: > Gabriel Scherer wrote: >> The problem is with the assumed injectivity of the abstract type 'a >> succ. You should write: >> >> type 'a succ =3D Succ >> >> then everything works out. >> >> Injectivity was assumed to hold for types *defined* to be abstract, but >> does not hold for types *declared* as abstract (That may have been >> defined concretely as just "int" in their implementation). For >> consistency, defined-abstract type are no more assumed to be injective, >> so you should always use a constructor for that (using a constructor >> makes your type nominal/generative/fresh, which enforces injectivity). >> >> Remark: I'll let you work out while it would be problematic to consider >> a ('a succ succ nat)-matching branch as dead when matching over a ('a >> succ nat) value, under the definition (type 'a succ =3D int). > > OK, thank you for your answer, I have taken some time to dive into the > question of injectivity of types, and I believe that there is something > I am missing. With your help, the following code compiles : > > =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D > type 'a succ =3D Succ > type _ nat =3D NS : 'a nat -> ('a succ) nat > =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D > > If we leave the type abstract, then the type function NS may not be > injective. But if we give a concrete implementation with a constructor, > it works out. To me, the concrete implementation is not injective (it > maps everything on "Succ nat"), but you proclaim that it becomes > automatically injective. Why does mapping everything onto a new type > enforce injectivity ? > > RENAULT David >