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 EAE437EE99 for ; Mon, 9 Dec 2013 18:26:12 +0100 (CET) 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.46; 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.46 as permitted sender) identity=mailfrom; client-ip=209.85.214.46; 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-f46.google.com) identity=helo; client-ip=209.85.214.46; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="postmaster@mail-bk0-f46.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AlgCAKL8pVLRVdYum2dsb2JhbABZFoMpU4J/gUGsA4gEToEnCBYOAQEBAQEGCwsJFCiCJQEBAwEBIwQZARsdAQMBCwYDAgsDNAICIQEBEQEFARwGEwiHZwEDCQYNliyPW4wGU4MJhB4KGScNZIYDEQEFDIxxgg8EB4JrgUgDlimBa4EwixoQg0wYKYRWOw X-IPAS-Result: AlgCAKL8pVLRVdYum2dsb2JhbABZFoMpU4J/gUGsA4gEToEnCBYOAQEBAQEGCwsJFCiCJQEBAwEBIwQZARsdAQMBCwYDAgsDNAICIQEBEQEFARwGEwiHZwEDCQYNliyPW4wGU4MJhB4KGScNZIYDEQEFDIxxgg8EB4JrgUgDlimBa4EwixoQg0wYKYRWOw X-IronPort-AV: E=Sophos;i="4.93,859,1378850400"; d="scan'208";a="47870960" Received: from mail-bk0-f46.google.com ([209.85.214.46]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 09 Dec 2013 18:26:12 +0100 Received: by mail-bk0-f46.google.com with SMTP id u15so1510645bkz.33 for ; Mon, 09 Dec 2013 09:26:11 -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=lnK4qd8RoMZRgi7jRBesolzt0IQxpCsXeA48IlRnDd8=; b=u2DukJcpPGZitXo0/hHGHgr5xWPqk+Q2k4I8LFTkrETcleiTxuaRe7vDuA7t/vynGW +/ht39J6UNm+O92abTabpey6Xev9m/CHd0XPqJH3tMG1bCqB+IppezjRq7liylKMQmOP ZCWiud/3fZvSndMyfaRvrN095koebmP9DJaD33PdJwxNO3JO2oLIxYWEsAJu7a3XlMDe kCgBqI4Ze6FOo7+Fs8/Fpg/3WqckmmwTr+Z+pCaGGNxFVsdSZTGF4Cu3y849jqVs2+Gh aaiTgYFlbMzQ9hRwQk44PCF6gaUUluEvGvj7eWYyABZYBZWkw4abGpZuvu0Qc1iKITSx QOFw== X-Received: by 10.205.64.209 with SMTP id xj17mr2681476bkb.76.1386609971686; Mon, 09 Dec 2013 09:26:11 -0800 (PST) MIME-Version: 1.0 Received: by 10.204.122.72 with HTTP; Mon, 9 Dec 2013 09:25:31 -0800 (PST) In-Reply-To: References: From: Gabriel Scherer Date: Mon, 9 Dec 2013 18:25:31 +0100 Message-ID: To: Lukasz Stafiniak Cc: Caml Content-Type: multipart/alternative; boundary=bcaec5430da0ce1d0304ed1d4acd Subject: Re: [Caml-list] Polymorphic recursion and GADTs --bcaec5430da0ce1d0304ed1d4acd Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable TL;DR: you should use those "rigid variables" to annotate type variable that will be refined in a GADT pattern matching. The way GADT type variables can be refined with different types in each branches is different and orthogonal to the type unification mechanism. Variables ('a) use type unification on each branch, which fails with the error you observe. Local type constructors (a), and only them, can be refined in GADT clauses, so that type refinement works. The syntax let rec f : type a . a -> ... =3D fun x -> ... as opposed to let rec f (type a) (x : a) ... =3D ... combines the GADT-readiness of those weird variables with polymorphic recursion -- which is orthogonal, but in practice they often come together. For more technical details, see "Ambivalent types for type inference with GADTs", by Jacques Garrigue and Didier R=C3=A9my, 2013: http://gallium.inria.fr/~remy/gadts/Garrigue-Remy:gadts@short2013.pdf On Mon, Dec 9, 2013 at 6:16 PM, Lukasz Stafiniak wrote: > Hello, > > I am at a loss as to the difference between ['a.] syntax and [type a.] > syntax of introducing polymorphic recursion. I will provide some examples. > (Bear with me, they are automatically generated.) > >>> > type _ term =3D > | Lit : integer -> integer term > | Plus : integer term * integer term -> integer term > | IsZero : integer term -> boolean term > | If : (*=E2=88=80'a.*)boolean term * 'a term * 'a term -> 'a term > and integer > > and boolean > > external plus : (integer -> integer -> integer) =3D "plus" > external is_zero : (integer -> boolean) =3D "is_zero" > external if_then : (boolean -> 'a -> 'a -> 'a) =3D "if_then" > let rec eval : 'a . ('a term -> 'a) =3D > (function Lit i -> i | IsZero x -> is_zero (eval x) > | Plus (x, y) -> plus (eval x) (eval y) > | If (b, t, e) -> if_then (eval b) (eval t) (eval e)) > <<< > The above produces: > Error: This pattern matches values of type boolean term > but a pattern was expected which matches values of type integer te= rm > Type boolean is not compatible with type integer > but if we replace the corresponding line with: > >>> > ... > let rec eval : type a . (a term -> a) =3D > ... > <<< > then it compiles fine. > > Now to a more complex example. According to my understanding (and > InvarGenT), the following code should type-check: > >>> > type _ place =3D > | LocA : a place > | LocB : b place > and a > and b > > type (_, _) nearby =3D > | Here : (*=E2=88=80'b.*)'b place * 'b place -> ('b, 'b) nearby > | Transitive : (*=E2=88=80'a, 'b, 'c.*)('a, 'b) nearby * ('b, 'c) nearb= y -> > ('a, 'c) nearby > type boolean > > external is_nearby : (('a, 'b) nearby -> boolean) =3D "is_nearby" > type _ ex1 =3D > | Ex1 : (*=E2=88=80'a, 'b.*)('b place * ('a, 'b) nearby) -> 'a ex1 > external wander : ('a place -> 'a ex1) =3D "wander" > type (_, _) meet =3D > | Same : (*=E2=88=80'b.*) ('b, 'b) meet > | NotSame : (*=E2=88=80'a, 'b.*) ('a, 'b) meet > external compare : ('a place -> 'b place -> ('a, 'b) meet) =3D "compare" > let rec walk : type a b . (a place -> b place -> (a, b) nearby) =3D > (fun x goal -> > ((function Same -> Here (x, goal) > | NotSame -> > let Ex1 ((y, to_y)) =3D wander x in Transitive (to_y, walk y > goal))) > (compare x goal)) > <<< > Here we get > Error: This expression has type b place > but an expression was expected of type a place > Type b is not compatible with type a > And when we switch to the ['a.] syntax, we get > Error: This definition has type 'a. 'a place -> 'a place -> ('a, 'a) near= by > which is less general than > 'a 'b. 'a place -> 'b place -> ('a, 'b) nearby > > Thanks in advance for any thoughts. > If you are curious, the source code is: > https://github.com/lukstafi/invargent/blob/master/examples/simple_eval.ga= dt > > https://github.com/lukstafi/invargent/blob/master/examples/equational_rea= s.gadt > > --bcaec5430da0ce1d0304ed1d4acd Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
TL;DR: you should use those "rigid variables&qu= ot; to annotate type variable that will be refined in a GADT pattern matchi= ng.

