[Haskell-cafe] Polykinded promoted types

[Gautier DI FOLCO]

2014-12-09 2:35 GMT+01:00 Richard Eisenberg <eir at cis.upenn.edu>:

> While it's true that Maybe's kind is (* -> *), there still may be a better
> answer to your question, which asks, "Is there a way to get a polykinded
> promoted type?" Maybe isn't polykinded, but it's also not promoted. With
>
> data Proxy a = P
>
> we get (Proxy :: k -> *). But that's not promoted either. On the other
> hand we have ('Just :: k -> Maybe k), which is promoted and polykinded, but
> maybe not what you want.
>
> Does this help?
>

Hello,

In fact my problem occurs when I try to describe (Iso)morphisms:
type Cons1 (e :: k1) (n :: k2) = Product e n
type Nil1 = Void

type Cons2 e n = Just (Product e n)
type Nil2 = Nothing

data List3 a = Nil3 | Cons3 a (List3 a)

type family List1_List2 a where
  List1_List2 (Cons1 a b) = Cons2 a (List1_List2 b)
  List1_List2 Nil1 = Nil2

type family List2_List1 a where
  List2_List1 (Cons2 a b) = Cons1 a (List2_List1 b)
  List2_List1 Nil2 = Nil1

type family List2_List3 a where
  List2_List3 (Cons2 a b) = Cons3 a (List2_List3 b)
  List2_List3 Nil2 = Nil3

type family List3_List2 a where
  List3_List2 (Cons3 a b) = Cons2 a (List3_List2 b)
  List3_List2 Nil3 = Nil2

type List1_List3 a = List2_List3 (List1_List2 a)
type List3_List1 a = List2_List1 (List3_List2 a)

There is an Isomorphism between List1 and List2 (List1_List2 (List2_List1
a) == a and List2_List1 (List1_List2 a) == a) but not between List3 and the
others due to it's * kind.

Thanks,
Regards.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20141210/5a2d4f5c/attachment.html>