Difference between revisions of "Dependent type"
EndreyMark (talk  contribs) (Linking with other wikipage: (1) a link back to Libraries and tools/Theorem provers (2) A more precise link (anchored to a section) to Type#See also) 
(→Epigram: Added the link to the Epigram site again) 

(29 intermediate revisions by 17 users not shown)  
Line 4:  Line 4:  
=== General === 
=== General === 

⚫  
⚫  
⚫  
⚫  
+  * [http://www.brics.dk/RS/01/10/BRICSRS0110.ps.gz Do we need dependent types?] by Daniel Fridlender and Mia Indrika, 2001. 

⚫  
+  
⚫  
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 CurryHoward 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 CurryHoward 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 CurryHoward isomorphism and the concept of dependent type: [http://www.cs.chalmers.se/~aarne/courselangtech/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 Haskellrelated approaches to linguisticshis online course and other linguistical materials on the Linguistics wikipage]]. 

[http://lists.seas.upenn.edu/mailman/listinfo/typeslist Types Forum] 
[http://lists.seas.upenn.edu/mailman/listinfo/typeslist Types Forum] 

−  === Illative 
+  === 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 firstorder 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 firstorder propositional and predicate calculus] by Henk Barendregt, Martin Bunder, Wil Dekkers. 

Line 31:  Line 35:  
=== Epigram === 
=== Epigram === 

−  [http://www.epig.org/ Epigram] is a full dependently typed programming language see especially 
+  [http://www.epig.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 notforgetful concept of '''views''' (already mentioned in the Haskell [[Future]]; 
+  Dependent types (of this language) also provide a notforgetful 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 42:  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 Haskelllike syntax. 

People who are interested also in theorem proving may see the [[Libraries and tools/Theorem proverstheorem provers]] page. 
People who are interested also in theorem proving may see the [[Libraries and tools/Theorem proverstheorem provers]] page. 

−  === 
+  === Idris === 
−  [http://www.cs.chalmers.se/~augustss/cayenne/index.html Cayenne] is influenced also by constructive type theory (see its page). 

+  [http://idrislang.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 Haskelllike 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.standrews.ac.uk/ University of St. Andrews]. 

⚫  
+  === Cayenne === 

−  === Other techniques === 

−  [http://wwwsop.inria.fr/oasis/DTP00/ APPSEM Workshop on Subtyping & Dependent Types in Programming] 

+  [https://en.wikipedia.org/wiki/Cayenne_(programming_language) Cayenne] is influenced also by [http://en.wikipedia.org/wiki/Constructive_type_theory constructive type theory]. The compiler can be found at [https://github.com/csgordon/cayenne GitHub] 

+  
⚫  
+  
⚫  
== Dependent types in Haskell programming == 
== Dependent types in Haskell programming == 

+  
+  === Lightweight Dependent Typing === 

+  [http://okmij.org/ftp/Computation/lightweightdependenttyping.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 KnuthMorrisPratt 

+  string search). The page also briefly describes `singleton types' (Hayashi and 

+  Xi). 

+  
+  === Library === 

+  
+  [http://www.cs.stand.ac.uk/~eb/ivor.php Ivor] is type theory based theorem proving library  written by [http://www.dcs.stand.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 === 

−  +  * Richard A. Eisenberg: [https://arxiv.org/pdf/1610.07978.pdf Dependent Types in Haskell: Theory and Practice] 

+  * John Hughes: <s> [http://www.coverproject.org/TalksUntilSpring2004/DependentTypesInHaskell.pdf Dependent Types in Haskell (some ideas)]</s> (404). 

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

⚫  
⚫  
⚫  
* On the usefulness of such idioms in practice, see HaskellDB's pages 
* 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]) 
** [http://haskelldb.sourceforge.net/ updated] page (see ''Papers'' subsection on [http://haskelldb.sourceforge.net/#documentation Documentation]) 

Line 70:  Line 90:  
[[Category:Theoretical foundations]] 
[[Category:Theoretical foundations]] 

+  
+  [[Category:Typelevel programming]] 
Revision as of 11:37, 22 December 2018
Contents
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 CurryHoward isomorphism and the connections between logic and programming, the book seemed cathartic for me even from its beginning.
Another interesting approach to CurryHoward 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 firstorder 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 notforgetful 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 Haskelllike 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 Haskelllike 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 Firstclass 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 KnuthMorrisPratt 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)