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 C9E037EE99 for ; Mon, 9 Dec 2013 22:35:02 +0100 (CET) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of lukstafi@gmail.com) identity=pra; client-ip=209.85.212.179; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="lukstafi@gmail.com"; x-sender="lukstafi@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.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=mail2-smtp-roc.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 (mail2-smtp-roc.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=mail2-smtp-roc.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: AqECAEg2plLRVdSzlGdsb2JhbABZhBK5FoErCBYOAQEBAQcLCwkSKoIlAQEEAScZARseAwELBgUEBzshAQERAQUBHAYTh28BAwkGpTyMWYMJhCUKGScNZIYDEQEFDIxxghqEMwOWKYFrjFqDTBgphFY7 X-IPAS-Result: AqECAEg2plLRVdSzlGdsb2JhbABZhBK5FoErCBYOAQEBAQcLCwkSKoIlAQEEAScZARseAwELBgUEBzshAQERAQUBHAYTh28BAwkGpTyMWYMJhCUKGScNZIYDEQEFDIxxghqEMwOWKYFrjFqDTBgphFY7 X-IronPort-AV: E=Sophos;i="4.93,860,1378850400"; d="scan'208";a="47901655" Received: from mail-wi0-f179.google.com ([209.85.212.179]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 09 Dec 2013 22:35:02 +0100 Received: by mail-wi0-f179.google.com with SMTP id z2so4418466wiv.12 for ; Mon, 09 Dec 2013 13:35:02 -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 :content-type; bh=KXnuAkw46ako8jFF21xua1bk0ljZfesnPwGVs5YIFTk=; b=yqD1F7vJ6NAXyw+jWqeYgldf9Y9JP6TYq9J5w41W5RvVHq4nGrBLmQ/9/eP17G1Quj UF4TreinfGFG/9TrOr6HhJ9qpg+e2YupNfcFYSqnpuVbP84hlX1v8B93Dyl9rmzdmpk3 R9XhMdfQIpVLfFgR/jNvTyUvFMpOeEtgNorzvhDtcKfJUNEOxpSLn2h2bs5hflrqzi48 Vs7wpWDrPz9Szcade7QXwVixUZtshN6S/+Nf91gPvD/UnC7SLVgnGOO5Q0sVmXC+K390 58rYaxFB/FigWfqC6OGXDvQER/1AmG2bMOO5xR94vU12nmw2NrFl6UI3Lb2tK6dsgWsp wqig== X-Received: by 10.194.93.193 with SMTP id cw1mr17622314wjb.38.1386624902010; Mon, 09 Dec 2013 13:35:02 -0800 (PST) MIME-Version: 1.0 Received: by 10.227.36.201 with HTTP; Mon, 9 Dec 2013 13:34:40 -0800 (PST) In-Reply-To: References: From: Lukasz Stafiniak Date: Mon, 9 Dec 2013 22:34:40 +0100 Message-ID: To: Caml Content-Type: multipart/alternative; boundary=047d7bdc0538b89c4904ed20c4ac Subject: Re: [Caml-list] Polymorphic recursion and GADTs --047d7bdc0538b89c4904ed20c4ac Content-Type: text/plain; charset=ISO-8859-1 The annotation needs to be directly at the "function" node: let rec walk : type a b . (a place -> b place -> (a, b) nearby) = (fun x goal -> ((function Same -> Here (x, goal) | NotSame -> let Ex1 ((y, to_y)) = wander x in Transitive (to_y, walk y goal)) : ((a, b) meet -> (a, b) nearby)) (compare x goal)) Regarding the first part, thanks to Gabriel, that explained it to me. On Mon, Dec 9, 2013 at 6:24 PM, Lukasz Stafiniak wrote: > 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.) >> [...] >> Now to a more complex example. >> > > In the complex example, the problem is not the difference between ['a.] > syntax and [type a.] syntax, but polymorphic recursion and GADTs in OCaml > generally. What type annotations do I need to provide? > --047d7bdc0538b89c4904ed20c4ac Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable
The annotation needs to be directly at the "function&= quot; node:

let rec walk : type a b . (a place ->= ; b place -> (a, b) nearby) =3D
=A0 (fun x goal ->
=A0 =A0 ((function Same -> Here (x, goal)
=A0 =A0 =A0 =A0| NotSame ->
=A0 =A0 =A0 =A0 =A0 =A0let Ex= 1 ((y, to_y)) =3D wander x in
=A0 =A0 =A0 =A0 =A0 =A0Transitive (= to_y, walk y goal))
=A0 =A0 : ((a, b) meet -> (a, b) nearby))<= /div>
=A0 =A0 =A0 (compare x goal))

Regarding the first part, thanks to Gabriel, that expla= ined it to me.

On Mon, Dec 9, 2013 at 6:24 PM, Lukasz Stafiniak <lukstafi@= gmail.com> wrote:
On Mon, Dec 9, 2013 at 6:16 PM, Lukasz Stafiniak <lukst= afi@gmail.com> 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 examp= les. (Bear with me, they are automatically generated.)
[...]
Now to a more complex example.=

In the complex example, = the problem is not=A0the difference between ['a.] syntax and [type a.] = syntax, but polymorphic recursion and GADTs in OCaml generally. What type a= nnotations do I need to provide?

--047d7bdc0538b89c4904ed20c4ac--