Epigram (programming language)

Syntax

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

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 )

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

N a t I n d   P   m z   m s   z e r o ≡ m z

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 )

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

...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 ⋆ ; types are arbitrary expressions of type ⋆ , and type equivalence is defined in terms of the types' normal forms. Second, it has a dependent function type; instead of P → Q , ∀ x : P ⇒ 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.