Higher-order kinds?

Higher-order kinds?

[Jacques Carette]

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:

http://caml.inria.fr/pub/ml-archives/caml-list/2006/09/05dcdcb7064cc73bfdfb756a419a9010.fr.html

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. 

Jacques

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