# Dependent type

(Difference between revisions)
 Revision as of 16:48, 1 March 2006 (edit)m (,,Illative'' misstype corrected)← Previous diff Revision as of 17:19, 1 March 2006 (edit) (undo) (Links on Curry-Howard isomorphism added to ,,Concept'' section / ,,TypeTheory'' subsection)Next diff → 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 40: == 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 =

# 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 $\forall x : S \Rightarrow T$ of Epigram corresponds to $\mathbf G\;S\;(\lambda x . T)$ in Illative Combinatory Logic. I think e.g. the followings should correspond to each other:

• $\mathrm{realNullvector} :\;\;\;\forall n: \mathrm{Nat} \Rightarrow \mathrm{RealVector}\;n$
• $\mathbf G\;\,\mathrm{Nat}\;\,\mathrm{RealVector}\;\,\mathrm{realNullvector}$

# 2 Dependently typed languages

## 2.1 Epigram

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