<p>There are a few different ways of approaching this:</p>

<ol>
<li><p><strong>Dependent Type Theory</strong>.
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.</p></li>
<li><p><strong>Theorem proving</strong>. Firstly, take a look at my answer to a related question: <a href="https://cstheory.stackexchange.com/questions/5836/how-would-i-go-about-learning-the-underlying-theory-of-the-coq-proof-assistant">How would I go about learning the underlying theory of the Coq proof assistant?</a>. </p></li>
<li><p><strong>Programming with dependent types</strong>. Looking at recent languages with dependent types  such as <a href="http://en.wikipedia.org/wiki/Epigram_%28programming_language%29" rel="nofollow noreferrer">Epigram</a> or <a href="http://wiki.portal.chalmers.se/agda/pmwiki.php" rel="nofollow noreferrer">Agda</a> or less recent ones such as <a href="http://www.cs.bu.edu/~hwxi/DML/DML.html" rel="nofollow noreferrer">Dependent ML</a> and writing some programs will help solidify the ideas. Epigram, for example, is extremely clean in design. Another angle is to see <a href="https://www.andres-loeh.de/LambdaPi/" rel="nofollow noreferrer">how dependent types are implemented</a>. One practical dependent type theory is <a href="https://www.andres-loeh.de/PiSigma/PiSigma.pdf" rel="nofollow noreferrer"><span class="math-container">$\Pi\Sigma$</span>: Dependent Types without the sugar.</a> Several PhD theses are devoted to programming with dependent type theory: <a href="http://www.google.be/url?sa=t&amp;source=web&amp;cd=3&amp;ved=0CCwQFjAC&amp;url=http://www.cs.cmu.edu/~drl/pubs/thesis/thesis.pdf&amp;ei=bRSrTdawL42gOpC2kYEK&amp;usg=AFQjCNEvdramjks4Sk6aSpep-q03MY6i_w&amp;sig2=hou1HQ24nsUBH7F8gDNmDw" rel="nofollow noreferrer">Dan Licata's</a>, <a href="http://www.cse.chalmers.se/~nad/publications/danielsson-phd.pdf" rel="nofollow noreferrer">Nils Anders Danielsson's</a>, <a href="http://www.cse.chalmers.se/~ulfn/papers/thesis.pdf" rel="nofollow noreferrer">Ulf Norrel's</a>, <a href="http://www.cl.cam.ac.uk/~ss726/papers/thesis.pdf" rel="nofollow noreferrer">Susmit Sarkar's</a>, among others. And of course there's Adam Chlipala's book, given in Marc Hamann's answer.</p></li>
</ol>

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

CC BY-SA 3.0
2011-04-17T23:01:06.473Z
I can find papers for Epigram, but I can't find an actual download for Epigram, only the yet unfinished Epigram 2. Any ideas?
John Salvatier
CC BY-SA 3.0
2011-04-18T06:39:15.017Z
Did you find: http://www.e-pig.org/darcs/Pig09/web/? Epigram is available at the bottom of the page.
Dave Clarke
CC BY-SA 3.0
2014-03-26T00:31:32.933Z
Epigram 1 is essentially unmaintained since quite a while AFAIK — the author uses Agda these days (while working on Epigram 2 to the side).
Blaisorblade
CC BY-SA 4.0
2019-05-18T05:17:06.797Z
In 2019, I don't think Epigram 2 is ever going to happen - but there's Idris (and Idris 2!) now.
xrq
CC BY-SA 4.0
2011-04-17T16:33:18.097Z
2018-10-12T07:42:32.097Z
2018-10-12T07:42:32.097Z
Dave Clarke
<p>The $\lambda\pi$ calculus &mdash;which is essentially the core of LF, in turn the most widely reimplemented approach to higher-order logic&mdash; 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.</p>

<p>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.</p>

<p>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.</p>

CC BY-SA 3.0
2011-04-20T09:45:19.180Z
2011-04-20T09:56:53.163Z
2011-04-20T09:56:53.163Z
Charles Stewart
<p>CoC is most likely the way to go.  Just dive into <a href="http://coq.inria.fr/">Coq</a> and work through a nice tutorial like <a href="http://www.cis.upenn.edu/~bcpierce/sf/">Software Foundations</a> (which Pierce of TaPL and ATTaPL is involved in).</p>

<p>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.</p>

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

