# Difference between revisions of "Dependent type"

EndreyMark (talk | contribs) (Refining the structure: adding subsections ,,General'' to ,,Concept'', ,,Other Techniques'' to ,,Languages'') |
EndreyMark (talk | contribs) m (,,Illative'' misstype corrected) |
||

Line 11: | Line 11: | ||

... | ... | ||

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

To see how Illative [[CombinatoryLogic]] 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 [[CombinatoryLogic]] 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 16:48, 1 March 2006

## Contents

# The concept of dependent types

## General

Dependent Types in Programming abstract in APPSEM'2000

## Type Theory

...

## Illative Combinatory Logic

To see how Illative CombinatoryLogic 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*).

## Other techniques

[APPSEM Workshop on Subtyping & Dependent Types in Programming

# Dependent types in Haskell programming

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