Brian Hicks (Sep 16 2021 at 16:10): Brian Hicks (Sep 16 2021 at 16:10):Are there any plans to have the compiler only accept programs that it can guarantee terminate?
For example, Dhall is intentionally not turing-complete and guarantees programs terminate. (they link to https://en.wikipedia.org/wiki/Total_functional_programming to explain this.) Idris does this by default too, although you can turn it off.
I'm thinking about this in context of build scripts (#rbt.) There are a couple situations in build script land where it'd be really helpful to only accept terminating functions or scripts!
Zeljko Nesic (Sep 16 2021 at 17:05):Shouldn't that be a feature of the platform that you are compiling Roc to? Or even better some Type-level wizardry?
Eg, webservers and health monitors do not want to terminate.
Brian Hicks (Sep 16 2021 at 19:01):it turns out you can prove totality for long-running processes, actually! Say you're writing a map function over a stream. If you can prove that it terminates with an empty stream, and a stream with one more than the last thing, you can prove it's total for an infinite stream.
Brian Hicks (Sep 16 2021 at 19:01):I don't know that it'd be a platform feature; I think it'd have to be specified in the types of the language.
Richard Feldman (Sep 17 2021 at 03:19):so I'm pretty interested in trying what Rust does and seeing if there's still a concern
Richard Feldman (Sep 17 2021 at 03:20):Rust isn't total, but the compiler detects and reports a few cases where you definitely have an infinite loop
Richard Feldman (Sep 17 2021 at 03:20):e.g. every branch inside a function results in recursion
Richard Feldman (Sep 17 2021 at 03:20):the reason I know it reports these is that I've accidentally made those mistakes on more than one occasion, and the compiler told me about it before I ran the program :sweat_smile:
Richard Feldman (Sep 17 2021 at 03:21):my concern about having "total mode" is that there will be some functions that won't work with it, and sometimes they'll be in packages you've imported, and you won't necessarily know which ones they are (unless we advertise "total-mode-compatible" as part of the package metadata or something)
Richard Feldman (Sep 17 2021 at 03:32):so there are nontrivial ecosystem implications there, and I'd want to be careful about introducing something like that
Richard Feldman (Sep 17 2021 at 03:34):I believe the ergonomics implications are also potentially pretty serious for the Dhall approach as compared to the Idris approach; as I understand it, Idris can tell at compile time when a termination condition is "making progress" towards terminating on each recursive call, but Dhall can't and so it just disallows unbounded recursion and makes (for example) recursive sum types impossible to use directly
Brian Hicks (Sep 17 2021 at 11:37):Makes sense, thanks! It’s true that Idris can make much more progress here. I wonder if it’s something in dependent types that enables it or if it’s just that Edwin Brady is a Very Clever Human (or at least a Human Who Applies Implements Important Type Theory Papers)
Folkert de Vries (Sep 17 2021 at 15:00):types help. Say you calculate the factorial factorial n: in idris, the n is a natural number (at compile time anyway, at runtime it's just an i64) and so you can do inductive reasoning. You could do this in roc too of course, but without compiler support it's verbose and slow.
Brian Hicks (Sep 17 2021 at 15:21):hah, right? I wouldn't want to have to actually use peano numbers at runtime :dizzy:
Last updated: Jul 06 2025 at 12:14 UTC