Not What You Meant? There are 3 definitions for Epigram.

Epigram (programming language)

About 2 pages (660 words)

Know this topic well? Help others and get FREE products!

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 from the Epigram homepage together with a user manual, a tutorial and some background material. The system has been used under Linux, Windows and Mac OS X.

1 Syntax
- 1.1 Examples
2 Dependent types in Epigram
3 See also
4 External links

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

<math>\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)</math>

...And in ASCII:

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

Recursion on naturals

<math>\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}</math>

<math>\mathsf{NatInd}\ P\ mz\ ms\ zero \equiv mz</math> <math>\mathsf{NatInd}\ P\ mz\ ms\ (\mathsf{suc}\ n) \equiv ms\ n\ (NatInd\ P\ mz\ ms\ n)</math> ...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

<math>\mathsf{plus}\ x\ y \Leftarrow \underline\mathrm{rec}\ x\ \{</math>

<math>\mathsf{plus}\ x\ y \Leftarrow \underline\mathrm{case}\ x\ \{</math>

<math>\mathsf{plus\ zero}\ y \Rightarrow y</math>

<math>\quad\quad \mathsf{plus}\ (\mathsf{suc}\ x)\ y \Rightarrow suc\ (\mathsf{plus}\ x\ y)\ \}\ \}</math>

...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 in Epigram

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 <math>\star</math>; types are arbitrary expressions of type <math>\star</math>, and type equivalence is defined in terms of the types' normal forms. Second, it has a dependent function type; instead of <math>P \rightarrow Q</math>, <math>\forall x : P \Rightarrow Q</math>, where <math>x</math> is bound in <math>Q</math> to the value that the function's argument (of type <math>P</math>) 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.