Typing rules for TypeClassLang

[hrutvik]

Define inductive typing (elaboration) rules for TypeClassLang

These effectively describe valid annotations for an untyped TypeClassLang program - ill-typed programs are those without any valid annotations. This requires a declarative specification of how to resolve overloading.

We should carefully design exactly what the type annotations are: they should not be required for all sub-expressions, and must be sufficient to make dictionary construction "easy". In other words, when we specify the semantics of TypeClassLang via dictionary construction, a well-annotated input program should provide all the information on exactly which dictionaries to construct where - there should be no duplication of overloading resolution in the specification of the typing rules and semantics.

Some further considerations are below.

Types and kinds

TypeClassLang types must extend those of PureLang to incorporate type class constraints (the "context").
TypeClassLang must also have a kind system, (e.g. to consider Functor). We will use Haskell's simple * kind and -> kind
constructor.

• Contexts may contain only typeclasses applied to single type variables
  (i.e. not Eq [a], but Eq a fine).
• Data type declarations may incorporate class constraints; ML-style exceptions remain monomorphic. For example:

  data Eq a => Set a = NilSet | ConsSet a (Set a)

  This introduces type constructor Set :: * -> *, and constructors NilSet :: ∀a. Set a and ConsSet :: ∀a. Eq a => ....
  Note how the Eq a context is only applied where it is required, i.e. where a appears in the arguments of the constructor.
• Partial application is a key feature of kinds - our formalisation should not be overly arity-aware.

Type classes

Declarations

• Note that top-level definitions can be used in default operations - type classes exist at the same top-level scope.
• The hierarchy of superclasses must be acyclic.
• All overloading used within the class/instance declaration itself must appear in the context (or in method contexts, below)
• Methods can have their own context (!) as long as they don't constrain the type variable of the class declaration. For example:

  class C a where
    m                     :: Show b => a -> b

• Method names must be unique

Instances

• Each instance must define a minimal set of methods described by the class declaration, or it is invalid.
• Instance resolution must be deterministic: for any given call-site, there must be only one instance which matches.
  Haskell permits overlapping instance declarations, but forbids a call-site which causes ambiguity. We might prefer to check for ambiguity at declaration time.
• "ambiguous types" are also an issue:
  "a type ∀u. cx => t where a type variable in u occurs in cx but not in t", e.g.

  let x = read "..." in show x
  -- show :: ∀a. Show a => a -> String
  -- read :: ∀a. Read a => String -> a