Personal tools

Dependent type

From HaskellWiki

(Difference between revisions)
Jump to: navigation, search
m (Using level 1 headlines for top-level structuring, according to HaskellWiki:Guidelines)
(Refining the structure: adding subsections ,,General'' to ,,Concept'', ,,Other Techniques'' to ,,Languages'')
Line 2: Line 2:
   
 
= The concept of dependent types =
 
= The concept of dependent types =
  +
  +
== General ==
  +
[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 ==
  +
...
  +
  +
== Illatice Combinatory Logic ==
   
 
To see how Illative [[CombinatoryLogic]] 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 [[CombinatoryLogic]] 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 16: Line 24:
   
 
= Dependently typed languages =
 
= Dependently typed languages =
  +
  +
== 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 23: Line 33:
 
Dependent types (of this language) also provide a not-forgetful concept of '''views''' (already mentioned in the Haskell [[Future]];
 
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'').
 
the connection between these concepts is described in p. 32 of Epigram Tutorial (section ''4.6 Patterns Forget; Matching Is Remembering'').
  +
  +
== Other techniques ==
  +
  +
[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 16:46, 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

...

1.3 Illatice 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