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 B59057EE99 for ; Mon, 9 Dec 2013 18:17:13 +0100 (CET) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of lukstafi@gmail.com) identity=pra; client-ip=209.85.212.179; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="lukstafi@gmail.com"; x-sender="lukstafi@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of lukstafi@gmail.com designates 209.85.212.179 as permitted sender) identity=mailfrom; client-ip=209.85.212.179; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="lukstafi@gmail.com"; x-sender="lukstafi@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-wi0-f179.google.com) identity=helo; client-ip=209.85.212.179; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="lukstafi@gmail.com"; x-sender="postmaster@mail-wi0-f179.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AvgCAIn6pVLRVdSzlGdsb2JhbABZgz9Tgn+BQbQHToEnCBYOAQEBAQcLCwkSKoJPBBkBGx4DEgMNNwIkAREBBQEiiAIBAw8NliyMVoMFjAZTgwmEHgoZJw1khgMRAQEEDI8AgnaBSAOYFJAmGCmEVjs X-IPAS-Result: AvgCAIn6pVLRVdSzlGdsb2JhbABZgz9Tgn+BQbQHToEnCBYOAQEBAQcLCwkSKoJPBBkBGx4DEgMNNwIkAREBBQEiiAIBAw8NliyMVoMFjAZTgwmEHgoZJw1khgMRAQEEDI8AgnaBSAOYFJAmGCmEVjs X-IronPort-AV: E=Sophos;i="4.93,859,1378850400"; d="scan'208";a="40103208" Received: from mail-wi0-f179.google.com ([209.85.212.179]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 09 Dec 2013 18:17:13 +0100 Received: by mail-wi0-f179.google.com with SMTP id z2so4056779wiv.6 for ; Mon, 09 Dec 2013 09:17:12 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:from:date:message-id:subject:to:content-type; bh=MEbm4mQNX1syhRGolp+tzshalLlQpDiP0EErnWGoN84=; b=lHE9XI9bSATu1+IV926LTfOiBTNl2RXNWqxmXf3lKgCQpMCaHG6fDINP0ZdVp92WBF wkfO7fTm8k0WBUGpLJre440hq4tFooVH4vQVWAE52ux8F/XphKnt69nn8VU72SH83eFI buUsolgQQ03d7ijZvG2lxIaWun/KieM9YfBRVZEI0faamtf6psaIU4j/EONONg0yutL+ SOim7Sy4iofi9pV7zIMfaPKeP7bwvuRFthrBDStTtf4r+3Mc/avCr05y7ltUCXzuEA7L vwaBSCIBjmwycOi1q66KnpP6nt3i+KPGhQDsbF/bI6aSkqQ41P+BFf7uq3dDUf+rG6xz KyKg== X-Received: by 10.180.20.15 with SMTP id j15mr15330854wie.4.1386609432580; Mon, 09 Dec 2013 09:17:12 -0800 (PST) MIME-Version: 1.0 Received: by 10.227.36.201 with HTTP; Mon, 9 Dec 2013 09:16:52 -0800 (PST) From: Lukasz Stafiniak Date: Mon, 9 Dec 2013 18:16:52 +0100 Message-ID: To: Caml Content-Type: multipart/alternative; boundary=bcaec53f3985abf4d204ed1d2a43 Subject: [Caml-list] Polymorphic recursion and GADTs --bcaec53f3985abf4d204ed1d2a43 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable 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 term 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) nearby = -> ('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) nearby 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.gadt https://github.com/lukstafi/invargent/blob/master/examples/equational_reas.= gadt --bcaec53f3985abf4d204ed1d2a43 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
Hello,

I am at a loss as to the differe= nce between ['a.] syntax and [type a.] syntax of introducing polymorphi= c recursion. I will provide some examples. (Bear with me, they are automati= cally 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:

--bcaec53f3985abf4d204ed1d2a43--