48
$\begingroup$

I am interested in getting a really solid grasp on dependent typing. I've read most of TaPL and read (if not fully absorbed) 'Dependent Types' in ATTaPL. I've also read and skimmed a bunch of articles on dependent typing.

Many type theory discussions seem to focus on adding incremental features to previous type systems, not "what's the next large generalization up from type system X?". Dependent types seem to be the next large generalization from System F, but I have yet to find the intuitive, canonical dependently typed language. The many references to Calculus of (inductive) Constructions makes me think CoC is that language, but the explanations of the language I have seen don't seem very clear or intuitive to me.

I am expecting/guessing such a language would have features like: (and please let me know if anything in particular jumps out as confused or unrealistic)

  • Generalized abstraction (can have functions from any domain in the type hierarchy to other, kind -> term, term->type''' etc.)
  • Has an infinite hierarchy of typing (terms : types : types' : types'' : ...)
  • A minimum number of basic elements. I am imagining that the language only asserts a single element for each level. For example it might assert that (() : Unit : Type : Type' : ...). Other elements are built from these elements.
  • Sum and product types are derivable.

I am also looking for an explanation of that language which ideally would discuss:

  • The relationship between abstraction and quantification in that language. If they are not unified, then explain why they are not unified.
  • The infinite type hierarchy explicitly

I am asking this question because I want to learn dependent type theory but also because I want to put together a guide that, assuming a little CS background, teaches the use of and how to understand proof assistants and dependently typed languages.

(Cross posted to Reddit)

Improve this question
$\endgroup$

5 Answers 5

Reset to default
36
$\begingroup$

There are a few different ways of approaching this:

  1. Dependent Type Theory. This is probably not the easiest way of learning about dependent types, but you could look at the Calculus of Constructions papers and their variants, Pure Type Systems, and Martin Hofmann's article on the Syntax and Semantics of Dependent Types, for example.

  2. Theorem proving. Firstly, take a look at my answer to a related question: How would I go about learning the underlying theory of the Coq proof assistant?.

  3. Programming with dependent types. Looking at recent languages with dependent types such as Epigram or Agda or less recent ones such as Dependent ML and writing some programs will help solidify the ideas. Epigram, for example, is extremely clean in design. Another angle is to see how dependent types are implemented. One practical dependent type theory is $\Pi\Sigma$: Dependent Types without the sugar. Several PhD theses are devoted to programming with dependent type theory: Dan Licata's, Nils Anders Danielsson's, Ulf Norrel's, Susmit Sarkar's, among others. And of course there's Adam Chlipala's book, given in Marc Hamann's answer.

I'd be inclined to start with programming, before moving to using theorem proving, then start exploring the more theoretical issues.

Improve this answer
$\endgroup$
4
  • $\begingroup$ I can find papers for Epigram, but I can't find an actual download for Epigram, only the yet unfinished Epigram 2. Any ideas? $\endgroup$
    – John Salvatier
    Commented Apr 17, 2011 at 23:01
  • 1
    $\begingroup$ Did you find: e-pig.org/darcs/Pig09/web? Epigram is available at the bottom of the page. $\endgroup$
    – Dave Clarke
    Commented Apr 18, 2011 at 6:39
  • 3
    $\begingroup$ Epigram 1 is essentially unmaintained since quite a while AFAIK — the author uses Agda these days (while working on Epigram 2 to the side). $\endgroup$
    – Blaisorblade
    Commented Mar 26, 2014 at 0:31
  • $\begingroup$ In 2019, I don't think Epigram 2 is ever going to happen - but there's Idris (and Idris 2!) now. $\endgroup$
    – xrq
    Commented May 18, 2019 at 5:17
15
$\begingroup$

The $\lambda\pi$ calculus —which is essentially the core of LF, in turn the most widely reimplemented approach to higher-order logic— is by far the simplest dependently typed system you can learn, since it consists just of the extension of the type system of the simply typed lambda calculus with dependently typed quantifiers. So the key intuitions needed to master LF are intuitions you need to master with any theory with dependent types.

Twelf is a good theorem-proving system based on LF. Looking over the advanced course notes offered by Frank Pfenning are a good introduction to the theory and practice of LF.

That said, it is perhaps not the best first system to learn if your interest is in constructive mathematics rather than the essentials of type theory: LF means logical framework and it is a system used to axiomatise theories, and is not so often worked in as a target system directly. Using a system based on Martin-Loef's type theory is probably the best introduction -Dave mentions Agda, among others- is maybe a better starting point if this is your goal, since you can get going with arithmetic and inductive types more quickly in such a framework.

Improve this answer
$\endgroup$
10
$\begingroup$

CoC is most likely the way to go. Just dive into Coq and work through a nice tutorial like Software Foundations (which Pierce of TaPL and ATTaPL is involved in).

Once you get a feel for the practical aspects of the dependent typing, go back to the theoretical sources: they'll make a lot more sense then.

Your list of features sounds basically correct, but seeing how they play out in practice is worth a thousand feature points.

(Another, slightly more advanced tutorial is Adam Chlipala's Certified Programming with Dependent Types)

Improve this answer
$\endgroup$
2
  • $\begingroup$ "intuitive" is maybe the sticking point here: there's a lot more intuitions flying about in CoC/CIC than just dependent typing. It's a good final goal –to my mind the choice is really between Coq and Twelf– but maybe not the best first step towards "getting a really solid grasp on dependent typing". $\endgroup$
    – Charles Stewart
    Commented Apr 20, 2011 at 9:50
  • $\begingroup$ @Charles: Your point is taken. I still think from a practical point of view it is a good bet. Even though a full understanding of CoC/CIC might be a more complex undertaking, Coq (plus the existence of good basic level tutorials for it) makes it easy to focus on learning just the programming aspects or just the basic proof-assistant aspects (as your interests dictate) even before you have grasped all the complexities. I think this qualifies as "intuitive" for someone not coming from a theoretical background. $\endgroup$
    – Marc Hamann
    Commented Apr 20, 2011 at 11:55
4
$\begingroup$

I thought this article helped demystify the concept at an elementary level: http://golem.ph.utexas.edu/category/2010/03/in_praise_of_dependent_types.html

Improve this answer
$\endgroup$
2
$\begingroup$

Take a look at http://www2.tcs.ifi.lmu.de/~abel/talkDTP2011.pdf and an older PiSigma system mentioned there.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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