Dependent type

The concept of dependent types

General

Wikipedia

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 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 $\mathrm{\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{r}\mathrm{e}\mathrm{a}\mathrm{l}\mathrm{N}\mathrm{u}\mathrm{l}\mathrm{l}\mathrm{v}\mathrm{e}\mathrm{c}\mathrm{t}\mathrm{o}\mathrm{r}:\mathrm{\forall }n:\mathrm{N}\mathrm{a}\mathrm{t}\Rightarrow \mathrm{R}\mathrm{e}\mathrm{a}\mathrm{l}\mathrm{V}\mathrm{e}\mathrm{c}\mathrm{t}\mathrm{o}\mathrm{r}n$
• $\mathbf{G}\mathrm{N}\mathrm{a}\mathrm{t}\mathrm{R}\mathrm{e}\mathrm{a}\mathrm{l}\mathrm{V}\mathrm{e}\mathrm{c}\mathrm{t}\mathrm{o}\mathrm{r}\mathrm{r}\mathrm{e}\mathrm{a}\mathrm{l}\mathrm{N}\mathrm{u}\mathrm{l}\mathrm{l}\mathrm{v}\mathrm{e}\mathrm{c}\mathrm{t}\mathrm{o}\mathrm{r}$

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