Personal tools

Dependent type

From HaskellWiki

(Difference between revisions)
Jump to: navigation, search
(Referring to HaskelDB, as a practical case study on the usefulness of such idioms (i.e. those related to simulating dependent types))
(Dependently typed languages)
(31 intermediate revisions by 14 users not shown)
Line 1: Line 1:
 
__TOC__
 
__TOC__
   
= The concept of dependent types =
+
== The concept of dependent types ==
   
== General ==
+
=== 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://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.brics.dk/RS/01/10/BRICS-RS-01-10.ps.gz Do we need dependent types?] by Daniel Fridlender and Mia Indrika, 2001.
   
== Type Theory ==
+
  +
=== Type theory ===
   
 
Simon Thompson: [http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ Type Theory and Functional Programming]. Section 6.3 deals with dependent types, but because of the strong emphasis on [http://en.wikipedia.org/wiki/Curry_Howard_isomorphism Curry-Howard isomorphism] and the connections between logic and programming,
 
Simon Thompson: [http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ Type Theory and Functional Programming]. Section 6.3 deals with dependent types, but because of the strong emphasis on [http://en.wikipedia.org/wiki/Curry_Howard_isomorphism Curry-Howard isomorphism] and the connections between logic and programming,
 
the book seemed cathartic for me even from its beginning.
 
the book seemed cathartic for me even from its beginning.
  +
  +
Another interesting approach to Curry-Howard isomorphism and the concept of dependent type: [http://www.cs.chalmers.se/~aarne/course-langtech/lectures/lang09.html Lecture 9. Semantics and pragmatics of text and dialogue] dicsusses these concepts in the context of linguistics. Written by [http://www.cs.chalmers.se/~aarne/ Arne Ranta], see also [[Libraries and tools/Linguistics#Other functional or Haskell-related approaches to linguistics|his online course and other linguistical materials on the Linguistics wikipage]].
   
 
[http://lists.seas.upenn.edu/mailman/listinfo/types-list Types Forum]
 
[http://lists.seas.upenn.edu/mailman/listinfo/types-list Types Forum]
   
== Illative Combinatory Logic ==
+
=== Illative combinatory logic ===
   
 
To see how Illative [[Combinatory logic]] 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 [[Combinatory logic]] 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 26: Line 28:
   
   
= Dependently typed languages =
+
== Dependently typed languages ==
   
== Epigram ==
+
=== 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
* [http://www.e-pig.org/downloads/epigram-notes.pdf Epigram Tutorial] by Conor McBride
+
* [http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.115.9718&rep=rep1&type=pdf Epigram Tutorial] by Conor McBride
* and [http://www.e-pig.org/downloads/ydtm.pdf Why dependent types matter] by Thorsten Altenkirch, Conor McBride and James McKinna).
+
* and [http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.106.8190&rep=rep1&type=pdf 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]];
+
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'').
 
the connection between these concepts is described in p. 32 of Epigram Tutorial (section ''4.6 Patterns Forget; Matching Is Remembering'').
   
== Other techniques ==
+
See Epigram also as [[Libraries and tools/Theorem provers|theorem prover]].
   
[http://www-sop.inria.fr/oasis/DTP00/ APPSEM Workshop on Subtyping & Dependent Types in Programming]
+
=== Agda ===
   
= Dependent types in Haskell programming =
+
[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.
== Proposals ==
+
  +
People who are interested also in theorem proving may see the [[Libraries and tools/Theorem provers|theorem provers]] page.
  +
  +
=== Idris ===
  +
  +
[http://idris-lang.org/ 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 [http://hackage.haskell.org/package/idris Hackage].
  +
  +
Idris is actively developed by [http://edwinb.wordpress.com/ Edwin Brady] at the [http://www.cs.st-andrews.ac.uk/ University of St. Andrews].
  +
  +
=== Cayenne ===
  +
  +
[http://www.augustsson.net/Darcs/Cayenne/html/ Cayenne] is influenced also by [http://en.wikipedia.org/wiki/Constructive_type_theory constructive type theory].
  +
  +
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 [[Applications and libraries/Theorem provers|theorem prover]].
  +
  +
== Dependent types in Haskell programming ==
  +
  +
=== Lightweight Dependent Typing ===
  +
[http://pobox.com/~oleg/ftp/Computation/lightweight-dependent-typing.html 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).
  +
  +
=== Library ===
  +
  +
[http://www.cs.st-and.ac.uk/~eb/ivor.php Ivor] is type theory based theorem proving library -- written by [http://www.dcs.st-and.ac.uk/~eb/index.php Edwin Brady] (see also the author's homepage, there are a lot of materials concerning dependent type theory there).
  +
  +
=== Proposals ===
 
John Hughes: [http://www.coverproject.org/TalksUntilSpring2004/DependentTypesInHaskell.pdf Dependent Types in Haskell (some ideas)].
 
John Hughes: [http://www.coverproject.org/TalksUntilSpring2004/DependentTypesInHaskell.pdf Dependent Types in Haskell (some ideas)].
   
== Simulating them ==
+
=== Simulating them ===
* [http://haskell.org/hawiki/SimulatingDependentTypes SimulatingDependentTypes] of HaWiki
+
* [http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.22.2636 Faking it: Simulating Dependent Types in Haskell], by Conor McBride
* [[Smart constructors]]
+
* <s>[http://haskell.org/hawiki/SimulatingDependentTypes SimulatingDependentTypes] of HaWiki</s> (404 Error)
* On the usefulness of such idioms in practice, see HaskellBD's [http://haskelldb.sourceforge.net/ updated] and [http://www.haskell.org/haskellDB/ original] pages
+
* The [[Type#See also|''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
  +
** [http://haskelldb.sourceforge.net/ updated] page (see ''Papers'' subsection on [http://haskelldb.sourceforge.net/#documentation Documentation])
  +
** which presupposes reading also paper on the [http://www.haskell.org/haskellDB/ original] page (see [http://www.haskell.org/haskellDB/doc.html Documentation subpage], PostScript version)
   
 
[[Category:Theoretical foundations]]
 
[[Category:Theoretical foundations]]
  +
  +
[[Category:Type-level programming]]

Revision as of 11:35, 16 June 2013

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

2.4 Cayenne

Cayenne is influenced also by constructive type theory.

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.

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