[Haskell-cafe] Polykinded promoted types

[Richard Eisenberg]

On Dec 10, 2014, at 12:31 PM, Gautier DI FOLCO <gautier.difolco at gmail.com> wrote:

> 2014-12-10 16:21 GMT+01:00 Richard Eisenberg <eir at cis.upenn.edu>:
> 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 ? 

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...

Richard
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20141210/a65289c5/attachment.html>