Personal tools

Dependent type

From HaskellWiki

(Difference between revisions)
Jump to: navigation, search
m (Link to Combinatory Logic wiki page)
m (Using level 1 headlines for top-level structuring, according to HaskellWiki:Guidelines)
Line 1: Line 1:
 
__TOC__
 
__TOC__
   
== The concept of dependent types ==
+
= The concept of dependent types =
   
 
[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
Line 15: Line 15:
   
   
== Dependently typed languages ==
+
= Dependently typed languages =
   
 
[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 24: Line 24:
 
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'').
   
== Dependent types in Haskell programming ==
+
= Dependent types in Haskell programming =
   
 
* 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)].

Revision as of 16:23, 1 March 2006

Contents


1 The concept of dependent types

Dependent Types in Programming abstract in APPSEM'2000

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

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

3 Dependent types in Haskell programming