ucsd-progsys / liquidhaskell

Liquid Types For Haskell
BSD 3-Clause "New" or "Revised" License
1.18k stars 134 forks source link

performance problem with deeply nested lists #393

Open hasufell opened 9 years ago

hasufell commented 9 years ago

Given the following funny fizzbuzz version liquidhaskell consumes up a lot of memory (I have 16GB) and I have to kill it out of precaution. I could nail it down to the line with [[[[[[[[[[[[["FizzBuzz"]]]]]]]]]]]]].

But I guess this is not really a common use case anyway. But it's still interesting.

import Control.Monad

main =
  sequence_ $ fmap fmap' [1..300]
  where
    essence = (2309213093109 `friday` 66) - 18
    suchFunctional :: Eq what => what -> what -> Bool
    suchFunctional = (==)
    friday = fst (mod, "whatever")
    monday = head . tail . tail . tail $ [2..3892398]
    cat = sum . concat $ [[]]
    {- doorway = print -}
    nirvana = [[[[[[[[[[[[["FizzBuzz"]]]]]]]]]]]]]
    hooray = ("Fizz", ",", "where to go from here?", "zzuB")
    fmap' maybeTrue
      | flip friday essence maybeTrue `suchFunctional` (cat) &&
          friday maybeTrue monday == cat = print (concat
      . concat
      . concat
      . concat
      . join
            . join . concat
        . concat . join . join
        . concat
        . concat . concat $ nirvana)
      | (flip . flip) friday  maybeTrue essence `suchFunctional`
        cat                   = print
          $ (\(darkKnight, _, _, muh) -> darkKnight) hooray
      | maybeTrue `friday` monday `suchFunctional` cat
            = print $ (\(can, this, be, true) -> reverse true) hooray
      | otherwise                        = print maybeTrue
ranjitjhala commented 9 years ago

Hmm interesting! Thanks for pointing out we'll take a look!

On May 14, 2015, at 4:33 PM, Julian Ospald notifications@github.com wrote:

Given the following funny fizzbuzz version liquidhaskell consumes up a lot of memory (I have 16GB) and I have to kill it out of precaution. I could nail it down to the line with [[[[[[[[[[[[["FizzBuzz"]]]]]]]]]]]]].

But I guess this is not really a common use case anyway. But it's still interesting.

import Control.Monad

main = sequence $ fmap fmap' [1..300] where essence = (2309213093109 friday 66) - 18 suchFunctional :: Eq what => what -> what -> Bool suchFunctional = (==) friday = fst (mod, "whatever") monday = head . tail . tail . tail $ [2..3892398] cat = sum . concat $ [[]] {- doorway = print -} nirvana = [[[[[[[[[[[[["FizzBuzz"]]]]]]]]]]]]] hooray = ("Fizz", ",", "where to go from here?", "zzuB") fmap' maybeTrue | flip friday essence maybeTrue suchFunctional (cat) && friday maybeTrue monday == cat = print (concat . concat . concat . concat . join . join . concat . concat . join . join . concat . concat . concat $ nirvana) | (flip . flip) friday maybeTrue essence suchFunctional cat = print $ ((darkKnight, , _, muh) -> darkKnight) hooray | maybeTrue friday monday suchFunctional cat = print $ ((can, this, be, true) -> reverse true) hooray | otherwise = print maybeTrue — Reply to this email directly or view it on GitHub.

nikivazou commented 9 years ago

Well, this is not super surprising since [[[[[[[[[[[[["FizzBuzz"]]]]]]]]]]]]] is desugared to a huge expression in GHC's core. If you run liquid with the verbose flag (liquid -v Foo.hs) and search for CoreBinds you can see the (huge) generated internal code that liquidHaskell type checks.

For now, you can have all these constants in another file (that you will not check) and import them?

But we should take these cases into account and provide a "do-not-check-this-expression" flag. We already have an assert keyword in that assert nirvana :: t means that liquidHaskell trusts that nirvana has type t but still liquidHaskell will check that the implementation of nirvana does not violate any types. Thus, I do not think that assert will solve your problem. We should provide another keyword that totally ignores the implementation of nirvana.