Personal tools

Dependent type

From HaskellWiki

(Difference between revisions)
Jump to: navigation, search
m (,,Illative'' misstype corrected)
(Links on Curry-Howard isomorphism added to ,,Concept'' section / ,,TypeTheory'' subsection)
Line 9: Line 9:
   
 
== 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,
  +
the book seemed cathartic for me even from its beginning.
  +
  +
[http://lists.seas.upenn.edu/mailman/listinfo/types-list Types Forum]
   
 
== Illative Combinatory Logic ==
 
== Illative Combinatory Logic ==
Line 36: Line 36:
 
== 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 =

Revision as of 17:19, 1 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 CombinatoryLogic 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 Other techniques

APPSEM Workshop on Subtyping & Dependent Types in Programming

3 Dependent types in Haskell programming