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.

At the moment import and export decls are accepted in any order, but they shouldn't be #91.


    ::= 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;+  } 

Import the symbols that are exported by another module.

The second form allows us to use the offside rule when writing the list of modules. For example:

import Data.List


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


    ::=  pragma ...

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


    ::=  foreign import  String  Var  ::  Type
     |   foreign import data  String  Con :: Kind
     |   foreign import data  String  Con

Foreign imports define the type of an external symbol.

Foreign data imports import a type name from C land. If no kind is given then the kind is assumed to be * (value types). For example:

foreign import data "String" String# :: % -> %
foreign import data "Int32"  Int32#


    ::= 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. An abstract type constructor has no associated data constructors.


    ::=  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 !. For example:

effect !Read    :: % -> !
effect !ReadT   :: * -> !
effect !Console :: !

Type inference involving user defined effect constructors of kinds other than ! 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

Region, effect and closure classes are abstract, as we do not define instance functions for them. Classes such as Mutable and Pure are defined as abstract classes in the the base libraries. For example:

class Mutable :: % -> +
class Pure    :: ! -> +

The return kind of an abstract class constraint must be + (witnesses).

Value type classes are as per Haskell, though we don't yet support default instances #90.


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


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


    ::=  Var  ::  Type