Halo nucleus: Difference between revisions
en>Double sharp |
en>Graeme Bartlett m link Borromean nucleus |
||
Line 1: | Line 1: | ||
== | {{Infobox programming language | ||
| name = Epigram | |||
| logo = | |||
| paradigm = [[Functional programming|Functional]] | |||
| year = 2004 | |||
| designer = [[Conor McBride]] and<br/>James McKinna | |||
| developer = ''Unmaintained'' | |||
| latest_release_version = 1 | |||
| latest release date ={{release date|mf=yes|2006|10|11}} | |||
| typing = [[strong typing|strong]], [[static typing|static]], [[dependent typing|dependent]] | |||
| implementations = | |||
| dialects = | |||
| influenced_by = [[ALF (theorem prover)|ALF]] | |||
| influenced = | |||
| operating_system = [[Cross-platform]]: [[Linux]], [[Microsoft Windows|Windows]], [[Mac OS X]] | |||
| license = MIT<ref>http://code.google.com/p/epigram/</ref> | |||
| file_ext = | |||
}} | |||
'''Epigram''' is the name of a [[functional programming language]] with [[dependent type]]s. ''Epigram'' also refers to the [[Integrated development environment|IDE]] usually packaged with the language. Epigram's [[type system]] is strong enough to express [[program specification]]s. 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 [[United Kingdom|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]], [[Microsoft Windows|Windows]] and [[Mac OS X]]. | |||
It is currently unmaintained, and version 2, which was intended to implement [[Observational Type Theory]], was never released. | |||
== 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]]: | |||
<pre> ( ! ( ! ( n : Nat ! | |||
data !---------! where !----------! ; !-----------! | |||
! Nat : * ) !zero : Nat) !suc n : Nat)</pre> | |||
The declaration says that <code>Nat</code> is a type with [[Type system#Types of types|kind]] <code>*</code> (i.e., it is a simple type) and two constructors: <code>zero</code> and <code>suc</code>. The constructor <code>suc</code> takes a single <code>Nat</code> argument and returns a <code>Nat</code>. This is equivalent to the [[Haskell (programming language)|Haskell]] declaration "<code>data Nat = Zero | Suc Nat</code>". | |||
In LaTeX, the code is displayed as: | |||
<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> | |||
==== 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\ \mathsf{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: | |||
<pre>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)</pre> | |||
==== 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: | |||
<pre>plus x y <= rec x { | |||
plus x y <= case x { | |||
plus zero y => y | |||
plus (suc x) y => suc (plus x y) | |||
} | |||
}</pre> | |||
== 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 <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''. | |||
== See also == | |||
*[[ALF (proof assistant)|Alf]], a proof assistant among the predecessors of Epigram. | |||
==Further reading== | |||
*Conor McBride and James McKinna (2004), ''The view from the left'', Journal of Functional Programming | |||
*Conor McBride (2004), ''The Epigram Prototype, a nod and two winks'' | |||
*Conor McBride (2004), ''The Epigram Tutorial'' | |||
*Thorsten Altenkirch, Conor McBride and James McKinna (2005), ''Why Dependent Types Matter'' | |||
== External links == | |||
*[http://www.macs.hw.ac.uk/~fairouz/projects/EffProClaLog.html EPSRC] on ALF, lego and related | |||
== References == | |||
{{reflist}} | |||
[[Category:Functional languages]] | |||
[[Category:Dependently typed languages]] | |||
[[Category:Proof assistants]] | |||
[[Category:Discontinued programming languages]] |
Revision as of 00:33, 12 January 2014
Template:Infobox programming language
Epigram is the name of a functional programming language with dependent types. Epigram also refers to the IDE usually packaged with the language. 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.
It is currently unmaintained, and version 2, which was intended to implement Observational Type Theory, was never released.
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:
Recursion on naturals
...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 , , where is bound in to the value that the function's argument (of type ) 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
- Conor McBride and James McKinna (2004), The view from the left, Journal of Functional Programming
- Conor McBride (2004), The Epigram Prototype, a nod and two winks
- Conor McBride (2004), The Epigram Tutorial
- Thorsten Altenkirch, Conor McBride and James McKinna (2005), Why Dependent Types Matter
External links
- EPSRC on ALF, lego and related
References
43 year old Petroleum Engineer Harry from Deep River, usually spends time with hobbies and interests like renting movies, property developers in singapore new condominium and vehicle racing. Constantly enjoys going to destinations like Camino Real de Tierra Adentro.