optimize Natural/fold in the strict case by winitzki · Pull Request #2585 · dhall-lang/dhall-haskell

winitzki · 2024-05-11T15:52:32Z

The proposed optimization follows the discussion in dhall-lang/dhall-lang#1213 (comment)

The beta-normalization for Natural/fold n t succ zero corresponds to evaluating succ(succ(succ(...(succ(zero))...))) where we apply succ exactly n times.

The current code uses a loop where succ is always evaluated n times.
However, sometimes the loop can be stopped early because the values stop changing.

For example:

let f : Natural → Natural = λ(x : Natural) → if Natural/isZero x then 1 else x
in Natural/fold 10000000 Natural f 5

With this definition, we have f x = x when x is nonzero. The expression evaluates to 5, but the evaluation takes time linear in the first argument (10000000) because the function f will be applied that many times to the value 5 and beta-normalization will be performed each time.

The new code rewrites strictLoop via strictLoopShortcut, which stops the loop as soon as f x = x.

This optimization is only applied in the "strict" case (Normalization.hs introduces strict and lazy cases when evaluating Natural/fold.)

There should be no change of behavior after this optimization.
This is because all Dhall functions are pure; if f x = x then the result of evaluating f (f (f x)) is exactly the same as just x.
So, the only effect of the new code is that some Natural/fold expressions will be beta-normalized faster than before.

I'd like to add some tests for the new behavior but I don't know how. The new behavior returns exactly the same normal forms as before, but does it faster when the "shortcut" is detected (when f x = x is detected). I am not a Haskell programmer, so any suggestions will be welcome here.

Another issue is that I am not familiar with the Haskell build systems, and both cabal new-build dhall as well as stack build fail on my machine in this project, with dependency errors that I am unable to fix.

dhall/src/Dhall/Normalize.hs

Co-authored-by: Gabriella Gonzalez <[email protected]>

winitzki · 2024-05-12T15:39:22Z

@Gabriella439 Thank you for the suggestion.

I'm not sure why the build fails for MacOS. I also have trouble building dhall-haskell on my Mac. I opened another PR to see if the project builds with no changes. #2586 And the macOS build fails there too (while all other OSes succeed).

Update - this is fixed now.

winitzki · 2024-05-14T09:12:46Z

@Gabriella439 My changes do not actually seem to work. I built a local executable (stack build dhall) and ran it (stack exec dhall ) but I don't observe any speedup in the test code shown here.

let f : Natural → Natural = λ(x : Natural) → if Natural/isZero x then 1 else x
in Natural/fold 100000000 Natural f 0

takes about 5 seconds but should be instantaneous. Am I doing something wrong?

