<p>One obvious missing feature from most dependent type theories is the ability for <a href="https://en.wikipedia.org/wiki/Substructural_logic" rel="nofollow noreferrer">substructural reasoning</a>.</p>

<p>The guarantees given by systems like Agda and Coq tend to be very extensional, that is they enforce properties about the <em>values</em> of the computations, rather than their operation. Some obvious things we might want to track about the operation of an algorithm:</p>

<ul>
<li>Runtime</li>
<li>Space usage</li>
<li>Which resources they "own", e.g. which files they are allowed to access without risk of a race condition</li>
</ul>

<p>All these things (and more!) become possible with various flavors of <a href="https://en.wikipedia.org/wiki/Substructural_type_system" rel="nofollow noreferrer">substructural types</a>. This seems to be an important active research subject in the PL community.</p>

<p>A possible reference is Wadler, <em><a href="http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.55.5439&amp;rep=rep1&amp;type=pdf" rel="nofollow noreferrer">Linear Types can Change the World!</a></em></p>

<p>Note that using "deep embeddings", it is possible to enforce some of these properties in a standard dependent types system, see e.g. Brady &amp; Hammond <em><a href="https://pdfs.semanticscholar.org/8983/6d038b1a2e38a84843d579150a0eadbd1e2d.pdf" rel="nofollow noreferrer">Resource-safe Systems Programming with
Embedded Domain Specific Languages</a></em>.</p>

CC BY-SA 4.0
2018-06-26T01:49:28.100Z
It might be worth mentioning that dependent and linear types don't play very well together yet, at least they don't last time I looked this up...
xrq
CC BY-SA 4.0
2018-06-25T17:51:56.787Z
2018-06-25T17:51:56.787Z
cody
<p>I'm not an expert on dependent type theory, but I'd like to put in my 50 cents. Off the top of my head:</p>

<p>(1) Both Agda and Idris are based off Martin-Lof type theory (MLTT) without the Type : Type axiom so that they remain consistent. But notably, they don't support general recursion as a first-class citizen.</p>

<p>In Agda, there is no general <code>fix</code> operator. Only syntactic and structural recursion are allowed. In Idris, general recursion is allowed, but those which are not also syntactically and/or structurally recursive will be considered non-total by Idris and will not be expanded during type-checking, effectively making them second-class.</p>

<p>Now this is painful because many algorithms (like quicksort and the Euclidean algorithm) are easily proven to be total, but the termination checker can't prove that structurally. You can write them in a structurally recursive manner, but the process is painstaking and the result is often unreadable.</p>

<p>The transformation by Bove and Capretta (2005) mitigates this problem by allowing general recursive programs to be transformed into their structurally-recursive counterparts via an accessibility predicate. But then, AFAIK, I still have not seen a dependent type theory that fully integrates general recursion as a first-class citizen (via accessibility predicates or otherwise). But see Casinghino et al.'s 2014 POPL paper for a system that does the job pretty well (in a different way, though).</p>

<p><strong>Update</strong>: I came back to this answer just now, and find my characterization of the problem inaccurate. Adapting general recursion into dependent type theories should generally be undecidable and no good, but a limited form of general recursion --- namely provably terminating general recursion based on accessibility proofs --- should be possible. </p>

<p>In other words, what I'm thinking of is perhaps more similar to Coq's <code>Program Fixpoint</code>: however, instead of proof obligations on dependent types, I'd like to be able to program with proof obligations on termination. Naturally, this probably requires some termination proof terms in the type theory. But I am not sure.</p>

<p>(2) Equivalence in type theories like CoIC (Calculus of Inductive Constructions) and MLTT are not satisfactory. Specifically, there is proper equivalence on neither lambdas nor types. You can't express equivalence between functions as a first-class proof.</p>

<p>Homotopy type theory fixes this problem in a way that I don't claim to understand. But it would definitely be worthy to take a look at that. </p>

<hr>

<p>References:</p>

<p>Ana Bove and Venanzio Capretta. 2005. Modelling general recursion in type theory. <em>Mathematical Structures in Computer Science</em> 15. Cambridge University Press, Cambridge, UK, 671-708.  </p>

<p>Chris Casinghino, Vilhelm Sjöberg, and Stephanie Weirich. 2014. Combining proofs and programs in a dependently typed language. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '14). ACM, New York, NY, USA, 33-45.   </p>

<p>The Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study, Princeton, NJ, USA. <a href="https://homotopytypetheory.org/book" rel="nofollow noreferrer">https://homotopytypetheory.org/book</a>  </p>

