Higherorder kinds?
 Jacques Carette
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:  20061109 (21:44) 
From:  Jacques Carette <carette@m...> 
Subject:  Higherorder kinds? 
Is there any way to get higherorder 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/mlarchives/camllist/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 typelevel function, and the types F1 and F2 are used 'partially applied'. It is possible to expand this all out into firstorder, 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 linkedto 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