37

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.

Chris Martin
  • 30,334
  • 10
  • 78
  • 137
Alec
  • 31,829
  • 7
  • 67
  • 114
  • “since `:~:` has exactly one inhabitant (`Refl`), GHC could optimize `gcastWith commutativity e ⇒ e`” – first, I reckon GHC does already do that in some cases (if it specialises to concrete `n` and `m`)? — In general though, I doubt this kind of totality analysis would really help much performance-wise, since the power of dependently-typed proofs is really their constructive nature, and the work in constructing equalities etc. can't in general be _O_(1) at runtime. – leftaroundabout Feb 10 '17 at 09:07
  • @leftaroundabout I buy that GHC can make optimizations for concrete `n` and `m`, but that seems a bit of a brittle mechanism. I reckon most of my (current) use cases for proofs would be O(1) optimizable... Do you have an example of a dependently-typed proof that can't in general be O(1)? I don't doubt they exist - I'd just like an example to think about. Thanks! – Alec Feb 10 '17 at 09:17
  • 3
    @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 Feb 10 '17 at 09:17
  • 17
    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 *co*induction. 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 Feb 10 '17 at 09:37
  • 2
    @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 Feb 10 '17 at 09:55
  • @Alec A proof for `Either (n :~: m) ((n :~: m) -> Void)` (for Peano naturals `n,m`) can not be O(1), I think. At runtime we need to check whether the runtime values are equal or not. For single-value types, it should be always O(1) I guess. – chi Feb 10 '17 at 09:59
  • @chi Sure! I was only thinking about single-value types like `:~:` or `()`. Otherwise, I agree all bets are off (I reckon something could be worked out with refinement types here, but that is a bit out of scope and nowhere in sight of GHC). – Alec Feb 10 '17 at 10:14
  • 1
    Since `:~:` is a boxed type, it has 2 inhabitants: `Refl` and `_|_`. – Heimdell Feb 13 '17 at 05:52
  • @Heimdell That's the point of this question - if the function producing the `:~:` is total, it cannot be `_|_`. – Alec Feb 13 '17 at 17:47
  • 1
    @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 Feb 26 '17 at 14:03

1 Answers1

20

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.

Community
  • 1
  • 1
Christopher Done
  • 5,886
  • 4
  • 35
  • 38
  • 3
    What sort of limitations are there to this being part of GHC? AFAICT, LH is just a sort of advanced linter - it won't optimize away total values of types with only one inhabitant. Thanks! – Alec Feb 10 '17 at 17:26
  • 2
    @Alec Section 8.4 of Richard A. Eisenberg's thesis https://arxiv.org/abs/1610.07978 has some suggestions on how something like Liquid Haskell might be incorporated in a future dependently-typed Haskell. – danidiaz Feb 10 '17 at 18:36
  • 3
    @danidiaz Funny you bring this up: that section was actually one of the reasons I asked this question. I'm trying to scope out what exactly is the work that would go into such a GHC plugin. I was hoping more for a discussion on the details of data/codata (and the nasty in-between stuff)... – Alec Feb 10 '17 at 18:41