# Difference between revisions of "Dependent type"

EndreyMark (talk | contribs) (The description of Epigram got a link to Libraries and tools/Theorem provers, because that page also mentions Epigram) |
EndreyMark (talk | contribs) m (typographic corrections) |
||

Line 46: | Line 46: | ||

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

− | === |
+ | === Cayenne === |

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

=== Other techniques === |
=== Other techniques === |
||

Line 55: | Line 55: | ||

== 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)]. |

## Revision as of 07:19, 1 April 2006

## Contents

## The concept of dependent types

### General

Dependent Types in Programming abstract in APPSEM'2000

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

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

## Dependently typed languages

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

See Epigram also as theorem prover.

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

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

### Other techniques

APPSEM Workshop on Subtyping & Dependent Types in Programming

## Dependent types in Haskell programming

### Proposals

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

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