Difference between revisions of "Dependent type"

From HaskellWiki
Jump to: navigation, search
(Categorizing this article, creating a new category ,,Theoretical foundations'')
(Adding a new section ,,Simulating them [dependent types in Haskell]''. Links to wikipages: how to achieve static type checks instead of runtime assertions. Link to Smart constructors wikipage)
Line 43: Line 43:
= Dependent types in Haskell programming =
= Dependent types in Haskell programming =
== 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 ==
* [http://haskell.org/hawiki/SimulatingDependentTypes SimulatingDependentTypes] of HaWiki
* [http://haskell.org/hawiki/SimulatingDependentTypes SimulatingDependentTypes] of HaWiki
* [[Smart constructors]]
[[Category:Theoretical foundations]]
[[Category:Theoretical foundations]]

Revision as of 10:35, 6 March 2006

The concept of dependent types



Dependent Types in Programming abstract in APPSEM'2000

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

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}

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

Other techniques

APPSEM Workshop on Subtyping & Dependent Types in Programming

Dependent types in Haskell programming


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

Simulating them