https://wiki.haskell.org/api.php?action=feedcontributions&user=Bhterra&feedformat=atomHaskellWiki - User contributions [en]2021-01-24T16:58:52ZUser contributionsMediaWiki 1.27.4https://wiki.haskell.org/index.php?title=Dependent_type&diff=45462Dependent type2012-04-26T18:29:59Z<p>Bhterra: fixed link</p>
<hr />
<div>__TOC__<br />
<br />
== The concept of dependent types ==<br />
<br />
=== General ===<br />
<br />
* [http://en.wikipedia.org/wiki/Dependent_types Wikipedia]<br />
* [http://www-sop.inria.fr/oasis/Caminha00/abstract.html Dependent Types in Programming] abstract in APPSEM'2000<br />
* [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.<br />
<br />
<br />
=== Type theory ===<br />
<br />
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,<br />
the book seemed cathartic for me even from its beginning.<br />
<br />
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]].<br />
<br />
[http://lists.seas.upenn.edu/mailman/listinfo/types-list Types Forum]<br />
<br />
=== Illative combinatory logic ===<br />
<br />
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.<br />
It seems to me that the dependent type construct<br />
<math>\forall x : S \Rightarrow T</math><br />
of Epigram corresponds to<br />
<math>\mathbf G\;S\;(\lambda x . T)</math><br />
in Illative Combinatory Logic. I think e.g. the followings should correspond to each other:<br />
* <math>\mathrm{realNullvector} :\;\;\;\forall n: \mathrm{Nat} \Rightarrow \mathrm{RealVector}\;n</math><br />
* <math>\mathbf G\;\,\mathrm{Nat}\;\,\mathrm{RealVector}\;\,\mathrm{realNullvector}</math><br />
<br />
<br />
== Dependently typed languages ==<br />
<br />
=== Epigram ===<br />
<br />
[http://www.e-pig.org/ Epigram] is a full dependently typed programming language, see especially<br />
* [http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.115.9718&rep=rep1&type=pdf Epigram Tutorial] by Conor McBride<br />
* 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).<br />
<br />
Dependent types (of this language) also provide a not-forgetful concept of '''views''' (already mentioned in the Haskell [[Future of Haskell#Extensions of Haskell]];<br />
the connection between these concepts is described in p. 32 of Epigram Tutorial (section ''4.6 Patterns Forget; Matching Is Remembering'').<br />
<br />
See Epigram also as [[Libraries and tools/Theorem provers|theorem prover]].<br />
<br />
=== Agda ===<br />
<br />
[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.<br />
<br />
People who are interested also in theorem proving may see the [[Libraries and tools/Theorem provers|theorem provers]] page.<br />
<br />
=== Cayenne ===<br />
<br />
[http://www.cs.chalmers.se/~augustss/cayenne/index.html Cayenne] is influenced also by constructive type theory (see its page).<br />
<br />
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.<br />
<br />
Depandent types make it useful also as a [[Libraries and tools/Theorem provers|theorem prover]].<br />
<br />
== Dependent types in Haskell programming ==<br />
<br />
=== Lightweight Dependent Typing ===<br />
[http://pobox.com/~oleg/ftp/Computation/lightweight-dependent-typing.html This web page] describes the lightweight approach<br />
and its applications, e.g., statically safe head/tail functions and<br />
the elimination<br />
of array bound check (even in such complex algorithms as Knuth-Morris-Pratt<br />
string search). The page also briefly describes `singleton types' (Hayashi and<br />
Xi).<br />
<br />
=== Library ===<br />
<br />
[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).<br />
<br />
=== Proposals ===<br />
John Hughes: [http://www.coverproject.org/TalksUntilSpring2004/DependentTypesInHaskell.pdf Dependent Types in Haskell (some ideas)].<br />
<br />
=== Simulating them ===<br />
* [http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.22.2636 Faking it: Simulating Dependent Types in Haskell], by Conor McBride<br />
* <s>[http://haskell.org/hawiki/SimulatingDependentTypes SimulatingDependentTypes] of HaWiki</s> (404 Error)<br />
* 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.<br />
* On the usefulness of such idioms in practice, see HaskellDB's pages<br />
** [http://haskelldb.sourceforge.net/ updated] page (see ''Papers'' subsection on [http://haskelldb.sourceforge.net/#documentation Documentation])<br />
** 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)<br />
<br />
[[Category:Theoretical foundations]]<br />
<br />
[[Category:Type-level programming]]</div>Bhterra