Difference between revisions of "Dependent type"
EndreyMark (talk | contribs) m (/Qi*/ Typographic correction) |
(→Cayenne: links updated; link added for constructive type theory) |
||
(14 intermediate revisions by 13 users not shown) | |||
Line 4: | Line 4: | ||
=== General === |
=== General === |
||
⚫ | |||
⚫ | |||
− | [http://www-sop.inria.fr/oasis/Caminha00/abstract.html Dependent Types in Programming] abstract in APPSEM'2000 |
+ | * [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 === |
||
Line 34: | Line 36: | ||
[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:// |
+ | * [http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.115.9718&rep=rep1&type=pdf Epigram Tutorial] by Conor McBride |
− | * and [http:// |
+ | * 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#Extensions of Haskell]]; |
+ | 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''). |
||
Line 44: | Line 46: | ||
=== Agda === |
=== Agda === |
||
− | + | [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. |
||
Line 50: | Line 52: | ||
=== Cayenne === |
=== Cayenne === |
||
− | [http://www. |
+ | [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 |
+ | 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]]. |
|
⚫ | |||
− | === Qi === |
||
+ | === Lightweight Dependent Typing === |
||
− | [http://www.lambdassociates.org/ 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 [http://www.lambdassociates.org/advtypes.htm a very powerful type system]. |
||
+ | [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 |
||
− | === Other techniques === |
||
+ | the elimination |
||
− | |||
+ | of array bound check (even in such complex algorithms as Knuth-Morris-Pratt |
||
− | Also [http://www.defmacro.org/blaise/faq.html Blaise] is a Lisp-based language with dependent types. It will be released under GPL, but has not yet a released implementation. |
||
+ | string search). The page also briefly describes `singleton types' (Hayashi and |
||
− | |||
+ | Xi). |
||
− | [http://www-sop.inria.fr/oasis/DTP00/ APPSEM Workshop on Subtyping & Dependent Types in Programming] |
||
− | |||
⚫ | |||
=== Library === |
=== Library === |
||
− | [http://www. |
+ | [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 === |
=== Proposals === |
||
Line 76: | Line 76: | ||
=== Simulating them === |
=== Simulating them === |
||
+ | * [http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.22.2636 Faking it: Simulating Dependent Types in Haskell], by Conor McBride |
||
− | * [http://haskell.org/hawiki/SimulatingDependentTypes SimulatingDependentTypes] of HaWiki |
+ | * <s>[http://haskell.org/hawiki/SimulatingDependentTypes SimulatingDependentTypes] of HaWiki</s> (404 Error) |
* 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. |
* 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 |
* On the usefulness of such idioms in practice, see HaskellDB's pages |
||
Line 83: | Line 84: | ||
[[Category:Theoretical foundations]] |
[[Category:Theoretical foundations]] |
||
+ | |||
+ | [[Category:Type-level programming]] |
Revision as of 20:29, 8 August 2012
The concept of dependent types
General
- Wikipedia
- Dependent Types in Programming abstract in APPSEM'2000
- Do we need dependent types? by Daniel Fridlender and Mia Indrika, 2001.
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.
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 of Epigram corresponds to in Illative Combinatory Logic. I think e.g. the followings should correspond to each other:
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.
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.
Dependent types in Haskell programming
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).
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
John Hughes: Dependent Types in Haskell (some ideas).
Simulating them
- Faking it: Simulating Dependent Types in Haskell, by Conor McBride
SimulatingDependentTypes of HaWiki(404 Error)- 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)