Status of the Programatica Haskell front-end

Overall status

Abstract syntax

Structure, old version

data E e p ds t c    = ...	-- Expressions
data D e p ds t c tp = ...	-- Declarations
data P   p           = ...	-- Patterns
data T        t      = ...	-- Types

Recursion, old version

newtype HsExp  = Exp (E HsExp HsPat [HsDecl] HsType [HsType]
newtype HsDecl = Dec (D HsExp HsPat [HsDecl] HsType [HsType] HsType
newtype HsPat  = Pat (P HsPat)
newtype HsType = Typ (T HsTyp)

Notes on extensibility

The choice of parameters seems somewhat ad-hoc, but is presumably based on some foreseen need for extensibility.

• Identifiers are not a parameter in the types, and they are not manipulated by the general map, acc & seq functions.
• The do syntax is not a parameter in the types, so e.g. the O'Haskell extensions of the do notation can not be accomodated in an elegant way.
• The type for the do syntax, HsStmt, is recursive...

Identifiers

type Id = String

newtype Module = Module String

data HsName = Qual Module Id | UnQual Id

data HsIdent = HsVar HsName | HsCon HsName

Structure, current version

data EI i e p ds t c    = ...	-- Expressions
data DI i e p ds t c tp = ...	-- Declarations
data PI i   p           = ...	-- Patterns
data TI i        t      = ...	-- Types

data HsIdentI i =  HsVar i | HsCon i	-- Identifiers

Backwards compatiblity

type E = EI HsName
mapE = mapEI id

type HsIdent = HsIdentI HsName
...

Recursion, current version

newtype HsExpI  i = Exp (EI i (HsExpI i) (HsPatI i) [HsDeclI i] (HsTypeI i) [HsType i]
newtype HsDeclI i = Dec (DI i (HsExpI i) (HsPatI i) [HsDeclI i] (HsTypeI i) [HsTypeI i] (HsTypeI i)
newtype HsPatI  i = Pat (PI i (HsPatI i))
newtype HsTypeI i = Typ (TI i (HsTypI i))

Backwards compatibility

type HsExp = HsExpI HsName
...

The price of abstracting away from the type of identifiers

It would have been easier if one could add a type parameter to a module instead of adding it to every definition in the module...

Generalizing a type class

Before

class DefinedNames def where
  definedNames :: def -> [(HsIdent,IdType)]

After

class DefinedNames i def | def->i where
  definedNames :: def -> [(HsIdentI i,IdTy i)]

(See modules DefinedNames, DefinedNamesBaseStruct, DefinedNamesBase.)

Hiding the extra tagging

Old version

hsId n                      = Exp $ HsId n
hsLit lit                   = Exp $ HsLit lit
hsApp e1 e2                 = Exp $ HsApp e1 e2
hsLambda pats e             = Exp $ HsLambda pats e
...

Hiding the extra tagging, current version

Current version

class HasBaseStruct rec base | rec->base where
  base :: base -> rec

hsId n                      = base $ HsId n
hsLit lit                   = base $ HsLit lit
hsApp e1 e2                 = base $ HsApp e1 e2
hsLambda pats e             = base $ HsLambda pats e
...

This makes the constructor functions reusable in extensions to the base language. Code duplication is reduced, but there is a risk of introducing ambiguity...

Parsing

Parsing Haskell, problems

• The layout rules require interaction bewtween the lexer and the parser.
• The precedence and associativity of infix operators is not easily available.
  • Infix declarations can be put wherever a type signature is allowed, even after a use of the operator.
  • Fixity follows the scope of a specific binding, so you have to know which identifiers are in scope and where they were originally defined.
  • Determining the fixity of imported operators requires a full-fledged implementation of the module system!

Parsing Haskell, solutions

• Layout: the lexer state is part of the parser monad.
• Infix operators: parsing is done in stages:
  • A parse tree is constructed as if all operators had the default fixity. Parentheses in expressions are preserved.
  • The module structure is analyzed. This tells us (amongst other things) what is in scope on the top level of each module. Infix applications are rewritten (reassociated) according to the fixity of operators. The traversal of the syntax tree uses an environment to keep track of what is in scope locally.
  The class ReAssoc as been introduced, make the reassociation functions reusable. See modules ReAssoc, ReAssocBaseStruct, ReAssocBase.

Using the Haskell parser

Static analysis

For the type checker, we need one more piece of information of this kind...

Free names

class FreeNames i t | t -> i where
  freeNames :: t -> [(HsIdent i,NameSpace)]

Strongly connected components

scc :: (Eq a) => Graph a -> [Graph a]
sccEq :: EqOp a -> Graph a -> [Graph a]
type Graph a = Assoc a [a]

A reusable wrapper function, that applies scc to declarations is used in the type checker:

sccD :: (Eq i, FreeNames i d, DefinedNames i d) => [d] -> [[d]]

Type checking, overview

• It is designed to be extensible. (In what dimensions?)
• It performs the dictionary translation.
• The output can also be decorated with inferred types.

• Thorough kind checking (but the type checker is still sound).
• Making use of the superclass relation in context reduction.
• Checking inferred types agains given type signatures (entailment).

Types used in the type checker

type Type i = HsTypeI i
type Pred i = Type i
data Qual i t = [Pred i] :=> t
data Scheme v = Forall [v] (Qual v (Type v))
data Typing x t = x :>: t deriving (Eq,Show)
type Assump i = Typing (HsIdentI i) (Scheme i)
type Typed i x = Typing x (Type i)
newtype Subst i = S [(i,Type i)] deriving (Show)

data Kind = K (K Kind) | Kvar KVar
newtype KVar = KVar Int

class TypeVar v => Types v t | t->v where
  tmap :: (Type v->Type v) -> t -> t
  apply :: Subst v -> t -> t
  tv :: t -> Set v

  apply = tmap . applySubst

Type Inference Monad

newtype IM i c ans = ...
type TI i = IM i (TypeConstraint i)
type KI i = IM i KindConstraint

• environments,
• name supply,
• constraint collection and
• error handling.

class Fresh a where
  fresh :: IM i c a

Generic Unification

type Equation t = (t,t)
type Equations t = [Equation t]
type Substitution v t = [(v,t)]

class (Show term,Eq var) => Unifiable term var | term -> var where
  topMatch :: Equation term -> Maybe (Equations term)
  isVar :: term -> Maybe var
  subst :: Substitution var term -> term -> term

unify :: (Monad m,Unifiable t v) => Equations t -> m (Substitution v t)
unify = ... -- 19 lines, purely functional implementation