Version française
Home     About     Download     Resources     Contact us    

This site is updated infrequently. For up-to-date information, please visit the new OCaml website at

Browse thread
Higher-order kinds?
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: 2006-11-09 (21:44)
From: Jacques Carette <carette@m...>
Subject: Higher-order kinds?
Is there any way to get higher-order kinds in Ocaml? 

While investigating some issues around partial evaluation (in 
MetaOCaml), we ran across this post from Jacques Guarrigue:

After a few emails between Ken Shan and Oleg Kiselyov, Ken produced a very elegant translation of this 'trick' into Haskell, which starts off thus:

data T f = Bool (f Bool) | Int (f Int) | Fun (T (F1 f))
newtype F1 f a = F1 { f1 :: T (F2 f a) }
newtype F2 f a b = F2 { f2 :: f (a -> b) }

Note how f in the above it a type-level function, and the types F1 and 
F2 are used 'partially applied'.  It is possible to expand this all out 
into first-order, but the end result is not pretty, to say the least!

Note that the rest of the Haskell code (classes and instances) can be 
translated into Functors and Modules [using that nice trick of having 
functors that produce module types, again thanks to Jacques G.].  The 
end result is definitely more verbose than the Haskell, but not 
desperately so. 


PS: rest of code, which just implements in an 'open' way what Jacques G. 
did using closed types in the email linked-to above

class Dynamic t where
    inj :: f t -> T f
    prj :: T f -> Maybe (f t)

instance Dynamic Bool where
    inj = Bool
    prj (Bool x) = Just x
    prj _ = Nothing

instance Dynamic Int where
    inj = Int
    prj (Int x) = Just x
    prj _ = Nothing

instance (Dynamic a, Dynamic b) => Dynamic (a -> b) where
    inj x = Fun (inj (F1 (inj (F2 x))))
    prj (Fun t) = prj t >>= prj . f1 >>= return . f2
    prj _ = Nothing