Designing TypeClassLang

[hrutvik]

Define TypeClassLang, a new source language with type classes.

TypeClassLang should have both typed and untyped variants - i.e. it can be in either "mode". This could be implemented by embedding option types in its syntax, or mirroring PureLang's :'a cexp type, or otherwise.

Programs

TypeClassLang programs consist of:

• data type and exception declarations
• type class and instance declarations
• top-level definitions, each with accompanying type signature

Expressions should mirror those of PureLang, except:

• TypeClassLang should contain only rich case syntax, not basic Case
  • This should effectively mirror NestedCase in PureLang
• Ideally we should incorporate pattern guards too
  • At first, we can translate only the subset of syntax that PureLang supports - later we can decide how to compile guards and so on, but the syntax should be designed with everything in mind from the start
• The syntax should contain a constructor for user type annotations (similar to that of CakeML)

Type class and instance declarations

• Type classes are applied to a single type variables only. Multi-parameter type classes are more complicated, and usually go hand-in-hand with "functional dependencies" (https://en.wikibooks.org/wiki/Haskell/Advanced_type_classes)
• Series of definitions ("methods") with type signatures and (optional) default operations.
• Need an idea of minimal definitions: GHC-style pragma, but stick to DNF for simplicity.
• May contain context (i.e. one or more superclasses) e.g.

  class (Eq a) => Ord a where
    compare              :: a -> a -> Ordering
    (<), (<=), (>=), (>) :: a -> a -> Bool
    max, min             :: a -> a -> a
  

• Method types are regular types, and so can have their own context
• Instances are similar: a series of method declarations.
  • May also be constrained by context, e.g. instance Eq a => Eq [a] where

[Gordon-Sau]

The TypeClassLang is currently defined in typeclass/typing/tcexpScript.sml in the typeclass branch. It is basically extending the original tcexp with type annotations (as option types). The Case are converted into NestedCase. For Let and LetRec, in order to support let-polymorphism, the explicit annotations are type scheme (includes the forall quantifiers ) instead of types.

Scope

To avoid complexity, it has been decided to limit the expressibility to the followings:

• Single parameter
• Class declaration must be in the form class A a, B a ... => C a (something like A (f a) is not allowed)
• The context (stuffs on the left of ==>) in Instance declaration must be in the form A a, B b, C c, that is a class name followed by a type variable used on the right hand side
• In order for termination, it is enforced that the right hand side must larger than the left hand side in instance declaration (in our case checking if the type on the right contains application should suffice)
• Default and minimal definitions are supported
• In order to support Functors and friends, we introduce VarTypeCons in typing/pure_typesScript.sml, for expressing something like f a where f is a type variable. As a consequence, a kind system is needed.
• The kind system is currently proposed to only contain * (Type) and ->, and kind inference would be the same as Haskell98, where kind that cannot inferred, are inferred as *. This will have some quirks that adding a method signature could affect the kind of the typeclass.
• We currently don't think it is required to support explicit kind signature at the moment, as even without it, the kind inference should still be powerful enough in most cases.

Plan

As kind inference is not the main part of the project, first we will assume the types are kind checked, when developing the semantics and dictionary translation, without developing the kind inference algorithm.