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?
$\begingroup$
$\endgroup$
6
-
$\begingroup$ Which dependent type system? $\endgroup$– xrqJun 21, 2018 at 14:25
-
$\begingroup$ Whichever is the strongest and provides the more comprehensive guarantees. Maybe Agda? Idris? $\endgroup$– Rusty FieldstoneJun 22, 2018 at 15:17
-
3$\begingroup$ Yes, Zermelo-Fraenkel set theory. What's the purpose of this question? $\endgroup$– Andrej BauerJun 25, 2018 at 16:16
-
$\begingroup$ 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. $\endgroup$– Rusty FieldstoneJun 27, 2018 at 2:50
-
$\begingroup$ ... also, for theories to learn more about: Homotopy type theory. $\endgroup$– Rusty FieldstoneJun 27, 2018 at 2:56
|
Show 1 more comment
2 Answers
$\begingroup$
$\endgroup$
1
One obvious missing feature from most dependent type theories is the ability for substructural reasoning.
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. This seems to be an important active research subject in the PL community.
A possible reference is Wadler, Linear Types can Change the World!
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.
-
$\begingroup$ 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... $\endgroup$– xrqJun 26, 2018 at 1:49
$\begingroup$
$\endgroup$
0
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
