Browse thread
Higher-order 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: | 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: 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