Epigram Core Syntax

It seems like a good idea to document Epigram’s core syntax somewhere other than its parser, so here goes. Remember, this is fully explicit, no frills, no crafty elaboration. There are some organising principles behind this syntax:

  • Evaluation should not require typechecking. Whether or not it’s wise, it must be possible to read in a term and run it. This means that information which could sometimes be filled in by a typechecker is made explicit anyway.
  • We separate
    • synth terms, whose types may be synthesised, from
    • check terms, which may only be checked against a known type but are perhaps less noisy.
  • We adopt a postfix spine representation of all elimination forms, such as application, projection and so on.

Grammar

\textit{Synth}\;:=

  • \texttt{(}\textit{Synth}\texttt{)}    parenthesized term
  • \textit{Check} \texttt{:} \textit{Check}    explicictly typed term
  • [Unparseable or potentially dangerous latex formula. Error 2 ]    variable reference
  • [Unparseable or potentially dangerous latex formula. Error 3 ]    elimination form
  • \textit{TBop}\:\textit{Icit}\:\textit{UId} \:\texttt{:}\:\textit{Check}\:\texttt{=>}\textit{Check}    binder type \textit{TBop}\in\{\texttt{all},\texttt{ex},\texttt{W}\}
  • [Unparseable or potentially dangerous latex formula. Error 3 ]    equality type
  • [Unparseable or potentially dangerous latex formula. Error 3 ]    datatype family
  • \texttt{lam}\:\textit{Icit}\:\textit{UId}\:\texttt{:} \:\textit{Check}\:\texttt{=>}\textit{Synth}    labelled lambda
  • \texttt{(} \textit{Icit}\:\textit{UId} \:\texttt{=>} \textit{Synth} \texttt{;} \textit{Check} \texttt{:} \textit{Check} \texttt{)}    labelled dependent pair
  • \texttt{refl \{} \textit{Check} \texttt{:} \textit{Check} \texttt{\}}    reflexive equality proof
  • \texttt{ext \{} \textit{Check} \texttt{\}} \: \textit{Check}    extensionality proof

I give up.

Leave a Reply