Simple polymorphic type annotation in OCaml

user_242189 0
Viewed 104

Are some annotations needed to make this typecheck in ocaml ?

type ('a,'b) roll = Roll of (('b,'a) roll -> 'b)
let unroll (Roll f) = f 

(* nope-   
This definition has type        ('b, 'b) roll -> ('b, 'b) roll -> ('b, 'b) roll
which is less general than  'c. ('b, 'c) roll -> ('b, 'b) roll -> ('b, 'c) roll *)

let rec (-:) : 'c. ('b,'c) roll -> ('a,'b) roll -> ('a, 'c) roll = fun f g ->
  Roll (fun k  ->  unroll f (g -: k)) 


(* nope -- unifies to 1 type ! 
let rec (-:) = fun f g ->
  Roll (fun k  ->  unroll f (g -: k)) 
*)

The same code in Haskell requires type annotations

{-# LANGUAGE RankNTypes #-}

newtype Roll a b = Roll (Roll b a  -> b)
unroll (Roll f) = f

(-:) :: forall a b c. Roll b c -> Roll a b -> Roll a c 
(-:)  f g =  Roll (\k  ->  unroll f (g -: k))
polymorphism ocaml haskell
1 Answers

Universally quantifying all the type variables, as in the equivalent Haskell code, seems to work fine:

let rec (-:) : 'a 'b 'c. ('b, 'c) roll -> ('a, 'b) roll -> ('a, 'c) roll = fun f g ->
  Roll (fun k  ->  unroll f (g -: k))

val ( -: ) : ('b, 'c) roll -> ('a, 'b) roll -> ('a, 'c) roll = <fun>
user_79435640
Related