[GHC] #9207: Detect obvious cases of infinite recursion.
#9207: Detect obvious cases of infinite recursion. --------------------------------------+------------------------------------ Reporter: mrugiero | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Keywords: infinite recursion | Operating System: Architecture: Unknown/Multiple | Unknown/Multiple Difficulty: Unknown | Type of failure: None/Unknown Blocked By: | Test Case: Related Tickets: | Blocking: --------------------------------------+------------------------------------ Pure functions are guaranteed to return the same value if the same arguments are used. Because of that, a compiler could be able to detect infinite recursion in the form of a function calling itself with the same arguments (case, some distracted programmer forgot to apply the function tail to a list). The way I see it, one of Haskell's main selling points is that it helps the programmer to avoid sources of bugs as much as it can, and infinite recursion is one of the few that stand unchecked. I specifically point to this example because both, I'm a newbie and made that newbie mistake, and think it shouldn't be hard to implement to the parsing stage of the compiler/interpreter. It probably should throw an error when this happens in pure functions, and maybe an opt-in warning if it happens in monads. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9207 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9207: Detect obvious cases of infinite recursion. ------------------------------------+-------------------------------------- Reporter: mrugiero | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: infinite recursion Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: None/Unknown | Blocked By: Test Case: | Related Tickets: Blocking: | ------------------------------------+-------------------------------------- Comment (by j80JjBjVNRMajmA): In a lazy language, writing and using infinite recursions is a feature! There is no way, unintentional infinite recursion could be captured by the compiler. Take a look at the perfectly good and useful function `repeat`: {{{ repeat :: a -> [a] repeat x = x : repeat x }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9207#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9207: Detect obvious cases of infinite recursion. ------------------------------------+-------------------------------------- Reporter: mrugiero | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: infinite recursion Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: None/Unknown | Blocked By: Test Case: | Related Tickets: Blocking: | ------------------------------------+-------------------------------------- Comment (by mrugiero): Can you put an example of use of that function? Because I don't really see right now (and as I said, I'm just learning the language) creating an infinite list is good or useful. It just sounds like a blown up stack to me, whenever the list actually gets created. I guess this moment will be, thankfully, whenever a tail recursion starts using the generated values, am I right? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9207#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9207: Detect obvious cases of infinite recursion. ------------------------------------+-------------------------------------- Reporter: mrugiero | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: infinite recursion Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: None/Unknown | Blocked By: Test Case: | Related Tickets: Blocking: | ------------------------------------+-------------------------------------- Comment (by j80JjBjVNRMajmA): You will get used to infinite lists in Haskell. Do you know this one `[1..]`? `repeat` is defined in Data.List (http://www.haskell.org/ghc/docs/latest/html/libraries/base/Data- List.html) and also used there to define `replicate`. One importat use case is to define the `ZipList` Applicative instance: {{{ pure = ZipList . repeat }}} in https://hackage.haskell.org/package/base-4.7.0.0/docs/Control- Applicative.html#t:ZipList. It is hard to motivate all the greatness the Haskell-way brings in a Bug- comment. Another note on topic: Merely checking, that the recursive function call has different arguments does not protect you from infinite recusion: {{{ f x = f $ x + 1 }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9207#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9207: Detect obvious cases of infinite recursion. ------------------------------------+-------------------------------------- Reporter: mrugiero | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: infinite recursion Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: None/Unknown | Blocked By: Test Case: | Related Tickets: Blocking: | ------------------------------------+-------------------------------------- Comment (by mrugiero): I'll look into those in a minute (I'm trying to finish another chapter of real world Haskell right now :) ), but in the meantime I want to clarify on your last comment that it's exactly why I put the "obvious" part in the title of the FR. When it's the same function calling itself with the same arguments it's really obvious, as long as it's pure, that it will end up in infinite recursion. I left implicit that non-obvious causes of infinite recursion wouldn't be intercepted by this. I didn't mention those because those would be harder for the compiler to catch, and the harder it gets the more it becomes proper of a static analysis tool to avoid wasting time at every compilation cycle. The obvious ones are the one that might belong to the compiler. But if you say it's part of the power of the language, I guess you must be right, I hope I'll understand why soon :) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9207#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9207: Detect obvious cases of infinite recursion. ------------------------------------+-------------------------------------- Reporter: mrugiero | Owner: Type: feature request | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: invalid | Keywords: infinite recursion Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: None/Unknown | Blocked By: Test Case: | Related Tickets: Blocking: | ------------------------------------+-------------------------------------- Changes (by Fuuzetsu): * status: new => closed * resolution: => invalid Comment: As pointed out, there are no ‘obvious’ cases of infinite recursion that the programmer doesn't actually want that GHC could catch, at least not in the way you stated. I'll close the ticket. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9207#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9207: Detect obvious cases of infinite recursion. ------------------------------------+-------------------------------------- Reporter: mrugiero | Owner: Type: feature request | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: invalid | Keywords: infinite recursion Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: None/Unknown | Blocked By: Test Case: | Related Tickets: Blocking: | ------------------------------------+-------------------------------------- Comment (by altaic): I don't think, in principal, this is a bad idea, but it is part of a very challenging problem: static complexity (time and space) analysis. There are quite a few papers on the topic, which I can post here if there's interest. In general it is undecidable, but there are many situations where it is not. I plan on opening a ticket for just that when I form a sensible plan of attack (though it might be awhile, since I'm currently focusing on more pragmatic issues). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9207#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9207: Detect obvious cases of infinite recursion. ------------------------------------+-------------------------------------- Reporter: mrugiero | Owner: Type: feature request | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: invalid | Keywords: infinite recursion Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: None/Unknown | Blocked By: Test Case: | Related Tickets: Blocking: | ------------------------------------+-------------------------------------- Comment (by mrugiero): Those papers certainly sound interesting. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9207#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9207: Detect obvious cases of infinite recursion. ------------------------------------+-------------------------------------- Reporter: mrugiero | Owner: Type: feature request | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: invalid | Keywords: infinite recursion Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: None/Unknown | Blocked By: Test Case: | Related Tickets: Blocking: | ------------------------------------+-------------------------------------- Comment (by rwbarton): Some version of strictness analysis could catch typos like `let y = y + 1 in ...` (oops, meant `let y = x + 1 in ...`), right? (Assuming `y` is inferred to have a concrete type like `Int` where `(+)` is known to be strict.) Those can be annoying to track down at runtime. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9207#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9207: Detect obvious cases of infinite recursion.
------------------------------------+--------------------------------------
Reporter: mrugiero | Owner:
Type: feature request | Status: closed
Priority: normal | Milestone:
Component: Compiler | Version: 7.8.2
Resolution: invalid | Keywords: infinite recursion
Operating System: | Architecture: Unknown/Multiple
Unknown/Multiple | Difficulty: Unknown
Type of failure: None/Unknown | Blocked By:
Test Case: | Related Tickets:
Blocking: |
------------------------------------+--------------------------------------
Comment (by simonpj):
GHC already does a guaranteed-divergence analysis. For example
{{{
f [] = f [True]
f (x:xs) = f xs
}}}
If you say
{{{
ghc -c -O -ddump-simpl Foo.hs
}}}
you get something like this
{{{
Foo.f [Occ=LoopBreaker] :: forall t_aK7. [GHC.Types.Bool] -> t_aK7
[GblId, Arity=1, Str=DmdType
#9207: Detect obvious cases of infinite recursion. ------------------------------------+-------------------------------------- Reporter: mrugiero | Owner: Type: feature request | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: invalid | Keywords: infinite recursion Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: None/Unknown | Blocked By: Test Case: | Related Tickets: Blocking: | ------------------------------------+-------------------------------------- Comment (by altaic): Replying to [comment:7 mrugiero]:
Those papers certainly sound interesting.
Whoops, missed your comment, sorry! Here are the papers I have that are related to static complexity analysis, in no particular order: * Elvira Albert, Puri Arenas, Samir Genaim, Germán Puebla. ''Cost Relation Systems: A Language-Independent Target Language for Cost Analysis'' * Nao Hirokawa. ''Automated Complexity Analysis Based on the Dependency Pair Method'' * Jan Hoffmann and Zhong Shao. ''Type-Based Amortized Resource Analysis with Integers and Arrays'' * Jan Hoffmann and Martin Hofmann. ''Amortized Resource Analysis with Polymorphic Recursion and Partial Big-Step Operational Semantics'' * Jan Hoffmann and Martin Hofmann. ''Amortized Resource Analysis with Polynomial Potential: A Static Inference of Polynomial Bounds for Functional Programs (Extended Version)'' * Jennifer Paykin. ''Automated Cost Analysis of a Higher-Order Language in Coq'' * Lars Noschinski, Fabian Emmes, and Jürgen Giesl. ''A Dependency Pair Framework for Innermost Complexity Analysis of Term Rewrite Systems'' * Sumit Gulwani. ''SPEED: Symbolic Complexity Bound Analysis'' * Edward Z. Yang, David Mazières. ''Resource Limits for Haskell'' * Jan Hoffmann, Klaus Aehlig, and Martin Hofmann. ''Resource Aware ML'' * Jan Hoffmann, Klaus Aehlig, and Martin Hofmann. ''Multivariate Amortized Resource Analysis'' * Jan Hoffmann. ''Types with Potential: Polynomial Resource Bounds via Automatic Amortized Analysis'' * Martin Avanzini, Georg Moser, and Andreas Schnabl. ''Automated Implicit Computational Complexity Analysis (System Description)'' * Aart Middeldorp, Georg Moser, Friedrich Neurauter, Johannes Waldmann, and Harald Zankl. ''Joint Spectral Radius Theory for Automated Complexity Analysis of Rewrite Systems'' * Chris Okasaki. ''Purely Functional Data Structures'' * Alessandra Di Pierro and Herbert Wiklicky. ''Probabilistic Analysis of Programs: A Weak Limit Approach'' * R. M. Amadio, N. Ayache, F. Bobot, J. P. Boender, B. Campbell, I. Garnier, A. Madet, J. McKinna, D. P. Mulligan, M. Piccolo, R. Pollack, Y. R ́egis-Gianas, C. Sacerdoti Coen, I. Stark, and P. Tranquilli. ''Certified Complexity (CerCo)'' * M. Brockschmidt, F. Emmes, S. Falke, C. Fuhs, and J. Giesl. ''Alternating Runtime and Size Complexity Analysis of Integer Programs'' * Wolf Zimmermann. ''Automatic Worst Case Complexity Analysis of Parallel Programs'' * Jean-Pierre Jouannaud and Weiwen Xu. ''Automatic Complexity Analysis for Programs Extracted from Coq Proof'' * Sébastian Pop. ''Analysis of induction variables using chains of recurrences: extensions'' * François Pottier. ''Types for complexity-checking'' (presentation) * Michael Kruse. ''Perfrewrite: Memory and Time Complexity Analysis via Source Code Instrumentation'' * Flemming Nielson, Hanne Riis Nielson, and Helmut Seidl. ''Automatic Complexity Analysis'' -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9207#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9207: Detect obvious cases of infinite recursion. -------------------------------------+------------------------------------- Reporter: mrugiero | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.4.4 Resolution: | Keywords: infinite | recursion Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bebarker): * status: closed => new * version: 7.8.2 => 8.4.4 * resolution: invalid => Comment: I respectfully disagree with Fuuzetsu's suggestion that there are no obvious cases, here is an example that came up for me recently. I'm somewhat new to Haskell but am also fairly familiar with writing recursive functions in other languages. Probably, this was difficult for me to spot because I wrote it: {{{#!haskell loadImage :: MonadIO m => FilePath -> m HicoImage loadImage fpath = liftIO $ loadImage fpath where loadImg :: FilePath -> IO HicoImage loadImg fp = Image <$> SDL.Image.load fp }}} Now, there are several issues with this function stylistically that probably would have prevented this, such as not really needing the `where` clause and choosing bad naming conventions (`loadImage` and `loadImg`). The good news is for folks who know more about GHC than myself, I think, is this snippet I found in [https://www.reddit.com/r/haskell/comments/6hng6n/which_haskell_features_prev... another discussion] regarding detecting "syntactic cycles" with GHC. To quote: Core differentiates between a single [https://downloads.haskell.org/~ghc/8.4.4/docs/html/libraries/ghc-8.4.4/CoreS... NonRec] binding at a time vs. a [https://downloads.haskell.org/~ghc/8.4.4/docs/html/libraries/ghc-8.4.4/CoreS... Rec] binding group. The part of GHC which does the conversion from a single, recursive group to these let nestings is called the Occurence Analyzer. It's basically a strongly connected component analysis, once you have figured out all edges. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9207#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9207: Detect obvious cases of infinite recursion. -------------------------------------+------------------------------------- Reporter: mrugiero | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.4.4 Resolution: | Keywords: infinite | recursion 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 svenpanne): OK, let's forget about the warning caused by not using `loadImg` for a moment. Why should a compiler warn about the body of `loadImage`? I seriously hope that it doesn't warn, because `liftIO` is a method of the `MonadIO` type class, so the compiler has no knowledge whatsoever about it, apart from its type. So passing `loadImage fpath` to it might actually make sense, see the `repeat` example above. If you are lucky and the compiler uses enough optimizations, you might get a warning at `loadImage`'s use sites, because then it might see enough context, but the function alone is perfectly OK from a compiler's point of view. In a lazy language, it's quite hard to distinguish between "wanted infinite recursion" and "unwanted infinite recursion". -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9207#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC