Epigram Programming Language Website Links For
Programming 		 

Information About

Epigram Programming Language
  CATEGORIES ABOUT EPIGRAM PROGRAMMING LANGUAGE
   
programming languages
   
functional languages
   
declarative programming languages
   
dependently-typed formal languages
   
theorem provers
   
APPAREL
BABY
BEAUTY
BOOKS
CAR TOYS
CELL PHONES
DVD'S
ELECTRONICS
GOURMET FOOD
GROCERIES
HEALTH & PERSONAL
HOME & GARDEN
JEWELRY
MUSIC
MUSIC INSTRUMENTS
OFFICE PRODUCTS
SOFTWARE
SPORTING GOODS
TOOLS & HARDWARE
TOYS
VIDEO GAMES
SHOPPING HOME
MORE SHOPPING...



The Epigram prototype was implemented by Conor McBride based on joint work with James McKinna. Its development is continued by the Epigram group in , 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

\underline\mathrm{data} \; \left( rac{}{\mathsf{Nat} : \star} ight) \; \underline\mathrm{where} \;
\left( rac{}{\mathsf{zero} : \mathsf{Nat}} ight) \; ; \;
\left( rac{n : \mathsf{Nat}}{\mathsf{suc}\ n : \mathsf{Nat}} ight)

...And in ASCII:
     (         !       (          !   (  n : Nat  !

data !
-! where !
--! ; !
---!


    

  •  )       !zero : Nat)   !suc n : Nat)



Recursion on naturals

\mathsf{NatInd} : \begin{matrix}
orall P : \mathsf{Nat} ightarrow \star \Rightarrow P\ \mathsf{zero} ightarrow \
( orall n : \mathsf{Nat} \Rightarrow P\ n ightarrow P\ (\mathsf{suc}\ n)) ightarrow\
orall n : \mathsf{Nat} \Rightarrow P\ n
\end{matrix}

\mathsf{NatInd}\ P\ mz\ ms\ zero \equiv mz

\mathsf{NatInd}\ P\ mz\ ms\ (\mathsf{suc}\ n) \equiv ms\ n\ (NatInd\ P\ mz\ ms\ n)

...And in ASCII:
  • => 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 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 \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 ightarrow Q, orall x : P \Rightarrow Q, where x is bound in Q to the value that the function's argument (of type P) eventually takes.

Dependent types are an abstraction of incredible power. To sample some of the new capabilities it adds to a language, read ''The Epigram Tutorial'' .


EXTERNAL LINKS