Dependent type

The concept of dependent types

Dependent Types in Programming abstract in APPSEM'2000

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

Dependent types in Haskell programming

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