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 002AE7F707 for ; Tue, 10 Dec 2013 23:52:24 +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=74.125.82.49; 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 74.125.82.49 as permitted sender) identity=mailfrom; client-ip=74.125.82.49; 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-wg0-f49.google.com) identity=helo; client-ip=74.125.82.49; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="lukstafi@gmail.com"; x-sender="postmaster@mail-wg0-f49.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AvECANOap1JKfVIxlGdsb2JhbABZDoQEuSGBGAgWDgEBAQEHCwsJEiqCJQEBBAEnGQEbHQEDDAYFBAc7IgERAQUBHAYTh28BAwkGpV+MWYMJhD0KGScNZIYDEQEFDI55B4Q0BJgUkCYYKYQWQDs X-IPAS-Result: AvECANOap1JKfVIxlGdsb2JhbABZDoQEuSGBGAgWDgEBAQEHCwsJEiqCJQEBBAEnGQEbHQEDDAYFBAc7IgERAQUBHAYTh28BAwkGpV+MWYMJhD0KGScNZIYDEQEFDI55B4Q0BJgUkCYYKYQWQDs X-IronPort-AV: E=Sophos;i="4.93,867,1378850400"; d="scan'208";a="48163571" Received: from mail-wg0-f49.google.com ([74.125.82.49]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 10 Dec 2013 23:52:17 +0100 Received: by mail-wg0-f49.google.com with SMTP id x12so5550243wgg.4 for ; Tue, 10 Dec 2013 14:52:16 -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=Qpg1BcZUBFa6LJmY5/XaL48oYh7bL8SqAUxR9HOELGY=; b=RVO7x1i+RYEG5smlUWKyC6/AOc41K2Gjeidj6zvBWjKyYcjFzEdEeM5Ve7fEgCJEsO t/K1zgi42HpfGLyLLcbX1UmnyPhWcqxTOrlmN3yx8v5q2HrU/Do9AUAPGi1eCvHViJUL OtVuiWo+Bvrk+e27mCIEuOWGxe+Kc9w9Rzjj7NoHPzjMRV9K4aMZazMfl1/lPa83fGvY inQq7x6+6DiS0cIyhgIGXzTXtUi9lD2oJnu0ax/TGwg5EzQmz0FDFs6E/gD6bp1R5OiW OvgXm38G7koBsr6Xe0NdXaGVw8zn4eSikGJry5nOLo+DLw0AhFDTDPhaJVdGtS9oY7qk YBKA== X-Received: by 10.194.95.198 with SMTP id dm6mr13571316wjb.57.1386715936127; Tue, 10 Dec 2013 14:52:16 -0800 (PST) MIME-Version: 1.0 Received: by 10.227.36.201 with HTTP; Tue, 10 Dec 2013 14:51:56 -0800 (PST) In-Reply-To: <83E00BC5-3599-4702-873E-0FD6863050CC@math.nagoya-u.ac.jp> References: <83E00BC5-3599-4702-873E-0FD6863050CC@math.nagoya-u.ac.jp> From: Lukasz Stafiniak Date: Tue, 10 Dec 2013 23:51:56 +0100 Message-ID: To: Jacques Garrigue Cc: OCaml Mailing List Content-Type: multipart/alternative; boundary=047d7bb03a50c7014604ed35f6de Subject: Re: [Caml-list] Polymorphic recursion and GADTs --047d7bb03a50c7014604ed35f6de Content-Type: text/plain; charset=ISO-8859-1 On Tue, Dec 10, 2013 at 11:43 PM, Jacques Garrigue < garrigue@math.nagoya-u.ac.jp> wrote: > > As always, Gabriel's answer is correct, but I have two remarks. > First, concerning your first example where you needed annotations on the > local function, > you can actually avoid that by using pattern matching rather than function > application: > > I realized that after posting :-) > > Now, for the above example, of course you don't need to annotate the > "function" construct, > but if you want to name the rigid variables 't47 and 't59, you can do that > through eta-expansion: > > let rec eval : type a . (a term -> a) = > 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) > | Pair (x, y) -> (eval x, eval y) > | Fst p -> (fun (type b) p -> let ((x, y): (a * b)) = eval p in x) p > | Snd p -> (fun (type b) p -> let ((x, y): (b * a)) = eval p in y) p > > Not very clean, so we need to do something about it. > > I do not need it, I am just exploring ways of outputting that information in case someone would find it useful (under the big conditional that someone would find InvarGenT useful in the first place, rather than just cool...) --047d7bb03a50c7014604ed35f6de Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable
On T= ue, Dec 10, 2013 at 11:43 PM, Jacques Garrigue <garrigue@math.n= agoya-u.ac.jp> wrote:

As always, Gabriel's answer is correct, but I have two rema= rks.
First, concerning your first example where you needed annotations on the lo= cal function,
you can actually avoid that by using pattern matching rather than function = application:

I realized that after posting= :-)
=A0
Now, for the above example, of course you don't need to annotate the &q= uot;function" construct,
but if you want to name the rigid variables 't47 and 't59, you can = do that through eta-expansion:

let rec eval : type a . (a term -> a) =3D
=A0 function Lit i -> i | IsZero x -> is_zero= (eval x)
=A0 =A0 | Plus (x, y) -> plus (eval x) (eval y)
=A0 =A0 | If (b, t, e) -> if_then (eval b) (eval t) (eval e)
=A0 =A0 | Pair (x, y) -> (eval x, eval y)
=A0 =A0 | Fst p -> (fun (type b) p -> let ((x, y): (a * b)) =3D= eval p in x) p
=A0 =A0 | Snd p -> (fun (type b) p -> let ((x, y): (b * a)) =3D eval = p in y) p

Not very clean, so we need to do something about it.

I do not need it, I am just exploring ways of outputting that infor= mation in case someone would find it useful (under the big conditional that= someone would find InvarGenT useful in the first place, rather than just c= ool...)
--047d7bb03a50c7014604ed35f6de--