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 701097F72A for ; Sun, 21 Aug 2016 14:36:02 +0200 (CEST) IronPort-PHdr: 9a23:QQMfdR+9MDjSv/9uRHKM819IXTAuvvDOBiVQ1KB80ukcTK2v8tzYMVDF4r011RmSDNydsaMP1rCe8/i5HzdRudDZ6DFKWacPfidNsd8RkQ0kDZzNImzAB9muURYHGt9fXkRu5XCxPBsdMs//Y1rPvi/6tmZKSV3BPAZ4bt74BpTVx5zukbvjotuJMk4V3nL9Oeo0d0Tu612J94E/ushLEu4J0BzHo39FKax95FhDAhatpSv6/dq655V58i5d6LoL/s9EVrjmLexjFeQLRBxvCW0+5dXquB/fVkPPoyJECiRF2iZPVirM5wjnU4y5nSLgrOtyxSTSacL/V6o1Vimvx6JiVB+uji4IMC8wtXyRg8c2jroN8zy7oBkq+JLZeIGYMrJSeafUe5tOXnZMRsZcUWpNBYe1aaMEC6wKNOMepoK7ulhY/kj2PhWlGO66kmwAvXTxx6Bvlr15SQw= Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=stedolan@stedolan.net; spf=None smtp.mailfrom=stedolan@stedolan.net; spf=None smtp.helo=postmaster@mail-oi0-f51.google.com Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of stedolan@stedolan.net) identity=pra; client-ip=209.85.218.51; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="stedolan@stedolan.net"; x-sender="stedolan@stedolan.net"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of stedolan@stedolan.net) identity=mailfrom; client-ip=209.85.218.51; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="stedolan@stedolan.net"; x-sender="stedolan@stedolan.net"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-oi0-f51.google.com) identity=helo; client-ip=209.85.218.51; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="stedolan@stedolan.net"; x-sender="postmaster@mail-oi0-f51.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0CIAABcn7lXhjPaVdFeDoQMfAeyZYUIgX4jhB6BITqBJwc4FAIBAQEBAQEBARIBAQEICwsJGS+CMgQBEwGCEwEBBAESEQQZAQE3AQQLAQoEBw0qAgIiEgEFARwGEyKIBwgECp4kgTI+MopVZ4RFAQEFhywag0kBAQgBAQEBGwMFEIYbhE2EbYJUglqZTYFkhDyIf49QjD+COBMegQ8eg3U8bwEEhXcBfgEBAQ X-IPAS-Result: A0CIAABcn7lXhjPaVdFeDoQMfAeyZYUIgX4jhB6BITqBJwc4FAIBAQEBAQEBARIBAQEICwsJGS+CMgQBEwGCEwEBBAESEQQZAQE3AQQLAQoEBw0qAgIiEgEFARwGEyKIBwgECp4kgTI+MopVZ4RFAQEFhywag0kBAQgBAQEBGwMFEIYbhE2EbYJUglqZTYFkhDyIf49QjD+COBMegQ8eg3U8bwEEhXcBfgEBAQ X-IronPort-AV: E=Sophos;i="5.28,555,1464645600"; d="scan'208,217";a="233553455" Received: from mail-oi0-f51.google.com ([209.85.218.51]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 21 Aug 2016 14:36:00 +0200 Received: by mail-oi0-f51.google.com with SMTP id f189so118799202oig.3 for ; Sun, 21 Aug 2016 05:36:00 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=stedolan-net.20150623.gappssmtp.com; s=20150623; h=mime-version:sender:in-reply-to:references:from:date:message-id :subject:to:cc; bh=XO2MLoaV+UN0nmpAbV4n2Df/FLmLwnaQE2qld/00D+4=; b=0gIAOk9JiK40hWopAWoc1oIb7ytE+8bMwQOJF8/L6tuB4UKiCS75v3l27KhOY6hbKI 3AP1UTXmyFfqOdQFG5LX1d48bOGzKSqOIh8SPnjJlEEEcMaZ89Qh6BFPI9cNz6wtMfz7 RkAbWgzDYnQG1/l1mxA229dxPyhqex2P6RqOlcaidVXt3Pm9smXpu9atFvghbDsUy/IS HrtIfJmqGg15swxQxuv1JSdXOPGHQsdFx4QYRPGEUj0aBICgfpLjIoHBhHmaGwX+ZAJ8 R8dMhsRGFhotlIedl4aIgkO0FG588uMT7PmZwGZMDClDZRVO4++pthNRSri7RE87FcU7 OAAw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20130820; h=x-gm-message-state:mime-version:sender:in-reply-to:references:from :date:message-id:subject:to:cc; bh=XO2MLoaV+UN0nmpAbV4n2Df/FLmLwnaQE2qld/00D+4=; b=kogcS1wTYTFuSfqtNfzYdkNmtkOl7tbehE0SNvjMroSmC6iESST4kf7uxsQzqI/gUJ 1sUS9xTzFPzKbJ1mHLOpenn86kGF698n6d8Pg+yPTx6iruya9pQOLgOiZySS902hraeh Vkeo1F49+favPOUW3yGOteqvP7FZTqZ9Nt49GGIy7N0MQLEuhm/q1TLVli4m10YUsvAw Ic/yvtRBhDtutMtWq9jAayQqvTAShv3wTN2qLqUFqbc26V3OM0sfINA4AocGsfCVrNN9 hxO+fK0xFabtsF9OKKm4ace5pRcQ/pbarNKoqzoHTPaus4lvRE3tihpqUhANTxqpBP6p CPxQ== X-Gm-Message-State: AEkoouvpqqXaAFRCLwNFIr8v6EE+E/j1d78bdsIFopAffHzi6SXn3Mspk+wj9xhwGav5gu/CjDfmXRywjI1KGw== X-Received: by 10.157.40.239 with SMTP id s102mr10189335ota.7.1471782959667; Sun, 21 Aug 2016 05:35:59 -0700 (PDT) MIME-Version: 1.0 Sender: stedolan@stedolan.net Received: by 10.202.240.2 with HTTP; Sun, 21 Aug 2016 05:35:59 -0700 (PDT) X-Originating-IP: [109.79.176.233] In-Reply-To: References: <1471651332.586948056@f325.i.mail.ru> From: Stephen Dolan Date: Sun, 21 Aug 2016 13:35:59 +0100 X-Google-Sender-Auth: vKt3avo2lXMffKWhnqMK9M4o21c Message-ID: To: Jacques Garrigue Cc: Alexey Egorov , OCaML List Mailing Content-Type: multipart/alternative; boundary=001a113f8ac07f73ab053a942cdc Subject: Re: [Caml-list] CPS converting existential data type --001a113f8ac07f73ab053a942cdc Content-Type: text/plain; charset=UTF-8 On Sat, Aug 20, 2016 at 2:57 AM, Jacques Garrigue < garrigue@math.nagoya-u.ac.jp> wrote: > On 2016/08/20 09:02, Alexey Egorov wrote: > > > > Hello, > > > > in haskell it's possible to convert some data type to it CPS'ed form > using rank-N polymorphism. > > > > I'm trying to do the same in ocaml using objects with polymorphic > methods (instead of GHC RankNTypes extension), and it works well unless I'm > using data type with existential type variables. > > > > Example - https://gist.github.com/anonymous/ > 57262e4e1009e658b97e8986a2d03d40 > > Haskell version compiles, while ocaml version gives type error about > universal variable escaping it's scope. > > > > What is the right way to do this? Is it possible at all? > > > The problem is that type annotations are not propagated to the body of > objects, so you need to annotate the method explicitly, or to annotate the > type of self. > The following annotated version works: > > let uncps : type a . a cps_t -> a t = > fun p -> p # get Nil (object > method get : 'e . (a, 'e) d -> ('e -> a) -> a t = fun d f -> Cons (d, > f) > end) > Incidentally, you can do it quite neatly by using polymorphic records instead of polymorphic objects: type ('a,'r) uncons = { cons : 'e . ('a, 'e) d -> ('e -> 'a) -> 'r } type 'a cps_t = { runCps : 'r . 'r -> ('a, 'r) uncons -> 'r } let uncps {runCps} = runCps Nil {cons = fun d f -> Cons(d, f)} Stephen --001a113f8ac07f73ab053a942cdc Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
On S= at, Aug 20, 2016 at 2:57 AM, Jacques Garrigue <garrigue@math.na= goya-u.ac.jp> wrote:
On 2016/08/20 09:02,= Alexey Egorov wrote:
>
> Hello,
>
> in haskell it's possible to convert some data type to it CPS'e= d form using rank-N polymorphism.
>
> I'm trying to do the same in ocaml using objects with polymorphic = methods (instead of GHC RankNTypes extension), and it works well unless I&#= 39;m using data type with existential type variables.
>
> Example - https://gist.github= .com/anonymous/57262e4e1009e658b97e8986a2d03d40
> Haskell version compiles, while ocaml version gives type error about u= niversal variable escaping it's scope.
>
> What is the right way to do this? Is it possible at all?


The problem is that type annotations are not propagated to the body of obje= cts, so you need to annotate the method explicitly, or to annotate the type= of self.
The following annotated version works:

let uncps : type a . a cps_t -> a t =3D
=C2=A0 fun p -> p # get Nil (object
=C2=A0 =C2=A0 method get : 'e . (a, 'e) d -> ('e -> a) -&= gt; a t =3D fun d f -> Cons (d, f)
=C2=A0 end)

Incidentally, you can do it quite neatly by usi= ng polymorphic records instead of polymorphic objects:

=
type ('a,'r) uncons =3D { cons : 'e . ('a, 'e) d -= > ('e -> 'a) -> 'r }
type 'a cps_t =3D {= runCps : 'r . 'r -> ('a, 'r) uncons -> 'r }

let uncps {runCps} =3D runCps Nil {cons =3D fun d f -&= gt; Cons(d, f)}

Stephen
--001a113f8ac07f73ab053a942cdc--