# Difference between revisions of "Dependent type"

EndreyMark (talk | contribs) m (Specifying exactly which papers are meant as I referred to HaskelDB) |
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) |
||

Line 48: | Line 48: | ||

== Simulating them == |
== Simulating them == |
||

* [http://haskell.org/hawiki/SimulatingDependentTypes SimulatingDependentTypes] of HaWiki |
* [http://haskell.org/hawiki/SimulatingDependentTypes SimulatingDependentTypes] of HaWiki |
||

− | * [[Smart constructors]] |
||

+ | * 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 |
* On the usefulness of such idioms in practice, see HaskellDB's pages |
||

** [http://haskelldb.sourceforge.net/ updated] page (see ''Papers'' subsection on [http://haskelldb.sourceforge.net/#documentation Documentation]) |
** [http://haskelldb.sourceforge.net/ updated] page (see ''Papers'' subsection on [http://haskelldb.sourceforge.net/#documentation Documentation]) |

## Revision as of 12:56, 6 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 Curry-Howard 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 first-order 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 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

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

- updated page (see