3 ms·

Non-Turing complete systems can also allow extremely strong constraints to be embedded, while also allowing the type system to be decidable. Remember, while Rus

by krapht 10y ago

Non-Turing complete systems can also allow extremely strong constraints to be embedded, while also allowing the type system to be decidable. Remember, while Rust makes a lot of noise about being safe, it isn't Ada Ravenspark, or ATS, or Idris/Agda.

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 ago
  Agda'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 ago
    You are right about agda. Idris however is not total by default.
Ar-Curunir 10y ago
What do Idris and Agda have to do with safety? They have a GC RUNTIME; Rust leverages the type system to get ergonomic, safe and fast code without a runtime.
- krapht 10y ago
  Program correctness (safety) is way more than just the memory access guarantees Rust gives you.
- pjmlp 10y ago
  Idris does not have one exclusively. Allocations can be removed just like in Rust thanks to uniqueness types: http://docs.idris-lang.org/en/latest/reference/uniqueness-types.html?highlight=memory http://docs.idris-lang.org/en/latest/reference/uniqueness-ty... Also funny that you mention ergonomics, given that improving the current state is one of the main goals of 2017's roadmap.

3 ms·

Non-Turing complete systems can also allow extremely strong constraints to be embedded, while also allowing the type system to be decidable. Remember, while Rus

by krapht 10y ago

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 ago
  Agda'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 ago
    You are right about agda. Idris however is not total by default.
Ar-Curunir 10y ago
What do Idris and Agda have to do with safety? They have a GC RUNTIME; Rust leverages the type system to get ergonomic, safe and fast code without a runtime.
- krapht 10y ago
  Program correctness (safety) is way more than just the memory access guarantees Rust gives you.
- pjmlp 10y ago
  Idris does not have one exclusively. Allocations can be removed just like in Rust thanks to uniqueness types: http://docs.idris-lang.org/en/latest/reference/uniqueness-types.html?highlight=memory http://docs.idris-lang.org/en/latest/reference/uniqueness-ty... Also funny that you mention ergonomics, given that improving the current state is one of the main goals of 2017's roadmap.