Re: [Caml-list] CPS converting existential data type

[Stephen Dolan <stephen.dolan@cl.cam.ac.uk>]

[-- Attachment #1: Type: text/plain, Size: 1412 bytes --]

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

[-- Attachment #2: Type: text/html, Size: 2261 bytes --]