# Dependent type

(Difference between revisions)
 Revision as of 16:23, 1 March 2006 (edit)m (Using level 1 headlines for top-level structuring, according to HaskellWiki:Guidelines)← Previous diff Revision as of 16:46, 1 March 2006 (edit) (undo) (Refining the structure: adding subsections ,,General'' to ,,Concept'', ,,Other Techniques'' to ,,Languages'')Next diff → 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 =

# 1 The concept of dependent types

## 1.1 General

Dependent Types in Programming abstract in APPSEM'2000

...

## 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 $\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).