The way GADT type variables can be refined with different types = in each branches is different and orthogonal to the type unification mechan= ism. Variables ('a) use type unification on each branch, which fails wi= th the error you observe. Local type constructors (a), and only them, can b= e refined in GADT clauses, so that type refinement works. The syntax
=C2=A0 let rec f : type a . a -> ... =3D fun x -> ...
a= s opposed to
=C2=A0 let rec f (type a) (x : a) ... =3D ...
combines the GADT-readiness of those weird variables with poly= morphic recursion -- which is orthogonal, but in practice they often come t= ogether.

For more technical details, see "Ambivalent types for type i= nference with GADTs", by Jacques Garrigue and Didier R=C3=A9my, 2013: = http://gallium.inria.fr/~remy/gadts/Garrigue-Remy:= gadts@short2013.pdf


On Mon, Dec 9, 2013 at 6:16 PM, L= ukasz Stafiniak <lukstafi@gmail.com> wrote:
Hello,
I am at a loss as to the difference between ['a.] syn= tax and [type a.] syntax of introducing polymorphic recursion. I will provi= de some examples. (Bear with me, they are automatically generated.)
>>>
type _ term =3D
=C2=A0 | Lit : i= nteger -> integer term
=C2=A0 | Plus : integer term * integer = term -> integer term
=C2=A0 | IsZero : integer term -> bool= ean term
=C2=A0 | If : (*=E2=88=80'a.*)boolean term * 'a term * 'a = term -> 'a term
and integer
=C2=A0=C2=A0
and boolean
=C2=A0=C2=A0
external plus : (integer -&= gt; integer -> integer) =3D "plus"
external is_zero : (integer -> boolean) =3D "is_zero"
external if_then : (boolean -> 'a -> 'a -> 'a) = =3D "if_then"
let rec eval : 'a . ('a term ->= ; 'a) =3D
=C2=A0 (function Lit i -> i | IsZero x -> is_zero (eval x)
=
=C2=A0 =C2=A0 | Plus (x, y) -> plus (eval x) (eval y)
=C2= =A0 =C2=A0 | If (b, t, e) -> if_then (eval b) (eval t) (eval e))
<<<
The above produces:
Error: This pattern matches values = of type boolean term
=C2=A0 =C2=A0 =C2=A0 =C2=A0but a pattern was= expected which matches values of type integer term
=C2=A0 =C2=A0= =C2=A0 =C2=A0Type boolean is not compatible with type integer=C2=A0
but if we replace the corresponding line with:
&g= t;>>
...
let rec eval : type a . (a term -> a)= =3D
...
<<<
then it compiles = fine.

Now to a more complex example. According to my understa= nding (and InvarGenT), the following code should type-check:
>= >>
type _ place =3D
=C2=A0 | LocA : a place<= /div>
=C2=A0 | LocB : b place
and a
and b
=C2= =A0=C2=A0
type (_, _) nearby =3D
=C2=A0 | Here : (*=E2= =88=80'b.*)'b place * 'b place -> ('b, 'b) nearby
=C2=A0 | Transitive : (*=E2=88=80'a, 'b, 'c.*)('a, = 'b) nearby * ('b, 'c) nearby ->
=C2=A0 =C2=A0 ('a, 'c) nearby
type boolean
=C2=A0=C2=A0
external is_nearby : (('a, 'b) nearby ->= boolean) =3D "is_nearby"
type _ ex1 =3D
=C2= =A0 | Ex1 : (*=E2=88=80'a, 'b.*)('b place * ('a, 'b) ne= arby) -> 'a ex1
external wander : ('a place -> 'a ex1) =3D "wander&quo= t;
type (_, _) meet =3D
=C2=A0 | Same : (*=E2=88=80'= ;b.*) ('b, 'b) meet
=C2=A0 | NotSame : (*=E2=88=80'a,= 'b.*) ('a, 'b) meet
external compare : ('a place -> 'b place -> ('a, = 9;b) meet) =3D "compare"
let rec walk : type a b . (a p= lace -> b place -> (a, b) nearby) =3D
=C2=A0 (fun x goal -&= gt;
=C2=A0 =C2=A0 ((function Same -> Here (x, goal)
=C2=A0 = =C2=A0 =C2=A0 =C2=A0| NotSame ->
=C2=A0 =C2=A0 =C2=A0 =C2=A0 = =C2=A0 =C2=A0let Ex1 ((y, to_y)) =3D wander x in Transitive (to_y, walk y g= oal)))
=C2=A0 =C2=A0 =C2=A0 (compare x goal))
<= ;<<
Here we get
Error: This expression has type b place
=C2=A0 =C2=A0 =C2=A0 =C2=A0but an expression was expected of type a = place
=C2=A0 =C2=A0 =C2=A0 =C2=A0Type b is not compatible with ty= pe a=C2=A0
And when we switch to the ['a.] syntax, we g= et
Error: This definition has type 'a. 'a place -> 'a= place -> ('a, 'a) nearby
=C2=A0 =C2=A0 =C2=A0 =C2=A0w= hich is less general than
=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0'= a 'b. 'a place -> 'b place -> ('a, 'b) nearby

Thanks in advance for any thoughts.
If = you are curious, the source code is:


--bcaec5430da0ce1d0304ed1d4acd--