pure Type classes

A general issue to collect discussion and decisions on supporting type classes. Discussion so far has been along the following lines:

Introduction of a new, typed language between parsing and PureLang. Type inference would produce this by annotating an untyped AST (perhaps even one targeted directly by parsing). This language would need a semantics, permitting verification of compilation of type classes and extension of our end-to-end theorem.
Type classes would be compiled using a standard dictionary construction. PureLang etc. would therefore need some sort of record/dictionary support.

Many outstanding questions remain. For example, desired features (Haskell 98 type classes, or more?).

Usage of this new typed AST (TAST) brings other possibilities too.

A typed equational theory over TAST to simplify verification of intra-TAST transformations.
Introduction of a copy of GHC's core in between TAST and PureLang, i.e. compilation of TAST -> Core -> PureLang. We could then attempt to port various intra-Core optimisations from GHC.

Jun 23 '23 15:06 hrutvik

Following further discussion, we have created a "Type classes" milestone to plan an implementation of type classes in PureCake.

At a high level, we aim to follow "Type classes in Haskell" by Hall et al. by defining an untyped source language (TypeClassLang) with type class constructs, and giving its semantics via translation to a typed language and dictionary construction. They provide links to more complete formalisations which handle details critical to a full implementation.

Where we have design choices, our aim is to follow Haskell 98. This provides a significant (and well-known) subset of the features of modern Haskell type classes, while keeping things well-delimited and not overly complicated.

In summary, the steps are:

Define TypeClassLang, a new source language with type classes. This has both untyped and typed variants.
The typing rules of TypeClassLang will relate its untyped variant to its typed variant, i.e. specifying which annotations are valid and making overloading explicit. A new type inference algorithm must be implemented and proved sound with respect to these typing rules.
The semantics of TypeClassLang will be defined by translation to PureLang, necessitating dictionary construction. This translation will be specified as naively and cleanly as possible. Compilation should be defined much less naively and proved sound with respect to this specification.
The key top-level result should be: well-typed TypeClassLang code has a PureLang translation, which itself is well-typed (and so does not crash)

Note that we separate typing rules and translation, where Hall et al. specify them all at once. We must be careful not to duplicate work by splitting these up.

Sep 26 '23 15:09 hrutvik