# Dependent type

(Difference between revisions)
Jump to: navigation, search
 Revision as of 07:19, 1 April 2006 (edit)m (typographic corrections)← Previous diff Revision as of 07:33, 1 April 2006 (edit) (undo) (Linking with other wikipage: (1) a link back to Libraries and tools/Theorem provers (2) A more precise link (anchored to a section) to Type#See also)Next diff → Line 48: Line 48: === Cayenne === === Cayenne === - [http://www.cs.chalmers.se/~augustss/cayenne/index.html Cayenne] is influenced also by constructive type theory (see its page). Dependent types make it possible not to have a separate module lenguage and a core language. This idea may concern Haskell too, see [[First-class module]] page. + [http://www.cs.chalmers.se/~augustss/cayenne/index.html Cayenne] is influenced also by constructive type theory (see its page). + Dependent types make it possible not to have a separate module lenguage and a core language. This idea may concern Haskell too, see [[First-class module]] page. + + Depandent types make it useful also as a [[Libraries and tools/Theorem provers|theorem prover]]. === Other techniques === === Other techniques === Line 61: Line 64: === Simulating them === === Simulating them === * [http://haskell.org/hawiki/SimulatingDependentTypes SimulatingDependentTypes] of HaWiki * [http://haskell.org/hawiki/SimulatingDependentTypes SimulatingDependentTypes] of HaWiki - * The ''See also'' section of [[Type]] page contains links to many related idioms. + * The [[Type#See also|''See also'' section of Type]] page contains links to many related idioms. * On the usefulness of such idioms in practice, see HaskellDB's pages * On the usefulness of such idioms in practice, see HaskellDB's pages ** [http://haskelldb.sourceforge.net/ updated] page (see ''Papers'' subsection on [http://haskelldb.sourceforge.net/#documentation Documentation]) ** [http://haskelldb.sourceforge.net/ updated] page (see ''Papers'' subsection on [http://haskelldb.sourceforge.net/#documentation Documentation])

## 1 The concept of dependent types

### 1.1 General

Dependent Types in Programming abstract in APPSEM'2000

### 1.2 Type Theory

Simon Thompson: Type Theory and Functional Programming. Section 6.3 deals with dependent types, but because of the strong emphasis on Curry-Howard isomorphism and the connections between logic and programming, the book seemed cathartic for me even from its beginning.

### 1.3 Illative Combinatory Logic

To see how Illative Combinatory logic deals with dependent types, see combinator G described in Systems of Illative Combinatory Logic complete for first-order propositional and predicate calculus by Henk Barendregt, Martin Bunder, Wil Dekkers. It seems to me that the dependent type construct $\forall x : S \Rightarrow T$ of Epigram corresponds to $\mathbf G\;S\;(\lambda x . T)$ in Illative Combinatory Logic. I think e.g. the followings should correspond to each other:

• $\mathrm{realNullvector} :\;\;\;\forall n: \mathrm{Nat} \Rightarrow \mathrm{RealVector}\;n$
• $\mathbf G\;\,\mathrm{Nat}\;\,\mathrm{RealVector}\;\,\mathrm{realNullvector}$

## 2 Dependently typed languages

### 2.1 Epigram

Epigram is a full dependently typed programming language see especially

Dependent types (of this language) also provide a not-forgetful concept of views (already mentioned in the Haskell Future; the connection between these concepts is described in p. 32 of Epigram Tutorial (section 4.6 Patterns Forget; Matching Is Remembering).

See Epigram also as theorem prover.

### 2.2 Agda

Agda is a system for incrementally developing proofs and programs. Agda is also a functional language with dependent types. This language is very similar to cayenne and agda is intended to be a (almost) full implementation of it in the future.“

People who are interested also in theorem proving may see the theorem provers page.

### 2.3 Cayenne

Cayenne is influenced also by constructive type theory (see its page).

Dependent types make it possible not to have a separate module lenguage and a core language. This idea may concern Haskell too, see First-class module page.

Depandent types make it useful also as a theorem prover.

## 3 Dependent types in Haskell programming

### 3.1 Proposals

John Hughes: Dependent Types in Haskell (some ideas).