Personal tools

Dependent type

From HaskellWiki

(Difference between revisions)
Jump to: navigation, search
m (typographic correction)
m (Using == ... == as top level headlines (according to HaskellWiki:Guidelines#Headlines))
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://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-sop.inria.fr/oasis/Caminha00/abstract.html Dependent Types in Programming] abstract in APPSEM'2000
   
== 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,
Line 15: Line 15:
 
[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 27: Line 27:
   
   
= 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
Line 38: Line 38:
 
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'').
   
== 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/~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.“
Line 44: Line 44:
 
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.
   
== Cayene ==
+
=== Cayene ===
   
 
[http://www.cs.chalmers.se/~augustss/cayenne/index.html Cayene] 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.
 
[http://www.cs.chalmers.se/~augustss/cayenne/index.html Cayene] 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.
   
== Other techniques ==
+
=== Other techniques ===
   
 
[http://www-sop.inria.fr/oasis/DTP00/ APPSEM Workshop on Subtyping & Dependent Types in Programming]
 
[http://www-sop.inria.fr/oasis/DTP00/ APPSEM Workshop on Subtyping & Dependent Types in Programming]
   
= Dependent types in Haskell programming =
+
== Dependent types in Haskell programming ==
== Proposals ==
+
=== 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://haskell.org/hawiki/SimulatingDependentTypes SimulatingDependentTypes] of HaWiki
 
* The ''See also'' section of [[Type]] page contains links to many related idioms.
 
* The ''See also'' section of [[Type]] page contains links to many related idioms.

Revision as of 21:23, 31 March 2006

Contents


1 The concept of dependent types

1.1 General

Wikipedia

Dependent Types in Programming abstract in APPSEM'2000

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.

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; the connection between these concepts is described in p. 32 of Epigram Tutorial (section 4.6 Patterns Forget; Matching Is Remembering).

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 very similar to cayenne and agda is intended to be a (almost) full implementation of it in the future.“

People who are interested also in theorem proving may see the theorem provers page.

2.3 Cayene

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

2.4 Other techniques

APPSEM Workshop on Subtyping & Dependent Types in Programming

3 Dependent types in Haskell programming

3.1 Proposals

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

3.2 Simulating them