What is Haskell missing for totality checking?

37
votes

A total (functional) language is one in which everything can be shown to terminate. Obviously, there are lots of places where I don't want this - throwing exceptions is sometimes handy, a web-server isn't supposed to terminate, etc. But sometimes, I would like a local totality check to enable certain optimizations. For example, if I have a provably-total function

commutativity :: forall (n :: Nat) (m :: Nat). n + m :~: m + n
commutativity = ...

then, since :~: has exactly one inhabitant (Refl), GHC could optimize

gcastWith (commutativity @n @m) someExpression
  ==>
someExpression

And my proof of commutativity goes from having an O(n) runtime cost to being free. So, now for my question:

What are some of the subtle difficulties in making a totality checker for Haskell?

Obviously, such a checker is conservative so whenever GHC isn't sure something is total (or is to lazy to check) it could assume it isn't... Seems to me it might not be too difficult to cobble together a not-so-smart checker that would still be very useful (at least it should be straightforward to eliminate all my arithmetic proofs). Yet, I can't seem to find any efforts to build such a thing into GHC, so obviously I'm missing some pretty big constraints. Go ahead SO, crush my dreams. :)

Relevant but not recent: Unfailing Haskell by Neil Mitchell, 2005.

1
haskelltypesghcproofdependent-type
@leftaroundabout: Re. constructivity: not quite; you're confusing "constructive proof" and "computational content". Since a :~: b only has one non-⊥ inhabitant, if we were in a total setting, we could say that proofs of a :~: b had no computational content; we know that castWith :: (a :~: b) -> a -> b must be computationally equivalent to const id (given totality). In a homotopy type theory setting, it's true that equalities have computational content, so you'd have to do the work – but in that setting, refl isn't the only inhabitant of a = b! – Antal Spector-Zabusky
A web server isn't supposed to terminate. Moreover, it's supposed to respond, and that (a.k.a. "productivity") is the form of totality that pertains to coinduction. The you-can't-write-a-total-server myth is one of the poorer excuses for retaining general recursion. I agree that a checkably total fragment of Haskell would be valuable (I once called it "Ask", because you can, with confidence, and because it's the part of Haskell that isn't "Hell"). The proof erasure motivation (cf Coq's Extraction) is good. Distinguishing data from codata (tricky in Haskell) would be a big help. – pigworker
@leftaroundabout As Antal mentions above, one can build optimized O(1) proofs for single-nonbottom-value types, like a:~:b. Everytime one has e :: a:~:b and a termination checker ensures e is non bottom, once can optimize it with unsafeCoerce Refl. The tricky part is proving totality on Haskell codata, where induction is not enough. Maybe we could restrict this to "data"-only types/kinds, like e.g. data Nat = O | S !Nat, where induction could be sound. I am not terribly confident about this, though. – chi
Since :~: is a boxed type, it has 2 inhabitants: Refl and _|_. – Heimdell
@Alec if you wan something in haskell to be total, it should be unboxed. And ypu will get problems with the unboxed things, since they are of different kind from boxed ones. – Heimdell

1 Answers

20
votes

Liquid Haskell has totality checking: https://github.com/ucsd-progsys/liquidhaskell#termination-check

Screenshot from homepage

By default a termination check is performed on all recursive functions.

Use the no-termination option to disable the check

liquid --no-termination test.hs

In recursive functions the first algebraic or integer argument should be decreasing.

The default decreasing measure for lists is length and Integers its value.

(I included screenshot and quote for posterity.)

Similar to in Agda or other languages with totality checking, the arguments to the function must become structurally smaller over time to reach the base case. Combined with a totality checker, this makes for a reliable check for a number of functions. LH also supports helping the checker along by indicating how things decrease, which you could do with an abstract data type that's opaque or from an FFI. It's really quite practical.