# Difference between revisions of "Dependent type"

EndreyMark (talk | contribs) (In section →Type theory: An approach to the concept of dependent type and Curry-Howard isomorphism: dicussed in the context of linguistics!) |
EndreyMark (talk | contribs) m (sentence-style capitalization of headlines) |
||

Line 8: | Line 8: | ||

[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 |
+ | === 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 17: | Line 17: | ||

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

− | === Illative |
+ | === 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. |

## Revision as of 09:38, 12 May 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.

Another interesting approach to Curry-Howard isomorphism and the concept of dependent type: Lecture 9. Semantics and pragmatics of text and dialogue dicsusses these concepts in the context of linguistics. Written by Arne Ranta, see also his online course and other linguistical materials on the Linguistics wikipage.

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

Depandent types make it useful also as a theorem prover.

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