[Caml-list] CPS converting existential data type

[Caml-list] CPS converting existential data type

[Alexey Egorov]

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

 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?

Thanks.


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

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

[Jacques Garrigue]

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)

Thank you for this interesting example.

Jacques Garrigue

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

[Stephen Dolan]

[-- 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 --]