Menu
Home
People
Places
Arts
History
Plants & Animals
Science
Life & Culture
Technology
Reference.org
Epigram (programming language)
open-in-new
<h2 id="syntax">Syntax</h2> <p>Epigram uses a two-dimensional, <a href="/facts/Natural_deduction/PPtgwoaJ">natural deduction</a> style syntax, with versions in <a href="/facts/LaTeX/c1lvjF0A">LaTeX</a> and <a href="/facts/ASCII/vGUI33Qu">ASCII</a>. Here are some examples from <i>The Epigram Tutorial</i>: </p> <h3>Examples</h3> <h4>The natural numbers</h4> <p>The following declaration defines the <a href="/facts/Natural_numbers/u65og8JE">natural numbers</a>: </p> ( ! ( ! ( n : Nat ! data !---------! where !----------! ; !-----------! ! Nat : * ) !zero : Nat) !suc n : Nat) <p>The declaration says that Nat is a type with <a href="/facts/Type_system/Tz0bAMS9">kind</a> * (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 <a href="/facts/Haskell_(programming_language)/4Htv9WLu">Haskell</a> declaration "data Nat = Zero | Suc Nat". </p><p>In LaTeX, the code is displayed as: </p> 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)} <p>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)." </p> <h4>Recursion on naturals</h4> 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)} <p>...And in ASCII: </p> 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) <h4>Addition</h4> 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)\ \}\ \}} <p>...And in ASCII: </p> plus x y <= rec x { plus x y <= case x { plus zero y => y plus (suc x) y => suc (plus x y) } } <h2 id="dependent-types">Dependent types</h2> <p>Epigram is essentially a <a href="/facts/Typed_lambda_calculus/g86GP4uK">typed lambda calculus</a> with <a href="/facts/Generalized_algebraic_data_type/c2tQGjcq">generalized algebraic data type</a> 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. </p><p>Full dependent types, as implemented in Epigram, are a powerful abstraction. (Unlike in <a href="/facts/Dependent_ML/aAyzD1n8">Dependent ML</a>, 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 <i>The Epigram Tutorial</i>. </p> <h2 id="see-also">See also</h2> <ul><li><a href="/facts/ALF_(proof_assistant)/QhjqTxbB">ALF</a>, a proof assistant among the predecessors of Epigram.</li></ul> <h2 id="further-reading">Further reading</h2> <ul><li>McBride, Conor; McKinna, James (2004). <a href="https://doi.org/10.1017%2FS0956796803004829">"The view from the left"</a>. <i>Journal of Functional Programming</i>. 14: 69–111. <a href="/facts/Doi_(identifier)/muM9Etpq">doi</a>:<a href="https://doi.org/10.1017%2FS0956796803004829">10.1017/S0956796803004829</a>. <a href="/facts/S2CID_(identifier)/ldJsHa2Y">S2CID</a> <a href="https://api.semanticscholar.org/CorpusID:6232997">6232997</a>.</li> <li>McBride, Conor (2004). The Epigram Prototype, a nod and two winks (Report).</li> <li>McBride, Conor (2004). The Epigram Tutorial (Report).</li> <li>Altenkirch, Thorsten; McBride, Conor; McKinna, James (2005). Why Dependent Types Matter (Report).</li> <li>Chapman, James; Altenkirch, Thorsten; McBride, Conor (2006). Epigram Reloaded: A Standalone Typechecker for ETT (Report).</li> <li>Chapman, James; Dagand, Pierre-Évariste; McBride, Conor; Morris, Peter (2010). The gentle art of levitation (Report).</li></ul> <h2 id="external-links">External links</h2> <ul><li><a href="http://e-pig.org">Official website</a></li> <li><a href="https://github.com/david-christiansen/epigram1">Epigram 1</a> on <a href="/facts/GitHub/n1hNCsc3">GitHub</a></li> <li><a href="https://github.com/mietek/epigram2">Epigram2</a> on <a href="/facts/GitHub/n1hNCsc3">GitHub</a></li> <li><a href="https://web.archive.org/web/20060209235723/http://www.macs.hw.ac.uk/~fairouz/projects/EffProClaLog.html">EPSRC</a> on ALF, lego and related; archived version from 2006</li></ul>