|Version 16 (modified by ia0, 4 years ago) (diff)|
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).
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.
User's Guide and Examples
There is a user guide available on the haskellwiki explaining how to build the compiler and how to use the extension.
The GHC branch is called ghc-kinds. There is also a branch with the same name for haddock and the testsuite. The implementation will follow these steps (in bold is the first phase (parser, renamer, type checker, ...) that does not work):
- Promotion of Haskell98 data types of kind star: *.
- Promotion of Haskell98 data types of first order kind: * -> .. * -> *. It involves kind polymorphism.
- [theory design] Kind polymorphic data types, type families, and type classes. This step needs some design choices about kind polymorphism.
- Singleton types.
- Built-in types.
- Extend TyCon with PromotedDataTyCon to have data constructors in type constructors.
- Extend the parser, renamer, type and kind checker, and core-lint accordingly.
Not 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.
- Use HsDocContext instead of SDoc to track renaming context.
- Kind check and type check by strongly connected components, instead of kind checking the whole module, and then type checking it. This implies that some modules now need additional kind annotations (since each strongly component gets zonkTcKindToKind before going to the next one).
- Rename KindVar which is used during type checking into MetaKindVar.