Personal tools

Dependent type

From HaskellWiki

(Difference between revisions)
Jump to: navigation, search
m (meta: adding Type-level programming category)
(Updated link to Agda)
Line 46: Line 46:
 
=== Agda ===
 
=== Agda ===
   
“[http://www.cs.chalmers.se/~catarina/agda/ Agda] is a system for incrementally developing proofs and programs. Agda is also a functional language with dependent types. This language is very similar to [http://www.cs.chalmers.se/~augustss/cayenne/index.html cayenne] and agda is intended to be a (almost) full implementation of it in the future.“
+
“[http://www.cs.chalmers.se/~ulfn/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 [[Libraries and tools/Theorem provers|theorem provers]] page.
 
People who are interested also in theorem proving may see the [[Libraries and tools/Theorem provers|theorem provers]] page.

Revision as of 14:19, 9 October 2007

Contents


1 The concept of dependent types

1.1 General


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.

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

Types Forum

1.3 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 \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 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.

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

2.3 Cayenne

Cayenne is influenced also by constructive type theory (see its page).

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

Depandent types make it useful also as a theorem prover.

2.4 Qi

Qi is a Lisp-based functional programming language. It provides many possibilities (currying, pattern matching, type checking etc.), and it uses sequent calculus notation for defining new types. This enables a very powerful type system.

2.5 Other techniques

Also Blaise is a Lisp-based language with dependent types. It will be released under GPL, but has not yet a released implementation.

APPSEM Workshop on Subtyping & Dependent Types in Programming

3 Dependent types in Haskell programming

3.1 Lightweight Dependent Typing

This web page describes the 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).

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

3.3 Proposals

John Hughes: Dependent Types in Haskell (some ideas).

3.4 Simulating them