Version 5 (modified by 6 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`

).

## 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. All data types cannot be promoted. For examples GADTs or data types with higher-order kinds. 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.

## Implementation

The branch is called `ghc-kinds`

. Its current state is:

ADT promotion | Primitives | Kind polymorphism | |

Parser | Yes | Yes | Yes |

Renamer | In progress | Yes | |

Typechecker |

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.

- Rename
- Allow promoted data and type constructors:
- Extend the parser to allow ticked names like
`'Zero`

or`'Nat.Succ`

as atoms in types. - Extend the parser to allow
*optionally*ticked names like`Nat`

or`'Bool`

as atoms in kinds. - Extend
`HsType name`

with`HsPromotedConTy name`

to represent ticked names. - Extend
`TyCon`

with`PromotedDataTyCon`

to represent promoted data constructors.

- Extend the parser to allow ticked names like
- 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.

The stage1 compiler does not work, since there is some `undefined`

s in the typechecker. So you won't be able to build a stage2 or even run validate. This is the first priority.