3 ms·
Decidability is not really important for type systems. As long as the type system is sound, you're good. If your compilation is taking too long, I would classif
by tathougies 10y ago
Decidability is not really important for type systems. As long as the type system is sound, you're good. If your compilation is taking too long, I would classify that as a bug.
Thanks for the obvious point that rust isn't agda. However, certainly you can agree that agdas type system is able to capture a strictly greater set of constraints than a typed language without a Turing complete type system
- Drup 10y agoAgda's type system is not turing complete, you can only run on the type-level functions that are proven to be terminating [1] (using well-founded induction or co-induction). Same for Coq, and probably Idris. [1]: http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.Totality http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceMa...
- tathougies 10y agoYou are right about agda. Idris however is not total by default.