Problems translating Conor McBride's talk into Haskell + DataKind + KindPoly

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
3 messages Options
Reply | Threaded
Open this post in threaded view
|

Problems translating Conor McBride's talk into Haskell + DataKind + KindPoly

Ahn, Ki Yung
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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

tmp.lhs (2K) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: Problems translating Conor McBride's talk into Haskell + DataKind + KindPoly

Ahn, Ki Yung
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
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe



_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: 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 <[hidden email]> 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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe



_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe