2014-12-09 0:04 GMT+01:00 Taylor Hedberg :

$ ghci -XDataKinds -XKindSignatures Prelude> data K = K Prelude> data Foo (a :: K) = Foo Prelude> :kind Foo Foo :: K -> *

Note that types with kinds other than * are uninhabited, so you can't write a version of Maybe with that kind (because the Just constructor would require a value that can't exist).

That was quick (and that is that I feared). Thanks anyway.

2014-12-09 2:35 GMT+01:00 Richard Eisenberg :

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.

2014-12-10 16:21 GMT+01:00 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?

Yes, it does. I guess that there is no way to escape ?

2014-12-10 21:32 GMT+01:00 Richard Eisenberg :

Escape what, exactly? I'm not sure what your end goal is, so I don't know what you're trying to escape from.

Is this what you want?

data List where Nil :: List Cons :: a -> b -> List

type Foo = Cons True (Cons "x" (Cons () Nil))

That works, but isn't very useful in practice, I don't think...

Escape from this trouble. When I try to apply a type family on it, I get a forall k, isn't there a way to "set" it? Thanks, Regards.