Version 8 (modified by benl, 8 years ago)



    ::= module  ModuleId  where  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.


    ::= 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.


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

Foreign imports define the type of an external symbol.


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


    ::=  pragma ...

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


    ::= 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.


    ::=  type  Con  ::  Kind 

Sets the kind of an abstract value type constructor.


    ::=  type  Con  TyVar+  =  Type 

Type synonyms are not implemented yet #16.


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

    ::=  Con  SimpleType*
     |   Con  {  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          -- prints "Fred"
    print fred.length        -- prints "5"

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


    ::=  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.


    ::=  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


    ::=  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.