13
$\begingroup$

I thought I understood dependent typing (DT) properly, but the answer to this question: https://cstheory.stackexchange.com/questions/30651/why-was-there-a-need-for-martin-l%C3%B6f-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.

Improve this question
$\endgroup$
9
  • 1
    $\begingroup$ Have you googled them? Have you heard of Coq, a theorem prover built on dependent types? Did you know that the 4 colour theorem has proven using Coq? $\endgroup$
    – Dave Clarke
    Mar 3, 2015 at 6:29
  • 2
    $\begingroup$ I did actually. What is hard to Google is what is that extra "power" (for lack of a better word) that DTs lend to type theory, intuitively speaking? $\endgroup$
    – PhD
    Mar 3, 2015 at 6:33
  • 1
    $\begingroup$ Why? Dependent types allow you to type more programs while still being type-safe. How? By parameterising types with programs. $\endgroup$
    – Martin Berger
    Mar 3, 2015 at 6:48
  • $\begingroup$ @MartinBerger - Can you please elaborate on "more programs"? What "more" can I do or need, from a theoretical standpoint? $\endgroup$
    – PhD
    Mar 3, 2015 at 6:49
  • 2
    $\begingroup$ @DaveClarke That Coq, with its fancy types, has been used to do fancy things doesn't imply that those fancy things require those fancy types. For example Twelf has had major successes (such as a proof of correctness of SML), and it's only second-order, not higher-order. I've seen some pretty big systems proved with first-order logic only. $\endgroup$
    – Gilles 'SO- stop being evil'
    Mar 5, 2015 at 16:48

2 Answers 2

Reset to default
23
$\begingroup$

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.

$^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.

Improve this answer
$\endgroup$
6
  • $\begingroup$ Now, THAT makes a lot of sense. It may have been obvious but for some reason I couldn't lay a finger on it. Appreciate the transition from comment to answer. Unfortunately, the question has been voted for closing, but I'm glad for the answer :) $\endgroup$
    – PhD
    Mar 3, 2015 at 19:03
  • 1
    $\begingroup$ I'm not crazy about your example, since list length is just something you could erase in types and get programs talking about ordinary (un-indexed) lists. It might be useful to note that there are types that do not remain well-typed after this kind of erasure, e.g. a program of type $\mathrm{Arr}\ n$, where $\mathrm{Arr}\ 0 = \mathrm{nat}$ and $\mathrm{Arr}\ (n+1) = \mathrm{nat}\rightarrow\mathrm{Arr}\ n$. $\endgroup$
    – cody
    Apr 29, 2015 at 17:44
  • $\begingroup$ @cody I'm not sure what you mean. Dependent types have (or can be set up to have) type erasure in the following sense: for all typeable P: $P\Downarrow V$ iff $erase(P)\Downarrow erase(V)$, where $\Downarrow$ is the run-time reduction relation. (This is a simplified description where the function erase maps programs with type annotation to 'the same' programs without annotation.) Maybe you mean something different? $\endgroup$
    – Martin Berger
    Apr 30, 2015 at 3:47
  • $\begingroup$ @MartinBerger: yes in this case I'm talking about erasing dependencies in dependent types to get simple types. The only example I can point to right now is the proof that $F_\omega$ normalizes iff $\mathrm{CoC}$ normalizes (in e.g. Barendregt's book). $\endgroup$
    – cody
    Apr 30, 2015 at 12:26
  • $\begingroup$ @cody I think it's unusual to call this type erasure. What's a better name? Maybe type simplification? $\endgroup$
    – Martin Berger
    Apr 30, 2015 at 12:42
2
$\begingroup$

Think of type declarations as nothing more than assertions. Currently, all you can say is things like isInt32(), isCharPtr(), etc. These various assertions are chosen to be checkable at compile-time. But this concept can be expanded to things like: isCharPtr() && isNotNull(). Nullable pointers are a huge problem. Pointers should not be nullable as the default stance, with nullable pointers being a type that isn't dereferenceable without knowing whether it is null or not. Similar problems are things like: isPositiveInteger(), or isEvenNaturalNumber().

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.