Ahn, Ki Yung | 26 Oct 03:07 2012
Picon

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

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
Attachment (tmp.lhs): text/x-literate-haskell, 2320 bytes
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Ahn, Ki Yung | 26 Oct 04:10 2012
Picon

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

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
(Continue reading)

José Pedro Magalhães | 26 Oct 08:27 2012
Picon

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

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



_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Gmane