[Haskell-cafe] Polykinded promoted types

[Richard Eisenberg]

The problem I see here is that your List1 and List2 kinds are essentially untyped. These lists are allowed to store any types. For example, I can say `Cons1 'True (Cons1 Int Nil1)`, even though 'True and Int have different kinds. Your List3 won't allow such a construction. You're right that the kinds aren't isomorphic.

Does this help?

Richard

On Dec 9, 2014, at 6:09 PM, Gautier DI FOLCO <gautier.difolco at gmail.com> wrote:
> 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.