Dependent Types

A function has dependent type if the type of a function's result depends on the VALUE of its argument; this is not the same thing as a ParameterizedType?. The second order lambda calculus possesses functions with dependent types.

Languages with dependent types:

• CayenneLanguage; "Cayenne a Language With Dependent Types" (1998) http://citeseer.ist.psu.edu/augustsson98cayenne.html
• XanaduLanguage?: http://www.cs.bu.edu/~hwxi/Xanadu/Xanadu.html
• EpigramLanguage?: http://cliki.tunes.org/Epigram

Why Dependent Types Matter http://www.cs.nott.ac.uk/~txa/talks/nijmegen-03.pdf

Dependent Types course handout http://www-2.cs.cmu.edu/~fp/courses/logic/handouts/dependent.pdf

Dependent types in practical programming (ACM subscription required) http://portal.acm.org/citation.cfm?id=292560&dl=ACM&coll=portal&CFID=11111111&CF TOKEN=2222222

Dynamic Typing With Dependent Types http://www.cs.princeton.edu/~gtan/paper/dynamic.pdf

mentioned in Formal Abstract Data Types http://www.cs.caltech.edu/~jyh/papers/depend/paper.ps

"Static Dependent Types for First Class Modules"

• "Static dependent types are the basis of a new type system that permits types and values to be packaged together into first class modules. Unlike other approaches to modules, static dependent types permit unrestricted access to the types and values in first class modules without sacrificing static type checking or data abstraction..."
• http://www.psrg.lcs.mit.edu/history/publications/Papers/lfp90abs.htm

Workshop on Subtyping & Dependent Types in Programming http://www-sop.inria.fr/oasis/DTP00/

Non-Dependent Types for Standard ML Modules http://www.dcs.ed.ac.uk/home/cvr/ppdp99.html

---

See MultiParadigmWeenie