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:

- In order to avoid explosion of parentheses, we support standard precedences and short-cuts for expressions, types, and kinds. Thus we had to introduce multiple non-terminals for each of these syntactic categories, and as a result, the concrete grammar is longer and more complex than the underlying abstract syntax.
- On the other hand, we have kept the grammar simpler by avoiding special syntax for tuple types and terms. Tuples (both boxed and unboxed) are treated as ordinary constructors.
- All type abstractions and applications are given in full, even
though some of them (e.g., for tuples) could be reconstructed;
this means a parser for Core does not have to reconstruct
types.
^{[17]} - The syntax of identifiers is heavily restricted (to just alphanumerics and underscores); this again makes Core easier to parse but harder to read.

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 | non-recursive | ||

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 0x20-0x7E 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` |