[Haskell-cafe] Problems translating Conor McBride's talk into Haskell + DataKind + KindPoly

[José Pedro Magalhães]

Hi,

Please use GHC 7.6 for experimenting with PolyKinds/DataKinds; the
implementation in 7.4 was not fully complete. Your code compiles fine in
7.6.


Cheers,
Pedro

On Fri, Oct 26, 2012 at 3:10 AM, Ahn, Ki Yung <kyagrd at gmail.com> wrote:

> Promotion works for user defined lists such as
>
> data List a = Nil | Cons a (List a)
>
> And, if I use (List Bool) instead of [Bool] everything works out.
> It's only the Haskell list type constructor [] is being a problem.
>
> In the "Giving Haskell a promotion" paper, it says that Haskell lists are
> "natively promoted". I believe this means that it is treated specially
> somehow. I don't know how it is implemented but what GHC 7.4.1 does
> specially for Haskell lists has some problems. So, it's clearly not a
> limitation of DataKind and PolyKind extension, but that special routine for
> [] is the issue.
>
> I might have to write bug report.
>
>
> On 2012년 10월 25일 18:07, Ahn, Ki Yung wrote:
>
>> Most part of Conor's talk at ICFP, until just before the last stage
>> where he heavily uses true value dependency for compiler correctness all
>> the code seemed to be able to translate into Haskell with the new hot
>> DataKinds and PolyKinds extension.
>>
>> I tried it in GHC 7.4.1 and it was possible to do it, but I got stuck
>> and I had to make the generic list structure mono-kinded with kind
>> signatures rather not use the PolyKinds extension.
>>
>> I wonder if this is just a but of GHC 7.4.1's implementation of
>> PolyKinds, or a limitation of the DataKind design.
>>
>> I attached a literate Haskell script with this message that illustrates
>> this problem.
>>
>> Thanks in advance for any comments including whether it runs in later
>> versions or still has problems, and discussions about the DataKinds and
>> PolyKinds extension.
>>
>> Ki Yung
>>
>>
>> ______________________________**_________________
>> Haskell-Cafe mailing list
>> Haskell-Cafe at haskell.org
>> http://www.haskell.org/**mailman/listinfo/haskell-cafe<http://www.haskell.org/mailman/listinfo/haskell-cafe>
>>
>
>
>
> ______________________________**_________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/**mailman/listinfo/haskell-cafe<http://www.haskell.org/mailman/listinfo/haskell-cafe>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20121026/e79f0353/attachment.htm>