# Difference between revisions of "Dependent type"

EndreyMark (talk | contribs) (The details of the Dependent Types item of Haskell Furure page has been moved here) |
EndreyMark (talk | contribs) |
||

Line 1: | Line 1: | ||

+ | __TOC__ |
||

+ | |||

== The concept of dependent types == |
== The concept of dependent types == |
||

Line 22: | Line 24: | ||

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

− | == Haskell == |
+ | == Dependent types for Haskell == |

* 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 14:28, 1 March 2006

## The concept of dependent types

Dependent Types in Programming abstract in APPSEM'2000

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

## Dependent types for Haskell

- John Hughes: Dependent Types in Haskell (some ideas).
- SimulatingDependentTypes of HaWiki