# Dependent type

### From HaskellWiki

EndreyMark (Talk | contribs) m (Using level 1 headlines for top-level structuring, according to HaskellWiki:Guidelines) |
EndreyMark (Talk | contribs) (Refining the structure: adding subsections ,,General'' to ,,Concept'', ,,Other Techniques'' to ,,Languages'') |
||

Line 2: | Line 2: | ||

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

+ | |||

+ | == General == | ||

+ | [http://en.wikipedia.org/wiki/Dependent_types Wikipedia] | ||

[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 Theory == | ||

+ | ... | ||

+ | |||

+ | == Illatice 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. | ||

Line 16: | Line 24: | ||

= Dependently typed languages = | = Dependently typed languages = | ||

+ | |||

+ | == Epigram == | ||

[http://www.e-pig.org/ Epigram] is a full dependently typed programming language see especially | [http://www.e-pig.org/ Epigram] is a full dependently typed programming language see especially | ||

Line 23: | Line 33: | ||

Dependent types (of this language) also provide a not-forgetful concept of '''views''' (already mentioned in the Haskell [[Future]]; | 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''). | the connection between these concepts is described in p. 32 of Epigram Tutorial (section ''4.6 Patterns Forget; Matching Is Remembering''). | ||

+ | |||

+ | == Other techniques == | ||

+ | |||

+ | [http://www-sop.inria.fr/oasis/DTP00/ [APPSEM Workshop on Subtyping & Dependent Types in Programming] | ||

= Dependent types in Haskell programming = | = Dependent types in Haskell programming = |

## Revision as of 16:46, 1 March 2006

## Contents |

# 1 The concept of dependent types

## 1.1 General

Dependent Types in Programming abstract in APPSEM'2000

## 1.2 Type Theory

...

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

# 2 Dependently typed languages

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

## 2.2 Other techniques

[APPSEM Workshop on Subtyping & Dependent Types in Programming

# 3 Dependent types in Haskell programming

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