In designing the external grammar, we have tried to strike a balance among a number of competing goals, including easy parseability by machines, easy readability by humans, and adequate structural simplicity to allow straightforward presentations of the semantics. Thus, we had to make some compromises. Specifically:
We use the following notational conventions for syntax:
[ pat ]  optional 
{ pat }  zero or more repetitions 
{ pat }^{+}  one or more repetitions 
pat_{1} ∣ pat_{2}  choice 
fibonacci

terminal syntax in typewriter font 
Module  module  →  %module mident { tdef ; }{ vdefg ; } 

Type defn.  tdef  →  %data qtycon { tbind } = { [ cdef {; cdef } ] } 
algebraic type 
∣  %newtype qtycon qtycon { tbind } = ty 
newtype  
Constr. defn.  cdef  →  qdcon { @ tbind }{ aty }^{+} 

Value defn.  vdefg  →  %rec { vdef { ; vdef } } 
recursive 
∣  vdef  nonrecursive  
vdef  →  qvar :: ty = exp 

Atomic expr.  aexp  →  qvar  variable 
∣  qdcon  data constructor  
∣  lit  literal  
∣  ( exp ) 
nested expr.  
Expression  exp  →  aexp  atomic expresion 
∣  aexp { arg }^{+}  application  
∣  \ { binder }^{+} > exp 
abstraction  
∣  %let vdefg %in exp 
local definition  
∣  %case ( aty ) exp %of vbind { alt { ; alt } } 
case expression  
∣  %cast exp aty 
type coercion  
∣  %note " { char } " exp 
expression note  
∣  %external ccall " { char } " aty 
external reference  
∣  %dynexternal ccall aty 
external reference (dynamic)  
∣  %label " { char } " 
external label  
Argument  arg  →  @ aty 
type argument 
∣  aexp  value argument  
Case alt.  alt  →  qdcon { @ tbind }{ vbind } > exp 
constructor alternative 
∣  lit > exp 
literal alternative  
∣  %_ > exp 
default alternative  
Binder  binder  →  @ tbind 
type binder 
∣  vbind  value binder  
Type binder  tbind  →  tyvar  implicitly of kind * 
∣  ( tyvar :: kind ) 
explicitly kinded  
Value binder  vbind  →  ( var :: ty ) 

Literal  lit  →  ( [ ] { digit }^{+} :: ty ) 
integer 
∣  ( [ ] { digit }^{+} % { digit }^{+} :: ty ) 
rational  
∣  ( ' char ' :: ty ) 
character  
∣  ( " { char } " :: ty ) 
string  
Character  char  →  any ASCII character in range 0x200x7E except 0x22,0x27,0x5c  
∣  \x hex hex 
ASCII code escape sequence  
hex  →  0∣…∣9 ∣a ∣…∣f  
Atomic type  aty  →  tyvar  type variable 
∣  qtycon  type constructor  
∣  ( ty ) 
nested type  
Basic type  bty  →  aty  atomic type 
∣  bty aty  type application  
∣  %trans aty aty 
transitive coercion  
∣  %sym aty 
symmetric coercion  
∣  %unsafe aty aty 
unsafe coercion  
∣  %left aty 
left coercion  
∣  %right aty 
right coercion  
∣  %inst aty aty 
instantiation coercion  
Type  ty  →  bty  basic type 
∣  %forall { tbind }^{+} . ty 
type abstraction  
∣  bty > ty 
arrow type construction  
Atomic kind  akind  → 
*

lifted kind 
∣ 
#

unlifted kind  
∣ 
?

open kind  
∣  bty :=: bty 
equality kind  
∣  ( kind ) 
nested kind  
Kind  kind  →  akind  atomic kind 
∣  akind > kind 
arrow kind  
Identifier  mident  →  pname : uname 
module 
tycon  →  uname  type constr.  
qtycon  →  mident . tycon 
qualified type constr.  
tyvar  →  lname  type variable  
dcon  →  uname  data constr.  
qdcon  →  mident . dcon 
qualified data constr.  
var  →  lname  variable  
qvar  →  [ mident . ] var 
optionally qualified variable  
Name  lname  →  lower { namechar }  
uname  →  upper { namechar }  
pname  →  { namechar }^{+}  
namechar  →  lower ∣ upper ∣ digit  
lower  →  a ∣ b ∣ … ∣ z ∣ _ 

upper  →  A ∣ B ∣ … ∣ Z 

digit  →  0 ∣ 1 ∣ … ∣ 9 