# Dependent type

### From HaskellWiki

EndreyMark (Talk | contribs) m (typographic correction) |
EndreyMark (Talk | contribs) m (Using == ... == as top level headlines (according to HaskellWiki:Guidelines#Headlines)) |
||

Line 1: | Line 1: | ||

__TOC__ | __TOC__ | ||

− | = The concept of dependent types = | + | == The concept of dependent types == |

− | == General == | + | === General === |

[http://en.wikipedia.org/wiki/Dependent_types Wikipedia] | [http://en.wikipedia.org/wiki/Dependent_types Wikipedia] | ||

[http://www-sop.inria.fr/oasis/Caminha00/abstract.html Dependent Types in Programming] abstract in APPSEM'2000 | [http://www-sop.inria.fr/oasis/Caminha00/abstract.html Dependent Types in Programming] abstract in APPSEM'2000 | ||

− | == Type Theory == | + | === Type Theory === |

Simon Thompson: [http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ Type Theory and Functional Programming]. Section 6.3 deals with dependent types, but because of the strong emphasis on [http://en.wikipedia.org/wiki/Curry_Howard_isomorphism Curry-Howard isomorphism] and the connections between logic and programming, | Simon Thompson: [http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ Type Theory and Functional Programming]. Section 6.3 deals with dependent types, but because of the strong emphasis on [http://en.wikipedia.org/wiki/Curry_Howard_isomorphism Curry-Howard isomorphism] and the connections between logic and programming, | ||

Line 15: | Line 15: | ||

[http://lists.seas.upenn.edu/mailman/listinfo/types-list Types Forum] | [http://lists.seas.upenn.edu/mailman/listinfo/types-list Types Forum] | ||

− | == Illative Combinatory Logic == | + | === Illative Combinatory Logic === |

To see how Illative [[Combinatory logic]] deals with dependent types, see combinator '''G''' described in [http://citeseer.ist.psu.edu/246934.html Systems of Illative Combinatory Logic complete for first-order propositional and predicate calculus] by Henk Barendregt, Martin Bunder, Wil Dekkers. | To see how Illative [[Combinatory logic]] deals with dependent types, see combinator '''G''' described in [http://citeseer.ist.psu.edu/246934.html Systems of Illative Combinatory Logic complete for first-order propositional and predicate calculus] by Henk Barendregt, Martin Bunder, Wil Dekkers. | ||

Line 27: | Line 27: | ||

− | = Dependently typed languages = | + | == Dependently typed languages == |

− | == Epigram == | + | === Epigram === |

[http://www.e-pig.org/ Epigram] is a full dependently typed programming language see especially | [http://www.e-pig.org/ Epigram] is a full dependently typed programming language see especially | ||

Line 38: | Line 38: | ||

the connection between these concepts is described in p. 32 of Epigram Tutorial (section ''4.6 Patterns Forget; Matching Is Remembering''). | the connection between these concepts is described in p. 32 of Epigram Tutorial (section ''4.6 Patterns Forget; Matching Is Remembering''). | ||

− | == Agda == | + | === Agda === |

“[http://www.cs.chalmers.se/~catarina/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 [http://www.cs.chalmers.se/~augustss/cayenne/index.html cayenne] and agda is intended to be a (almost) full implementation of it in the future.“ | “[http://www.cs.chalmers.se/~catarina/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 [http://www.cs.chalmers.se/~augustss/cayenne/index.html cayenne] and agda is intended to be a (almost) full implementation of it in the future.“ | ||

Line 44: | Line 44: | ||

People who are interested also in theorem proving may see the [[Libraries and tools/Theorem provers|theorem provers]] page. | People who are interested also in theorem proving may see the [[Libraries and tools/Theorem provers|theorem provers]] page. | ||

− | == Cayene == | + | === Cayene === |

[http://www.cs.chalmers.se/~augustss/cayenne/index.html Cayene] 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 Cayene] 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. | ||

− | == Other techniques == | + | === Other techniques === |

[http://www-sop.inria.fr/oasis/DTP00/ APPSEM Workshop on Subtyping & Dependent Types in Programming] | [http://www-sop.inria.fr/oasis/DTP00/ APPSEM Workshop on Subtyping & Dependent Types in Programming] | ||

− | = Dependent types in Haskell programming = | + | == Dependent types in Haskell programming == |

− | == Proposals == | + | === Proposals === |

John Hughes: [http://www.coverproject.org/TalksUntilSpring2004/DependentTypesInHaskell.pdf Dependent Types in Haskell (some ideas)]. | John Hughes: [http://www.coverproject.org/TalksUntilSpring2004/DependentTypesInHaskell.pdf Dependent Types in Haskell (some ideas)]. | ||

− | == 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 ''See also'' section of [[Type]] page contains links to many related idioms. |

## Revision as of 21:23, 31 March 2006

## Contents |

## 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
of Epigram corresponds to
in Illative Combinatory Logic. I think e.g. the followings should correspond to each other:

## 2 Dependently typed languages

### 2.1 Epigram

Epigram is a full dependently typed programming language see especially

- Epigram Tutorial by Conor McBride
- and Why dependent types matter by Thorsten Altenkirch, Conor McBride and James McKinna).

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

### 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 Cayene

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

### 2.4 Other techniques

APPSEM Workshop on Subtyping & Dependent Types in Programming

## 3 Dependent types in Haskell programming

### 3.1 Proposals

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

### 3.2 Simulating them

- SimulatingDependentTypes of HaWiki
- The
*See also*section of Type page contains links to many related idioms. - On the usefulness of such idioms in practice, see HaskellDB's pages
- updated page (see
*Papers*subsection on Documentation) - which presupposes reading also paper on the original page (see Documentation subpage, PostScript version)

- updated page (see