3 ms·

> In general, I think non-Turing complete (always terminating) languages are super useful and should be used more often. yup, always-terminating functions are

> In general, I think non-Turing complete (always terminating) languages are super useful and should be used more often. yup, always-terminating functions are also called total functions (if they're defined for every input). Which is a related concept to Total functional programming http://docs.idris-lang.org/en/latest/tutorial/theorems.html#totality-checking http://docs.idris-lang.org/en/latest/tutorial/theorems.html#... While Idris is turing complete for example, it's possible to mark functions and whole modules as total, and let the compiler prove it for you. Wish that more people knew that we have such tools available nowadays

dualogy 10y ago
Nice one, I wish there was a Haskell extension for that! (Can't risk switching existing/pending code-bases over to Idris just for that feature though)
- a-saleh 10y ago
  I remember reading about two projects og Gabriel Gonzales that might be interesting in this regard. Dhall, a total configuration language. https://github.com/Gabriel439/Haskell-Dhall-Library https://github.com/Gabriel439/Haskell-Dhall-Library There is Morte and Anna as well, that look like the previous experiments in total languages in haskell. https://github.com/Gabriel439/Haskell-Annah-Library https://github.com/Gabriel439/Haskell-Annah-Library