search

idris-lang / Idris-dev

A Dependently Typed Functional Programming Language
http://idris-lang.org
Other
3.43k stars 644 forks source link

'nicest' function in contrib/Text/PrettyPrint/Core.idr is not lazy #4048

Closed hejfelix closed 6 years ago

hejfelix commented 7 years ago

@jfdm

I'm trying to understand sources of complexity in the PrettyPrint module, and reading Wadler's article. On page 10 he states that lazy evaluation of bests "inner computation" is essential for efficiency.

I am unsure whether this can cause performance problems here: https://github.com/idris-lang/Idris-dev/blob/ec294a15690ead749f7ac77b2fc62adb366b6b84/libs/contrib/Text/PrettyPrint/WL/Core.idr#L162-L169

In my playing around with the library, I do see big performance dips on larger expressions that I cannot explain otherwise.

As an example, this expression doesn't terminate within any tolerable time:

:exec toString 0 15 $ fold (|//|) $ map text $ words "this is a long sentence with a lot of words that I can use for testing the performance of the prettier printer implementation. I need a few more words to prove my point, though."

The resulting doc from the fold is listed here: https://pastebin.com/4AJWcGnD

ahmadsalim commented 7 years ago

Thanks for reporting the issue

david-christiansen commented 7 years ago

Ken Friis Larsen has a strict version of the algorithm in SML at https://github.com/kfl/wpp .

hejfelix commented 7 years ago

Now we're talking. Thanks! While I want this to be fixed, right now I need something that works 😀

hejfelix commented 7 years ago

Oh, I thought it was in idris :/

david-christiansen commented 7 years ago

We have a Haskell library that looks astonishingly similar to Ken's that could potentially be ported to Idris: http://davidchristiansen.dk/drafts/final-pretty-printer-draft.pdf

No idea how to make it pass the totality checker, though. Perhaps it just will...

/David

jfdm commented 6 years ago

Sorry, for delayed response. My port of Wadler-Leijens pretty print was a port of Shayam's version, and is not a strict version. It is total though... The lack of laziness could be addressed using the Lazy annotation, or changing the core algorithm to be strict. I don't have time to really address this, but PRs are welcome, and I am happy to guide people through the process.

jfdm commented 6 years ago

oh, i've fixed this, awaiting tests to finish running

hejfelix commented 6 years ago

Man, so cool, thanks -- how would I understand which version of Idris would include this fix?

jfdm commented 6 years ago

@hejfelix Currently the 'fix' is in the development version of Idris. Once a new release has been made, then you can get the library with the fix. Alternatively, you can check out the development version of idris and install contents of libs/using the version of idris you have installed.