Difference between revisions of "Dependent type"
EndreyMark (talk | contribs) m (Link to Combinatory Logic wiki page) |
EndreyMark (talk | contribs) m (Using level 1 headlines for top-level structuring, according to HaskellWiki:Guidelines) |
||
| Line 1: | Line 1: | ||
__TOC__ |
__TOC__ |
||
| − | + | = 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 = |
|
[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 = |
|
* 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
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 of Epigram corresponds to in Illative Combinatory Logic. I think e.g. the followings should correspond to each other:
Dependently typed languages
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).
Dependent types in Haskell programming
- John Hughes: Dependent Types in Haskell (some ideas).
- SimulatingDependentTypes of HaWiki