I changed the Dhall version to 1.42.2 in dhall.cabal, I tried using strict always instead of lazy, and I tried adding Debug.Trace, and I even tried removing the entire App (App (App (App NaturalFold (NaturalLit n0)) t) succ') zero -> do code block, but nothing helped. In fact, I don't seem to be able to change the behavior of dhall in any way through local code changes.

$ stack build dhall
...
Installing executable dhall in /Users/sergei.winitzki/Code/winitzki-dhall-haskell/.stack-work/install/x86_64-osx/5cb58a553262eb646270303a92d2143ba964e30fb089950b829eb0787bd00e99/9.2.8/bin
Registering library for dhall-1.42.2..
$ stack exec dhall repl
Welcome to the Dhall v1.42.2 REPL! Type :help for more information.
⊢ :let f : Natural → Natural = λ(x : Natural) → if Natural/isZero x then 1 else x

f : Natural → Natural

⊢ Natural/fold 100000000 Natural f 0

1

This still takes about 5 seconds.

How could this even work if I compiled dhall with no code for App (App (App (App NaturalFold (NaturalLit n0)) t) succ') zero -> do? I know the code was recompiled because I get messages about recompiling Normalize.hs and a bunch of other files.

Am I editing the wrong place in the source code? I see that some code involving NaturalFold is also present in Eval.hs. What is the difference between Eval.hs and Normalize.hs?

winitzki · 2024-05-14T10:20:43Z

I added some new code to Eval.hs and now the test code executes instantaneously. The shortcut seems to be working.

Why is Natural/fold implemented in two different places and in two different ways?

For Eval.hs I couldn't figure out how to write that code properly. To detect the shortcut, I need to compare two values of type Val a but I don't see how to do that in general. Just for testing, I implemented a specific comparison in case the values are of type VNaturalLit but this is of course not satisfactory.

winitzki · 2024-06-12T08:07:34Z

@Gabriella439 You merged the PR but I still think the work is not finished. See my comment in the code.

winitzki · 2024-06-12T08:08:40Z

dhall/src/Dhall/Eval.hs

-                                in  go zero (fromIntegral n' :: Integer)
+                                go zero (fromIntegral n' :: Integer) where
+                                  go !acc 0 = acc
+                                  go (VNaturalLit x) m =


Here, we detect the shortcut only when the accumulator is a Natural literal. However, we would like to detect the shortcut in all cases. I could not find any way of comparing Val values. What kind of code would need to be written here?

Dhall.Eval.conv is what you want

1.42.2 * [Supports standard version 23.1.0](https://github.com/dhall-lang/dhall-lang/releases/tag/v23.1.0) * [Allow `Natural` and `Integer` literals in binary notation](dhall-lang/dhall-haskell#2540) * Fix macOS build [[#2561](dhall-lang/dhall-haskell#2561)] / [[#2586](dhall-lang/dhall-haskell#2586)] * [`dhall to-directory-tree`: Fix support for empty `Map`s](dhall-lang/dhall-haskell#2609) * [`Dhall.TH`: Improve recompilation checking](dhall-lang/dhall-haskell#2620) * `Dhall.TH` utilities now use `addDependentFile` internally so that GHC will recompile if any Dhall dependencies change * Performance improvements * Optimize `Natural/fold`: [[#2585](dhall-lang/dhall-haskell#2585)] / [[#2596](dhall-lang/dhall-haskell#2596)] * [Improve `Dhall.Map.traverseWithKey` performance](dhall-lang/dhall-haskell#2589) * The fold will now short-circuit if it reaches a fixed point * [#2611](dhall-lang/dhall-haskell#2611) * Fixes and improvements to test suite * [#2593](dhall-lang/dhall-haskell#2593) * Fixes and improvements to haddocks * [#2546](dhall-lang/dhall-haskell#2546) * Fixes and improvements to code formatting * [#2608](dhall-lang/dhall-haskell#2608)

winitzki added 3 commits May 11, 2024 16:56

optimize Natural/fold in the strict case

e36815e

remove tabs

89c54f7

fix syntax in do block

7bbee59

Gabriella439 reviewed May 12, 2024

View reviewed changes

dhall/src/Dhall/Normalize.hs Outdated Show resolved Hide resolved

Update Normalize.hs

9dcac33

Co-authored-by: Gabriella Gonzalez <[email protected]>

winitzki mentioned this pull request May 12, 2024

fixing the MacOS build #2586

Merged

adding wip code to Eval.hs

827fc45

winitzki and others added 4 commits May 14, 2024 15:31

fix code

ed07195

Merge branch 'main' into feature/optimize_natural_fold

9fae7ff

remove dummy change

33efa78

Merge branch 'main' into feature/optimize_natural_fold

be07882

Gabriella439 merged commit aa4cf87 into dhall-lang:main Jun 12, 2024

winitzki commented Jun 12, 2024

View reviewed changes

winitzki mentioned this pull request Jun 12, 2024

implement shortcut for more data types in Natural/fold #2596

Merged

winitzki deleted the feature/optimize_natural_fold branch June 12, 2024 15:41

kukimik mentioned this pull request Mar 19, 2025

Natural -> Hex Builtin dhall-lang/dhall-lang#1336

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

optimize Natural/fold in the strict case#2585

optimize Natural/fold in the strict case#2585
Gabriella439 merged 9 commits intodhall-lang:mainfrom
winitzki:feature/optimize_natural_fold

winitzki commented May 11, 2024 •

edited

Loading

Uh oh!

Uh oh!

winitzki commented May 12, 2024 •

edited

Loading

Uh oh!

winitzki commented May 14, 2024 •

edited

Loading

Uh oh!

winitzki commented May 14, 2024 •

edited

Loading

Uh oh!

winitzki commented Jun 12, 2024

Uh oh!

winitzki Jun 12, 2024

Uh oh!

Gabriella439 Jun 12, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Comments

Conversation

winitzki commented May 11, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

winitzki commented May 12, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

winitzki commented May 14, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

winitzki commented May 14, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

winitzki commented Jun 12, 2024

Uh oh!

winitzki Jun 12, 2024

Choose a reason for hiding this comment

Uh oh!

Gabriella439 Jun 12, 2024

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Comments

winitzki commented May 11, 2024 •

edited

Loading

winitzki commented May 12, 2024 •

edited

Loading

winitzki commented May 14, 2024 •

edited

Loading

winitzki commented May 14, 2024 •

edited

Loading