Dependent type

The concept of dependent types

General

• Dependent Types in Programming abstract in APPSEM'2000
• Do we need dependent types? by Daniel Fridlender and Mia Indrika, 2001.
• Dependent Type Systems as Macros by Stephen Chang, Michael Ballantyne, Milo Turner, and William J. Bowman, 2019.
• Wikipedia

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.

Another interesting approach to Curry-Howard isomorphism and the concept of dependent type: Lecture 9. Semantics and pragmatics of text and dialogue discusses these concepts in the context of linguistics. Written by Arne Ranta, see also his online course and other linguistical materials on the Linguistics wiki page.

Types Forum

Illative combinatory logic

To see how Illative Combinatory logic 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{𝐆}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{𝐆}\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}$

Dependent types as abstract data

Since it can vary according to the data (values) it is used with, a dependent type can be seen as a highly-stylised form of abstract data, with copious quantities of syntactic sugar for programming palatability. So by bringing types down to the level of data (and then requiring said data be total), the concept of types disappears altogether - in the end, it’s all just data.

Consequently, the only major point of difference between the stylised data of “types” and more-recognisable data (boolean, strings, integers, etc) is the time of their evaluation: at compile-time or run-time. Hence “static typing” is merely the partial evaluation of stylised “type” data at compile-time, with “dynamic typing” being that same evaluation, but at run-time.

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 of Haskell#Extensions of Haskell; the connection between these concepts is described in p. 32 of Epigram Tutorial (section 4.6 Patterns Forget; Matching Is Remembering).

See Epigram also as theorem prover.

Agda

Agda is a system for incrementally developing proofs and programs. Agda is also a functional language with dependent types. This language is similar to Epigram but has a more Haskell-like syntax.

People who are interested also in theorem proving may see the theorem provers page.

Idris

Idris is a general purpose pure functional programming language with dependent types, eager evaluation, and optional lazy evaluation via laziness annotations. It has a very Haskell-like syntax and is available on Hackage.

Idris is actively developed by Edwin Brady at the University of St. Andrews.

Cayenne

Cayenne is influenced also by constructive type theory. The compiler can be found at GitHub

Dependent types make it possible not to have a separate module language and a core language. This idea may concern Haskell too, see First-class module page.

Dependent types make it useful also as a theorem prover.

Ohmu

In Ohmu, types and values are both first-class. This is used to reduce the tension between functional and object-oriented programming.

• Functional versus OO Programming: Conflict Without a Cause, DeLesley Hutchins. In Joint proceedings of the Workshops on Multiparadigm Programming with Object-Oriented Languages (MPOOL’03): Declarative Programming in the Context of Object-Oriented Languages (DP-COOL’03) (pages 69-91 of 300).

Dependent types in Haskell programming

Lightweight Dependent Typing

These pages describe a lightweight approach and its applications, e.g., statically safe head/tail functions and the elimination of array bound check (even in such complex algorithms as Knuth-Morris-Pratt string search). The page also briefly describes `singleton types' (Hayashi and Xi).

Library

Ivor is type theory based theorem proving library -- written by Edwin Brady (see also the author's homepage, there are a lot of materials concerning dependent type theory there).

Proposals

• Richard A. Eisenberg: Dependent Types in Haskell: Theory and Practice
• John Hughes: Dependent Types in Haskell (some ideas) (404).

Simulating them

• Faking it: Simulating Dependent Types in Haskell, by Conor McBride
• SimulatingDependentTypes of HaWiki (Web Archive)
• The See also section of Type page contains links to many related idioms. Especially type arithmetic seems to me also a way yielding some tastes from dependent type theory.
• On the usefulness of such idioms in practice, see HaskellDB's pages
  • updated page (see Papers subsection on Documentation)
  • which presupposes reading also paper on the original page (see Documentation subpage, PostScript version)