I thought I understood dependent typing (DT) properly, but the answer to this question: Why was there a need for Martin-Löf to create intuitionistic type theory? has had me thinking otherwise.
After reading up on DT and trying to understand what they are, I'm trying to wonder, what do we gain by this notion of DTs? They seem to be more flexible and powerful than simply typed lambda calculus (STLC), although I can't understand "how/why" exactly.
What is that we can do with DTs that cannot be done with STLC? Seems like adding DTs makes the theory more complicated, but what's the benefit?
From the answer to the above question:
Dependent types were proposed by de Bruijn and Howard who wanted to extend the Curry-Howard correspondence from propositional to first-order logic.
This seems to make sense at some level, but I'm still unable to grasp the big-picture of "how/why"? Maybe an example explicitly show this extension of the C-H correspondence to FO logic could help hit the point home in understanding what is the big deal with DTs? I'm not sure I comprehend this as well I ought to.
Asked By : PhD
Answered By : Martin Berger
Expanding my comment: Dependent types can type more programs. "More" simply means that the set of programs typable with dependent types is a proper superset of the programs typable in the simply-typed $\lambda$-calculus (STLC). An example would be $List_{2*3+4}(\alpha)$, the lists of length $10$, carrying elements of type $\alpha$. The expression $2*3+4$ is at the same time a program and part of a type. You cannot do this in the STLC.
The key rule that distinguishes dependent from non-dependent types is application:
$$ \newcommand{\TYPES}[3]{#1 \vdash #2 : #3} \newcommand{\SUBST}[2]{\{#1/#2\}} \frac{ \TYPES{\Gamma}{\color{red}{M}}{A \rightarrow B} \qquad \TYPES{\Gamma}{\color{red}{N}}{A} }{ \TYPES{\Gamma}{\color{red}{MN}}{B} } \qquad \frac{ \TYPES{\Gamma}{{\color{red}M}}{\Pi x^A. B} \qquad \TYPES{\Gamma}{\color{red}{N}}{A} }{ \TYPES{\Gamma}{{\color{red}{MN}}}{B\SUBST{{\color{red}N}}{x}} } $$
On the left you have the STLC, where programs in the premises 'flow' only into the program of the conclusion. In contrast, in the dependent application rule on the right, the program $N$ from the right premise 'flows' into the type in the conclusion$^1$.
In order to be able to parameterise types by programs, the syntax of dependent types must be richer, and to ensure that types are well-formed we use a second 'typing system' called kinds that constrains the types. This kinding system is essentially the STLC, but "one level up".
There are many explanations of dependent types. Some examples.
- Dependent Types at Work, by Bove and Dybjer.
- Dependent Types, by Aspinall and Hofmann.
- Dependently Typed Programming in Agda, by Norell and Chapman.
- Lambda Calculi with Types, by Barendregt.
$^1$ In terms of colours: with non-dependent types, black expressions in the conclusion are constructed from black expressions in the premises while red expressions in the conclusion are constructed from red expressions in the premises. With dependent types the colours can be mixed by having black parts of the conclusion being constructed from red and black parts of the premise.
Best Answer from StackOverflow
Question Source : http://cs.stackexchange.com/questions/40097
0 comments:
Post a Comment
Let us know your responses and feedback