CC BY-SA 4.0
2018-06-22T17:03:07.230Z
2018-06-29T14:49:41.690Z
2018-06-29T14:49:41.690Z
xrq
<p>It seems dependent types can provide lots of desirable guarantees about program behavior. What kinds of program properties can they NOT guarantee (besides what's computationally infeasible)? Is there an even more powerful or general type system that can model any computable property of a program? </p>

CC BY-SA 4.0
2018-06-21T14:25:12.390Z
*Which* dependent type system?
xrq
CC BY-SA 4.0
2018-06-22T15:17:58.483Z
Whichever is the strongest and provides the more comprehensive guarantees. Maybe Agda? Idris?
Rusty Fieldstone
CC BY-SA 4.0
2018-06-25T16:16:20.263Z
Yes, Zermelo-Fraenkel set theory. What's the purpose of this question?
Andrej Bauer
CC BY-SA 4.0
2018-06-27T02:50:53.643Z
The purpose of the question is to learn. I haven't found it clearly expressed what kinds of guarantees these more advanced type systems can and cannot provide. I appreciate getting some some targets for theory to learn about (e.g. Zermelo-Fraenkel set theory, substructural reasoning). I'd love to see guarantees of the kinds provided by dependent type systems make it into more mainstream languages. I'm also dabbling in PL design.
Rusty Fieldstone
CC BY-SA 4.0
2018-06-27T02:56:57.073Z
... also, for theories to learn more about: Homotopy type theory.
Rusty Fieldstone
CC BY-SA 4.0
2018-07-02T06:47:27.077Z
In that case, it seems this question belongs on cs.stackexchange.com. This forum is for research-level questions.
Andrej Bauer
<type-theory><type-systems><dependent-type>
What are the limitations of dependent typing?
Rusty Fieldstone
# What are the limitations of dependent typing?

(Asked by: username_0 on 2018-06-20)

It seems dependent types can provide lots of desirable guarantees about program behavior. What kinds of program properties can they NOT guarantee (besides what's computationally infeasible)? Is there an even more powerful or general type system that can model any computable property of a program?

**Tags:** type-theory, type-systems, dependent-type
> **Comments:**
> **username_1**: *Which* dependent type system?  
> **username_0**: Whichever is the strongest and provides the more comprehensive guarantees. Maybe Agda? Idris?  
> **username_2**: Yes, Zermelo-Fraenkel set theory. What's the purpose of this question?  
> **username_0**: The purpose of the question is to learn. I haven't found it clearly expressed what kinds of guarantees these more advanced type systems can and cannot provide. I appreciate getting some some targets for theory to learn about (e.g. Zermelo-Fraenkel set theory, substructural reasoning). I'd love to see guarantees of the kinds provided by dependent type systems make it into more mainstream languages. I'm also dabbling in PL design.  
> **username_0**: ... also, for theories to learn more about: Homotopy type theory.  
> **username_2**: In that case, it seems this question belongs on cs.stackexchange.com. This forum is for research-level questions.  

---

## 2 answers

### Answer by username_3 on 2018-06-25. Score: 3

One obvious missing feature from most dependent type theories is the ability for [substructural reasoning](https://en.wikipedia.org/wiki/Substructural_logic).

The guarantees given by systems like Agda and Coq tend to be very extensional, that is they enforce properties about the *values* of the computations, rather than their operation. Some obvious things we might want to track about the operation of an algorithm:

* Runtime
* Space usage
* Which resources they "own", e.g. which files they are allowed to access without risk of a race condition

All these things (and more!) become possible with various flavors of [substructural types](https://en.wikipedia.org/wiki/Substructural_type_system). This seems to be an important active research subject in the PL community.

A possible reference is Wadler, *[Linear Types can Change the World!](http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.55.5439&rep=rep1&type=pdf)*

Note that using "deep embeddings", it is possible to enforce some of these properties in a standard dependent types system, see e.g. Brady & Hammond *[Resource-safe Systems Programming with
Embedded Domain Specific Languages](https://pdfs.semanticscholar.org/8983/6d038b1a2e38a84843d579150a0eadbd1e2d.pdf)*.

> **Comments:**
> **username_1**: It might be worth mentioning that dependent and linear types don't play very well together yet, at least they don't last time I looked this up...  

---

### Answer by username_1 on 2018-06-22. Score: 2

I'm not an expert on dependent type theory, but I'd like to put in my 50 cents. Off the top of my head:

(1) Both Agda and Idris are based off Martin-Lof type theory (MLTT) without the Type : Type axiom so that they remain consistent. But notably, they don't support general recursion as a first-class citizen.

In Agda, there is no general `fix` operator. Only syntactic and structural recursion are allowed. In Idris, general recursion is allowed, but those which are not also syntactically and/or structurally recursive will be considered non-total by Idris and will not be expanded during type-checking, effectively making them second-class.

Now this is painful because many algorithms (like quicksort and the Euclidean algorithm) are easily proven to be total, but the termination checker can't prove that structurally. You can write them in a structurally recursive manner, but the process is painstaking and the result is often unreadable.

The transformation by Bove and Capretta (2005) mitigates this problem by allowing general recursive programs to be transformed into their structurally-recursive counterparts via an accessibility predicate. But then, AFAIK, I still have not seen a dependent type theory that fully integrates general recursion as a first-class citizen (via accessibility predicates or otherwise). But see Casinghino et al.'s 2014 POPL paper for a system that does the job pretty well (in a different way, though).

**Update**: I came back to this answer just now, and find my characterization of the problem inaccurate. Adapting general recursion into dependent type theories should generally be undecidable and no good, but a limited form of general recursion --- namely provably terminating general recursion based on accessibility proofs --- should be possible.

In other words, what I'm thinking of is perhaps more similar to Coq's `Program Fixpoint`: however, instead of proof obligations on dependent types, I'd like to be able to program with proof obligations on termination. Naturally, this probably requires some termination proof terms in the type theory. But I am not sure.

(2) Equivalence in type theories like CoIC (Calculus of Inductive Constructions) and MLTT are not satisfactory. Specifically, there is proper equivalence on neither lambdas nor types. You can't express equivalence between functions as a first-class proof.

Homotopy type theory fixes this problem in a way that I don't claim to understand. But it would definitely be worthy to take a look at that.

---

References:

Ana Bove and Venanzio Capretta. 2005. Modelling general recursion in type theory. *Mathematical Structures in Computer Science* 15. Cambridge University Press, Cambridge, UK, 671-708.

Chris Casinghino, Vilhelm Sjöberg, and Stephanie Weirich. 2014. Combining proofs and programs in a dependently typed language. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '14). ACM, New York, NY, USA, 33-45.

The Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study, Princeton, NJ, USA. <https://homotopytypetheory.org/book>


---

