Module

Module
    ::= module  ModuleId  where  ModuleBody
     |  ModuleBody 

ModuleBody
    ::= {  ExportDecl;*  ImportDecl;*  TopDecl;+  }

Modules start with an optional module identifier, followed by a list of export and import declarations. Export declarations must come before import declarations.

Although we use semicolons as terminators instead of separators, in all cases the parser will accept a missing semicolon before a closing brace.

ExportDecl

ExportDecl
    ::= export  Var
     |  export type  Con
     |  export region  RVar
     |  export effect  ECon
     |  export class   Con 

When there is an explicit export list, only those identifiers mentioned are exported from the module. If there is no export list then all identifiers are implicitly exported.

ImportDecl

ImportDecl
    ::=  import  ModuleId
     |   import  {  ModuleId;+  } 
     |   foreign import  String  Var  ::  Type

Foreign imports define the type of an external symbol.

TopDecl

TopDecl
    ::=  Pragma
     |   InfixDecl
     |   TypeKind
     |   TypeSynonym
     |   DataDecl
     |   EffectDecl
     |   RegionDecl
     |   ClassDecl
     |   InstanceDecl
     |   ProjectionDecl
     |   TypeSig
     |   Binding

Pragma

Pragma
    ::=  pragma ...

These should be removed in favor of Haskell/GHC style pragmas #86.

InfixDecl

InfixDecl
    ::= infixl  Int  Symbol;+                  -- left associative
     |  infixr  Int  Symbol;+                  -- right associative
     |  infix   Int  Symbol;+                  -- non-associative

Sets the precedence and associativity of an infix binary operator.

TypeKind

TypeKind 
    ::=  type  Con  ::  Kind 

Sets the kind of an abstract value type constructor.

TypeSynonym

TypeSynonym
    ::=  type  Con  TyVar+  =  Type 

Type synonyms are not implemented yet #16.

DataDecl

DataDecl
    ::=  data  Con  TyVar*  =  CtorDecl  |CtorDecl+

CtorDecl
    ::=  Con  SimpleType*
     |   Con  {  DataField;+  }

DataField
    ::=  SimpleType                                  -- unnamed primary field
     |   Var  ::  SimpleType                         -- named primary field 
     |   .  Var  ::  SimpleType  =  Exp              -- secondary field with initial value

As we want to support type constraints on constructors #87, and constraints are separated by a commas, we separate data fields with semicolons. This is a difference from Haskell, but should allow us to use the offside rule when listing the fields of a constructor #88.

Data type definitions are elaborated, so you don't need to mention all the region, effect and closure variables in the types of constructor arguments. If the type of a constructor argument is missing a region, effect or closure variable, then the corresponding argument of the surrounding type constructor is used.

Primary fields become arguments of the constructor function, but secondary fields do not. For example, the following declaration:

data Animal
       = Cat   { name :: String; weight :: Int }
       | Mouse { name :: String; age :: Int; .length :: Int = 5 }

Generates the following (elaborated) constructors:

Cat   :: forall %r1. String %r1 -> Int %r1 -> Animal %r1
Mouse :: forall %r1. String %r1 -> Int %r1 -> Animal %r1

Note that Cat has an argument for its name and weight of lives left, but Mouse only has arguments for its name and age. The length field is initialized to 5 when a Mouse is constructed. Secondary fields can still be accessed via the projection syntax:

do  fred  = Mouse "Fred" 3
    print fred.name          -- prints "Fred"
    print fred.length        -- prints "5"

    fred.length := 6         -- changes Fred's length
    print fred.length        -- prints "6"

EffectDecl

EffectDecl 
    ::=  effect  ECon  ::  Kind  

Defines a new effect constructor and sets its kind. The result kind of the constructor must be !.

Inference involving effect constructors of kinds other than ! and (% -> !) is not well tested #89.

RegionDecl

RegionDecl
    ::=  region  RVar  (:-  TyConstraint  ,TyConstraint*)?

Defines a top-level (global) region.

Although explicitly binding top-level region variables is not nessesary, it can be useful to define the constraints on a global region in a single place in the source file, instead of trying to repeat them in each type signature that uses it. For example:

region %r :- Const %r

pi :: Float %r
pi = 3.1415926535

e :: Float %r
e = 2.71828183

ClassDecl

ClassDecl
    ::=  class  Con  ::  Kind                             -- abstract class constraint
     |   class  Con  TyVar+  where  {  TypeSig;+  }       -- value type class definition

The return kind of abstract class constraints must be +. We don't yet support default instances in type class declarations #90.

InstanceDecl

InstanceDecl
    ::=  instance  Con  SimpleType+  where  {  Binding;+  }

ProjectionDecl

ProjectionDecl
    ::=  project  Con  SimpleType*  where  {  (TypeSig|Binding)+  }    -- projection dictionary
     |   project  Con  SimpleType*  with   {  Var+  }                  -- projection punning

The first form defines some projection functions associated with a given type. Presently, all projections associated with a type must be declared in the same projection declaration and in the same source module, but there is a plan to relax this #7.

If two projection dictionaries are defined for types that overlap, eg List Int and List a, then the result is currently undefined. There is a ticket to fix this #40.

The projection punning syntax imports bindings at top level into the projection name space. For example:

project Set a with { insert; delete; size }

Is equivalent to

project Set a where { insert = insert; delete = delete; size = size }

This is useful when implementations of insert, delete and size are in the current module, but only the type Set is exported. All projections associated with a certain type are exported when the type is.

TypeSig

TypeSig
    ::=  Var  ::  Type