<p>(Another, slightly more advanced tutorial is Adam Chlipala's <a href="http://adam.chlipala.net/cpdt/">Certified Programming with Dependent Types</a>)</p>

CC BY-SA 3.0
2011-04-20T09:50:12.920Z
"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".
Charles Stewart
CC BY-SA 3.0
2011-04-20T11:55:54.567Z
@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.
Marc Hamann
CC BY-SA 3.0
2011-04-17T16:01:13.633Z
2011-04-17T16:01:13.633Z
Marc Hamann
<p>I thought this article helped demystify the concept at an elementary level: <a href="http://golem.ph.utexas.edu/category/2010/03/in_praise_of_dependent_types.html" rel="nofollow">http://golem.ph.utexas.edu/category/2010/03/in_praise_of_dependent_types.html</a></p>

CC BY-SA 3.0
2011-06-06T05:53:08.387Z
2011-06-06T05:53:08.387Z
solrize
<p>Take a look at <a href="http://www2.tcs.ifi.lmu.de/~abel/talkDTP2011.pdf" rel="nofollow">http://www2.tcs.ifi.lmu.de/~abel/talkDTP2011.pdf</a> and an older PiSigma system mentioned there.</p>

CC BY-SA 3.0
2011-11-09T16:24:29.327Z
2011-11-09T16:24:29.327Z
nponeccop
<p>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 <a href="http://www.cis.upenn.edu/~bcpierce/attapl/">ATTaPL</a>. I've also read and skimmed a bunch of articles on dependent typing.</p>

<p>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.</p>

<p>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)</p>

<ul>
<li>Generalized abstraction (can have functions from any domain in the type hierarchy to other, kind -> term, term->type''' etc.)</li>
<li>Has an infinite hierarchy of typing (terms : types : types' : types'' : ...)</li>
<li>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. </li>
<li>Sum and product types are derivable.</li>
</ul>

<p>I am also looking for an explanation of that language which ideally would discuss:</p>

<ul>
<li>The relationship between abstraction and quantification in that language. If they are not unified, then explain why they are not unified.</li>
<li>The infinite type hierarchy explicitly</li>
</ul>

<p>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.</p>

<p><a href="http://www.reddit.com/r/dependent_types/comments/grzfc/what_is_the_most_intuitive_dependent_type_theory/">(Cross posted to Reddit)</a></p>

<lo.logic><type-theory><dependent-type>
What is the most intuitive dependent type theory I could learn?
John Salvatier
# What is the most intuitive dependent type theory I could learn?

(Asked by: username_0 on 2011-04-17)

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](http://www.cis.upenn.edu/~bcpierce/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)](http://www.reddit.com/r/dependent_types/comments/grzfc/what_is_the_most_intuitive_dependent_type_theory/)

**Tags:** lo.logic, type-theory, dependent-type


---

## 5 answers

### Answer by username_1 on 2011-04-17. Score: 36

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?](https://cstheory.stackexchange.com/questions/5836/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](http://en.wikipedia.org/wiki/Epigram_%28programming_language%29) or [Agda](http://wiki.portal.chalmers.se/agda/pmwiki.php) or less recent ones such as [Dependent ML](http://www.cs.bu.edu/~hwxi/DML/DML.html) 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](https://www.andres-loeh.de/LambdaPi/). One practical dependent type theory is [$\Pi\Sigma$: Dependent Types without the sugar.](https://www.andres-loeh.de/PiSigma/PiSigma.pdf) Several PhD theses are devoted to programming with dependent type theory: [Dan Licata's](http://www.google.be/url?sa=t&source=web&cd=3&ved=0CCwQFjAC&url=http://www.cs.cmu.edu/~drl/pubs/thesis/thesis.pdf&ei=bRSrTdawL42gOpC2kYEK&usg=AFQjCNEvdramjks4Sk6aSpep-q03MY6i_w&sig2=hou1HQ24nsUBH7F8gDNmDw), [Nils Anders Danielsson's](http://www.cse.chalmers.se/~nad/publications/danielsson-phd.pdf), [Ulf Norrel's](http://www.cse.chalmers.se/~ulfn/papers/thesis.pdf), [Susmit Sarkar's](http://www.cl.cam.ac.uk/~ss726/papers/thesis.pdf), among others. And of course there's Adam Chlipala's book, given in username_5's answer.

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

> **Comments:**
> **username_0**: I can find papers for Epigram, but I can't find an actual download for Epigram, only the yet unfinished Epigram 2. Any ideas?  
> **username_1**: Did you find: http://www.e-pig.org/darcs/Pig09/web/? Epigram is available at the bottom of the page.  
> **username_2**: Epigram 1 is essentially unmaintained since quite a while AFAIK — the author uses Agda these days (while working on Epigram 2 to the side).  
> **username_3**: In 2019, I don't think Epigram 2 is ever going to happen - but there's Idris (and Idris 2!) now.  

---

### Answer by username_4 on 2011-04-20. Score: 15

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.


---

### Answer by username_5 on 2011-04-17. Score: 10

CoC is most likely the way to go. Just dive into [Coq](http://coq.inria.fr/) and work through a nice tutorial like [Software Foundations](http://www.cis.upenn.edu/~bcpierce/sf/) (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](http://adam.chlipala.net/cpdt/))

> **Comments:**
> **username_4**: "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".  
> **username_5**: @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.  

---

### Answer by username_6 on 2011-06-06. Score: 4

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>


---

### Answer by username_7 on 2011-11-09. Score: 2

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


---

