# Dependent type

### From HaskellWiki

EndreyMark (Talk | contribs) m (,,Illative'' misstype corrected) |
EndreyMark (Talk | contribs) (Links on Curry-Howard isomorphism added to ,,Concept'' section / ,,TypeTheory'' subsection) |
||

Line 9: | Line 9: | ||

== Type Theory == |
== 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, |
||

+ | the book seemed cathartic for me even from its beginning. |
||

+ | |||

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

== Illative Combinatory Logic == |
== Illative Combinatory Logic == |
||

Line 36: | Line 36: | ||

== Other techniques == |
== Other techniques == |
||

− | [http://www-sop.inria.fr/oasis/DTP00/ [APPSEM Workshop on Subtyping & Dependent Types in Programming] |
+ | [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 17:19, 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

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.

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

# 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