[Haskell-cafe] Parametric kinds

[Gautier DI FOLCO]

2014-12-17 22:54 GMT+01:00 Gautier DI FOLCO <gautier.difolco at gmail.com>:

> 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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20141221/2c02c6c8/attachment.html>