[Haskell-cafe] Problems translating Conor McBride's talk into Haskell + DataKind + KindPoly
Ahn, Ki Yung
kyagrd at gmail.com
Fri Oct 26 04:10:13 CEST 2012
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
More information about the Haskell-Cafe