Dependent type

From HaskellWiki
Revision as of 14:30, 1 March 2006 by EndreyMark (talk | contribs) (table of contents)
Jump to navigation Jump to search

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

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 in Haskell programming