wiki:GhcKinds

Version 10 (modified by ia0, 3 years ago) (diff)

fix hoopl link

GHC Kind level

This page gives the theory, implementation overview and details about GHC's kind level. This work is related to Conor's SHE system and will be related to Iavor's work on TypeNats to deal with primitive types (promoted Int and Char).

Theory

We use the mechanism of promotion to lift a data type to the kind level. This gives access at the type level to the data constructors, and at the kind level to the type constructor. Not all data types can be promoted; for example, GADTs or data types with higher-order kinds cannot be promoted. We add kind polymorphism to allow promotion of polymorphic data constructors (like Nil or Cons).

More details can be found in this theory pdf.

Examples

Examples of reimplementation of existing Haskell librairies can be found in this examples pdf. I use a repository for what works and what does not https://github.com/ia0/GhcKindsExamples.

Implementation

The GHC branch is called ghc-kinds. There is also a Haddock branch with the same name. Hoopl needs a kind annotation available on a branch in http://darcs.haskell.org/git-mirrors/hoopl/.

The implementation will follow these steps (in bold is the first phase (parser, renamer, type checker, ...) that does not work):

  1. Promotion of Haskell98 data types of kind star: *.
  2. [] Kind polymorphism in Core.
  3. Promotion of Haskell98 data types of first order kind: * -> .. * -> *.
  4. Kind polymorphic data types, type families, and type classes.
  5. Singleton types.
  6. Built-in types.

Promotion-related changelog:

  • Change the kind representation in HsSyn from Kind to LHsKind name adding some PostTcKind when necessary.
    • Rename rnHsType into rnHsTyKi and parametrize with a boolean to know if we are renaming a type or a kind.
  • Allow promoted data and type constructors:
    • Extend the parser to allow optionally ticked names as atoms in types and kinds.
    • Extend HsType name with HsPromotedConTy name to represent ticked names.
    • Extend the renamer to handle implicit promotion.
    • Extend TyCon with PromotedDataTyCon and PromotedTypeTyCon to represent promoted data and type constructors.
    • Extend the type checker accordingly.
  • Rename KindVar which is used during type checking into MetaKindVar, since we will add kind variables later.

Not promotion-related changelog:

  • Use HsDocContext instead of SDoc to track renaming context.