#14592: Totality checking -------------------------------------+------------------------------------- Reporter: varosi | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): See [https://ucsd-progsys.github.io/liquidhaskell-blog/ Liquid Haskell] which includes a pretty good totality checker. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14592#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14592: Totality checking -------------------------------------+------------------------------------- Reporter: varosi | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): There's a downside to totality checking: it means that the language needs to be simple enough to support it. GHC has several features making totality checking hard: * `Type :: Type` (whereas Idris has `Type :: Type 1`, `Type 1 :: Type 2`, etc.) * The `Type.Reflection` library (a.k.a. `Typeable`). Section 7 of the recent [https://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1002&context=compsci_pubs paper] shows how `Typeable` can lead to non-termination without recursion. * Non-strictly-positive datatypes (sorry, I don't know how Idris handles these, nor do I have a good reference for more information) * Pattern synonyms (should we trust `COMPLETE` pragmas here?) * Probably more... I agree that having a totality checker would be wonderful. But writing one with GHC's current feature set is a major research undertaking, and then maintaining it might force GHC to slow down its innovation in other areas. This isn't really an argument against it, but I just wanted to highlight that there are major tradeoffs here. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14592#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14592: Totality checking -------------------------------------+------------------------------------- Reporter: varosi | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): I agree with your first sentence -- it is of a similar impact to more types. The problem is that Haskell's type system is so flexible at the moment that I'm not sure we could prove any function that contains a function call as terminating. (Kind polymorphism and `Type :: Type` both introduce ways of writing very sneakily non-terminating functions.) So, essentially, I agree with you: we can verify totality only for certain functions, but those functions are (currently) very trivial: just case matches and returned constants. To expand this set would take ground- breaking research. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14592#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler