Difference between revisions of "Dependent type"
EndreyMark (talk  contribs) (Replacing the Smart constructors link with Type link. So the reference became more general, because Smart constructors can be reached from Type) 
EndreyMark (talk  contribs) m (Dependent types moved to Dependent type) 
(No difference)

Revision as of 19:53, 25 March 2006
Contents
The concept of dependent types
General
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 CurryHoward isomorphism and the connections between logic and programming, the book seemed cathartic for me even from its beginning.
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 firstorder propositional and predicate calculus by Henk Barendregt, Martin Bunder, Wil Dekkers. It seems to me that the dependent type construct of Epigram corresponds to in Illative Combinatory Logic. I think e.g. the followings should correspond to each other:
Dependently typed languages
Epigram
Epigram is a full dependently typed programming language see especially
 Epigram Tutorial by Conor McBride
 and Why dependent types matter by Thorsten Altenkirch, Conor McBride and James McKinna).
Dependent types (of this language) also provide a notforgetful 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
Proposals
John Hughes: Dependent Types in Haskell (some ideas).
Simulating them
 SimulatingDependentTypes of HaWiki
 The See also section of Type page contains links to many related idioms.
 On the usefulness of such idioms in practice, see HaskellDB's pages
 updated page (see Papers subsection on Documentation)
 which presupposes reading also paper on the original page (see Documentation subpage, PostScript version)