MiniML Compiler

Glossary

• MiniML: MiniML is a tiny subset of the ML language (of Standard ML and OCaml fame). Different authors include/exclude different features. When we say MiniML, we mean the version as used in Warwick's POPL.

Colloquially, the MiniML grammar

Term grammar

The term grammar is the set of valid MiniML expressions. Everything is an expression in MiniML: there are no statements.

Whitespace is never significant, except for comments which stretch until newline.

Comments are specified by two dashes --.

e :=
  -- Literals
  x                        -- Variables.
  | True | False           -- Booleans.
  | 0 | 1 | 2 | ...        -- Numerics.

  -- Binders
  | let x = e1 in e2       -- Let bindings.
  | fn x . e               -- Functions (a.k.a. abstractions)

  -- Application
  | e1 e2                  -- Juxtaposition
  | e1 (e2)                -- Explicit

  -- Boolean fundamental ops
  | e1 and e2              -- Conjunction
  | not(e1)                -- Negation
  | if e0 then e1 else e2  -- Conditional
  
  -- Numeric fundamental ops
  | succ(e) | pred(e)      -- +1 and -1
  | e1 + e2                -- Sum
  | e1 == e2               -- Equal?
  | zero?(e)               -- Is zero?

  -- Pairs
  | <e1,  e2>              -- A pair of values (possibly different types)
  | fst(e) | snd(e)        -- Element-wise access to pairs

  -- Lists
  | nil                    -- The empty list
  | e1 :: e2               -- Cons, or list join
  | hd(e) | tl(e)          -- The first entry of the list & the remainder of the list

Type grammar

The type grammar specifies the list of valid types.

t := num
  | bool
  | t1 -> t2               -- The type of functions
  | t1 * t2                -- The type of pairs
  | t list                 -- The type of lists
  | y                      -- Type variables

Type schemes

Type schemes cannot be entered or used directly by the programmer, they are purely a tool of the type system.

Type schemes occur when implicit polymorphism is required by let bindings.

s := forall a . t

Agreed Grammar

e_top    := (e_top)
          | e_zeroth
e_zeroth := e_zeroth (e_first)
          | e_zeroth e_first
          | e_first
e_first  := e_first + e_second
          | e_second
e_second := e_second and e_third
          | e_third
e_third  := e_third :: e_fourth
          | e_fourth
e_fourth := e_fourth == e_fifth
          | e_fifth
e_fifth  := fn x . e_top
          | e_null
e_null   := x
          | c_bool
          | c_num
          | let x = e_top in e_top
          | not(e_top)
          | if e_top then e_top else e_top
          | succ(e_top)
          | <e_top,e_top>
          | fst(e_top)
          | snd(e_top)
          | nil
          | hd(e_top)
          | tl(e_top)
          | pred(e_top)

x = [a-zA-Z_][a-zA-Z1-9]*
c_bool = true | false
c_num = [0-9]+

Stretch goals

Recursion

In a general enough implementation, recursion would 'fall out' using the Y combinator.

However, it might be best (simpler, more performant, more ergonomic) to introduce the mu binder.

Based on the mu or Y binder in PCF, mu is akin to fn, but introduces an abstraction that, when called, recurses into the body of the mu binding.

See the sample definition of recursive Fibonacci.

Recursive bindings with letrec

Introduce a new keyword letrec, which has the same structure as let, but allows self-referential use of the bound variable in its definition.