PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

[Iavor Diatchki]

Hello,

On Tue, Sep 18, 2012 at 12:10 AM, Simon Peyton-Jones
<simonpj at microsoft.com>wrote:

>
> The technically-straightforward thing to do is to add kind application,
> but that's a bit complicated notationally.
> http://hackage.haskell.org/trac/ghc/wiki/ExplicitTypeApplication   Does
> anyone have any other ideas?
>
>
I think that the right way to proceed would be to add explicit syntax for
kind abstraction and application (which, I imagine, we already have
internally in GHC).  As for the concrete syntax, I prefer the explicitly
annotated form, even if the ":: Kind" part is treated completely
syntactically for the moment, because the notation seems compatible with
future generalizations that we might want to do (e.g., the work that
Stephanie, Richard, Connor, and Adam are doing).  So the source Haskell
might look something like this:

type family SingRep (a :: Kind)
type instance SingRep (Nat :: Kind) = Integer

class SingE (a :: Kind) where ...


-Iavor
PS: I just modified the ExplicitTypeApplication wiki page to reflect more
accurately the singletons example.  For those who've seen the old page:  I
changed the 'Sing' data family example, because that family needs an actual
type parameter---it is not enough to just have a kind parameter (the reason
being that we want to write things like "Sing 5", where "5" is a type).
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20120918/8b29c0be/attachment.htm>