2014-12-17 22:54 GMT+01:00 Gautier DI FOLCO
Hello all,
I'm trying to port typeclasses to kind-level, here are my data types: -- newtype Fix f a = Fix (f (Fix f a)) -- data Mu f = In (f (Mu f)) data Fix (f :: k1 -> k0) (n :: k1) = Fx
data Maybe a = Nothing | Just a
If I try to create type families to represent Functors, I end up with this:
-- type family MapFix (f :: (* -> k) -> * -> k) a :: * where -- type family MapFix f a where type family MapFix (f :: (k0 -> k1) -> k0 -> k1) (a :: k2) :: * where MapFix f (Fix a n) = Fix (f a) (MapFix f n)
-- type family MapMaybe (f :: k -> k) (a :: Maybe k) :: Maybe k where -- type family MapMaybe f a where type family MapMaybe (f :: k0 -> k1) (a :: Maybe k0) :: Maybe k1 where MapMaybe f ('Just a) = 'Just (f a) MapMaybe f 'Nothing = 'Nothing
But I can't defined a single open type family for these two data types. I think I lack of parametric kinds, for example: `*k p*` could let me fit `*Maybe k*`. Currently, in the way I see kinds, on `*k0 -> k1*` allow me to parameterize kinds, but `*Maybe k*` doesn't fit.
I know that this is certainly unclear, don't hesitate to ask me for clarifications. I also know that my `*Fix*` sucks, any good idea on how to do it is welcome :) Also, if you have any links to have a deeper insight of Kinds it will save me from mental illness.
Thanks in advance for your help, Regards.
Hi all, I have pursued my investigations and end up with code: type family Morphism (a :: k0) (b :: k1) (c :: k2) :: * type instance Morphism t t t = t type instance Morphism A B A = B type instance Morphism B A B = A type instance Morphism D E (D a b) = E a b a :: Morphism A B A a = undefined -- Morphism A B A :: * -- = B b :: Morphism D E (D A B) b = undefined -- Morphism D E (D A B) :: * -- = forall (k :: BOX) (k :: BOX) (k :: BOX) (k :: BOX). E A B type family Morphism' (a :: k0) (b :: k1) (c :: k2) :: k3 type instance Morphism' t t t = t type instance Morphism' A B A = B type instance Morphism' B A B = A type instance Morphism' D E (D a b) = E a b a' :: Morphism' A B A a' = undefined -- Morphism' A B A :: k -- = forall (k :: BOX). Morphism' A B A They are two thing on which I want, if possible, an explanation: * Why I get a `forall k` when I declare a return polymorphic Kind? a Kind vs a' Kind * Why I get a `forall k` when I declare a parameter polymorphic Kind? a Kind vs b Kind Thanks, Regards.