Epigram is the name of a
functional programming
language with
dependent types and
of the
IDE
usually packaged with it. Epigram's
type
system is strong enough to express
program specifications. The goal is to
support a smooth transition from ordinary programming to integrated
programs and proofs whose correctness can be checked and certified
by the
compiler. Epigram exploits the
propositions as types
principle, and is based on
intuitionistic type theory.
The Epigram prototype was implemented by Conor McBride based on
joint work with James McKinna.
Its development is continued by the Epigram
group in Nottingham, Durham, St Andrews and Royal Holloway in
the UK. The current experimental implementation of
the Epigram system is freely available together with a user manual,
a tutorial and some background material. The system has been used
under
Linux,
Windows and
Mac OS
X.
Syntax
Epigram uses a two-dimensional syntax, with a LaTeX version and an
ASCII version. 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:
\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)
Recursion on naturals
\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}
\mathsf{NatInd}\ P\ mz\ ms\ \mathsf{zero} \equiv mz
\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 => mzNatInd P mz ms (suc n) => ms n
(NatInd P mz ms n)
Addition
\mathsf{plus}\ x\ y \Leftarrow \underline\mathrm{rec}\ x\
\{ |
\mathsf{plus}\ x\ y \Leftarrow
\underline\mathrm{case}\ x\ \{ |
\mathsf{plus\
zero}\ y \Rightarrow y |
\quad\quad
\mathsf{plus}\ (\mathsf{suc}\ x)\ y \Rightarrow 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 \star; types are arbitrary
expressions of type \star, and type equivalence is defined in terms
of the types' normal forms. Second, it has a dependent function
type; instead of P \rightarrow Q, \forall x : P \Rightarrow Q,
where x is bound in Q to the value that the function's argument (of
type 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.
It is planned that the forthcoming version of Epigram, Epigram 2,
will be based on
Observational Type Theory (note: link is to an
incomplete draft paper), a new development of
constructive type theory.
See also
- EPSRC on ALF, lego and related
- Alf, the
Algebraic Logic Functional programming language
External links