Additional information

• Images
• Videos
• Documents
• Books
• Articles

Syntax

Epigram uses a two-dimensional, natural deduction style syntax, with versions in LaTeX and ASCII. Here are some examples from The Epigram Tutorial:

Examples

The natural numbers

The following declaration defines the natural numbers:

( ! ( ! ( n : Nat ! data !---------! where !----------! ; !-----------! ! Nat : * ) !zero : Nat) !suc n : Nat)

The declaration says that Nat is a type with kind * (i.e., it is a simple type) and two constructors: zero and suc. The constructor suc takes a single Nat argument and returns a Nat. This is equivalent to the Haskell declaration "data Nat = Zero | Suc Nat".

In LaTeX, the code is displayed as:

d a t a _ ( N a t : ⋆ ) w h e r e _ ( z e r o : N a t ) ; ( n : N a t s u c   n : N a t ) {\displaystyle {\underline {\mathrm {data} }}\;\left({\frac {}{{\mathsf {Nat}}:\star }}\right)\;{\underline {\mathrm {where} }}\;\left({\frac {}{{\mathsf {zero}}:{\mathsf {Nat}}}}\right)\;;\;\left({\frac {n:{\mathsf {Nat}}}{{\mathsf {suc}}\ n:{\mathsf {Nat}}}}\right)}

The horizontal-line notation can be read as "assuming (what is on the top) is true, we can infer that (what is on the bottom) is true." For example, "assuming n is of type Nat, then suc n is of type Nat." If nothing is on the top, then the bottom statement is always true: "zero is of type Nat (in all cases)."

Recursion on naturals

N a t I n d : ∀ P : N a t → ⋆ ⇒ P   z e r o → ( ∀ n : N a t ⇒ P   n → P   ( s u c   n ) ) → ∀ n : N a t ⇒ P   n {\displaystyle {\mathsf {NatInd}}:{\begin{matrix}\forall P:{\mathsf {Nat}}\rightarrow \star \Rightarrow P\ {\mathsf {zero}}\rightarrow \\(\forall n:{\mathsf {Nat}}\Rightarrow P\ n\rightarrow P\ ({\mathsf {suc}}\ n))\rightarrow \\\forall n:{\mathsf {Nat}}\Rightarrow P\ n\end{matrix}}} N a t I n d   P   m z   m s   z e r o ≡ m z {\displaystyle {\mathsf {NatInd}}\ P\ mz\ ms\ {\mathsf {zero}}\equiv mz} N a t I n d   P   m z   m s   ( s u c   n ) ≡ m s   n   ( N a t I n d   P   m z   m s   n ) {\displaystyle {\mathsf {NatInd}}\ P\ mz\ ms\ ({\mathsf {suc}}\ n)\equiv ms\ n\ (NatInd\ P\ mz\ ms\ n)}

...And in ASCII:

NatInd : all P : Nat -> * => P zero -> (all n : Nat => P n -> P (suc n)) -> all n : Nat => P n NatInd P mz ms zero => mz NatInd P mz ms (suc n) => ms n (NatInd P mz ms n)

Addition

p l u s   x   y ⇐ r e c _   x   { {\displaystyle {\mathsf {plus}}\ x\ y\Leftarrow {\underline {\mathrm {rec} }}\ x\ \{} p l u s   x   y ⇐ c a s e _   x   { {\displaystyle {\mathsf {plus}}\ x\ y\Leftarrow {\underline {\mathrm {case} }}\ x\ \{} p l u s   z e r o   y ⇒ y {\displaystyle {\mathsf {plus\ zero}}\ y\Rightarrow y} p l u s   ( s u c   x )   y ⇒ s u c ( p l u s   x   y )   }   } {\displaystyle \quad \quad {\mathsf {plus}}\ ({\mathsf {suc}}\ x)\ y\Rightarrow {\mathsf {suc}}({\mathsf {plus}}\ x\ y)\ \}\ \}}

...And in ASCII:

plus x y <= rec x { plus x y <= case x { plus zero y => y plus (suc x) y => suc (plus x y) } }

Dependent types

Epigram is essentially a typed lambda calculus with generalized algebraic data type extensions, except for two extensions. First, types are first-class entities, of type ⋆ {\displaystyle \star } ; types are arbitrary expressions of type ⋆ {\displaystyle \star } , and type equivalence is defined in terms of the types' normal forms. Second, it has a dependent function type; instead of P → Q {\displaystyle P\rightarrow Q} , ∀ x : P ⇒ Q {\displaystyle \forall x:P\Rightarrow Q} , where x {\displaystyle x} is bound in Q {\displaystyle Q} to the value that the function's argument (of type P {\displaystyle P} ) eventually takes.

Full dependent types, as implemented in Epigram, are a powerful abstraction. (Unlike in Dependent ML, the value(s) depended upon may be of any valid type.) A sample of the new formal specification capabilities dependent types bring may be found in The Epigram Tutorial.

See also

• ALF, a proof assistant among the predecessors of Epigram.

Further reading

• McBride, Conor; McKinna, James (2004). "The view from the left". Journal of Functional Programming. 14: 69–111. doi:10.1017/S0956796803004829. S2CID 6232997.
• McBride, Conor (2004). The Epigram Prototype, a nod and two winks (Report).
• McBride, Conor (2004). The Epigram Tutorial (Report).
• Altenkirch, Thorsten; McBride, Conor; McKinna, James (2005). Why Dependent Types Matter (Report).
• Chapman, James; Altenkirch, Thorsten; McBride, Conor (2006). Epigram Reloaded: A Standalone Typechecker for ETT (Report).
• Chapman, James; Dagand, Pierre-Évariste; McBride, Conor; Morris, Peter (2010). The gentle art of levitation (Report).

External links

• Official website
• Epigram 1 on GitHub
• Epigram2 on GitHub
• EPSRC on ALF, lego and related; archived version from 2006