Is anyone working on (or interested in) opt-in totality checking for Haskell? I’d love to be able to mark a function or module and have GHC guarantee it never hits bottom: no partial matches, no error/undefined, and no non-termination (perhaps with some notion of productivity for lazy/infinite data?).
It feels like a natural extension of the purity philosophy, treating partiality as an effect to be tracked rather than something always implicitly allowed?
I’ve enjoyed Idris’ totality checking, and I know about Liquid Haskell’s termination checking and Agda’s total-by-default, but I’d love to be able to use it in something more practical for day-to-day programming like Haskell.
I’d love to hear folks’ thoughts on this. Does an extension or plugin dedicated to this sound at all feasible?
Why is liquid haskell not practical? (Note: I’m not making a point, I’m genuinely asking)
Ahh it might well be! I haven’t yet tried reaching for it, as my understanding is that it’s more focused on refinement types and formal verification, and it requires an external SMT solver and supports only one GHC version at a time. I guess I had in mind something lighter and focused just on totality checking? I will take a closer look either way, at the very least to get a better understanding of how intertwined their termination checking is with their approach to refinement types, thanks.
In my understanding, totality checking (and inference) in GHC will unlock a lot of optimization possibilities (especially in conjunction with linear types)
Of course, on obstacle is that we would want totality polymorphism, which probably has gotchas.