10.2. External Grammar of Core

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₁ ∣ pat₂	choice
`fibonacci`	terminal syntax in typewriter font

Module	module	→	`%module` mident { tdef ; }{ vdefg ; }
Type defn.	tdef	→	`%data` qtycon { tbind } `= {` [ cdef {`;` cdef } ] `}`	algebraic type
Type defn.	tdef	∣	`%newtype` qtycon qtycon { tbind } `=` ty	newtype
Constr. defn.	cdef	→	qdcon { `@` tbind }{ aty }⁺
Value defn.	vdefg	→	`%rec {` vdef { `;` vdef } `}`	recursive
	vdefg	∣	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
Argument	arg	∣	aexp	value argument
Case alt.	alt	→	qdcon { `@` tbind }{ vbind } `->` exp	constructor alternative
		∣	lit `->` exp	literal alternative
		∣	`%_ ->` exp	default alternative
Binder	binder	→	`@` tbind	type binder
Binder	binder	∣	vbind	value binder
Type binder	tbind	→	tyvar	implicitly of kind *
Type binder	tbind	∣	`(` 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
	char	∣	`\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
Kind	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`

These choices are certainly debatable. In particular, keeping type applications on tuples and case arms considerably increases the size of Core files and makes them less human-readable, though it allows a Core parser to be simpler.