Add a new environment machine normalizer #876

AndrasKovacs · 2019-03-31T18:11:06Z

See this post on discourse for motivation and background for this PR.

Dhall.Eval: new evaluator, conversion checker and normalizer. Standalone alpha normalizer is not yet available here.
There is a new option "new-normalize" for the dhall executable, which uses
the new normalizer.
Type checker and the rest of the Dhall codebase remains unchanged.
There are some benchmarking notes in dhall/benchmark/examples/new-normalize. There should be more benchmarks.

AndrasKovacs · 2019-04-01T06:26:08Z

Old GHCs trip up on Strict pragma. Should I just remove it?

jneira · 2019-04-08T08:35:35Z

@AndrasKovacs First of all congrats for this awesome improvement to dhall-haskell
I suppose @Gabriel439 is already aware of it but i've requested his review (sorry if i am bothering).
Imo the final change should be applied directly for default normalization, after the appropiate tests and benchmarks.

Re Strict: I am afraid that remove the pragma would need a important change in the modules cause you should add explicit strict annotations everywhere (following the semantics of the pragma: https://gitlab.haskell.org/ghc/ghc/wikis/strict-pragma#strict)

AndrasKovacs · 2019-04-08T09:33:38Z

@jneira adding strictness annotations is no big deal. On the other hand, adapting the codebase to the new normalizer is a substantial change, and ideally I'd like to defer that work to a new branch on dhall-haskell.

Gabriella439 · 2019-04-09T00:33:44Z

@AndrasKovacs: Sorry for the delay; I was a bit sick recently.

The reason CI builds against GHC 7.10.3 is to support Etlas (the package manager for Eta). Eta/Etlas are built with GHC 7.10.3 and Etlas depends on Dhall (since Dhall is an officially supported configuration format for configuring Etlas packages). So we have to figure out some way to merge this will supporting GHC 7.10.3.

I can think of two main solutions:

Configure the dhall package to only enable the new module for newer GHC versions
Disable Strict for now if the performance loss isn't too large

My weak preference is for the latter solution, since it seems like the other changes in this pull request are responsible for the large performance gains.

Gabriella439 · 2019-04-09T00:36:55Z

@AndrasKovacs: Instead of adding a new-normalize subcommand, would it be possible to always the new normalization algorithm for the command-line interpreter? My understanding is that the only reason we might need to preserve the old normalization code at this point is to support custom normalization, but we don't take advantage of custom normalization when using the command line executable.

I was actually going to suggest going a step further and replacing Dhall.Core.normalize with your faster algorithm, but leaving Dhall.Core.normalizeWith to use the old customizable normalization algorithm.

AndrasKovacs · 2019-04-09T09:09:18Z

Thanks for the feedback!

I'll remove the Strict pragma (and conform to GHC 7.10 if there's some other issue, e.g. I think I used newer-style pattern synonyms as well), and I'll look into replacing Dhall.core.normalize.

If that works, it's OK for now, but that's still overall very inefficient with the current typechecker and import resolver. I plan to switch them as well to the standard NbE algorithm, and I think I can do this sometime in the next 2 weeks.

Gabriella439 · 2019-04-10T05:04:58Z

@AndrasKovacs: Yeah, I'm fine merging this even with just the improvement to normalization performance. From my point of view the main reason to merge this is to reduce your maintenance burden since once you merge this into master we can ensure that it stays up to date

- Dhall.Eval: new evaluator, conversion checker and normalizer. There is no standalone alpha normalizer yet. - There is a new option "new-normalize" for dhall executable, which uses the new normalizer. - Type checker is unchanged.

- new implementation: alphaNormalize, judgmentallyEqual, normalize - normalizeWith takes a Maybe ReifiedNormalizer argument now, and switches to the new evaluator whenever the input normalizer is Nothing - QuickCheck test for isNormalized removed, because we don't support evaluation of ill-typed terms, which the test would require.

AndrasKovacs · 2019-04-12T17:57:51Z

Updates:

Branch now compiles with GHC 7.10
In Dhall.Core, normalize, judgmentallyEqual and alphaNormalize have new implementations.
normalizeWith takes Maybe ReifiedNormalizer as input (instead of a function), to make it possible to switch between new and old normalizers, depending on whether the custom normalizer parameter is a no-op.
Removed new-normalize command and the separate tests for the new normalizer which I previously added.
Added a new standalone alphaNormalize implementation, which behaves like the old one, in order to let TypeCheck and Import function without notable changes for now.
Removed isNormalized test from the QuickCheck part of tests. The issue is that my evaluator assumes well-typed expressions, and throws "impossible" errors otherwise, and the Arbitrary instance generates ill-typed terms. I think failing loudly on ill-typed terms is highly useful and important.

I also tested Vanessa McHale's big file, and we only have about 25% checking time reduction on that so far. Small computation-heavy examples seem to get far greater speedups. So I believe currently the practically most relevant overheads are in type checking and imports.

jneira · 2019-04-12T20:21:17Z

wow appveyor has reached the 1 hour limit build 😟

f-f · 2019-04-12T20:42:00Z

@jneira we should probably enable the cache on failed builds too, with APPVEYOR_SAVE_CACHE_ON_ERROR: true (see docs here)

jneira · 2019-04-14T15:46:58Z

@f-f maybe it could improve times in case of failed builds but i think the build times has increased since we are using ghc-8.6.4.
I am testing build times with lts-13 and lts-12, if it is the cause we could use lts-12 for now

dhall/src/Dhall/Eval.hs

Gabriella439 · 2019-04-14T14:31:04Z

dhall/src/Dhall/Eval.hs

+    (VIntegerToDouble t , VIntegerToDouble t') -> convE t t'
+
+    (VDouble       , VDouble)        -> True
+    (VDoubleLit n  , VDoubleLit n')  -> n == n'


The standard requires slightly different behavior for equality of Double literals. They are equal if their CBOR representation is equal. This is actually the case for all Dhall expressions (not just Doubles), but Double literals happen to beone of the few cases where ordinary equality doesn't give the same behavior as CBOR equality.

OK. I think now I should just export a doubleToTerm :: Double -> Term function from Dhall.Binary, and use that (I don't want to use encode because of the unnecessary ToTerm constraint on conv; also, the next iteration of conv will likely not have any class constraints, because it'll have access to Val-s of imported expressions).

Another way to do this without a ToTerm constraint is to wrap the Double value in a DoubleLit constructor and then Dhall.Binary.encode that

Right, I realize now I just have to specify a suitable Expr s a type for the DoubleLit.

I pushed a commit, I used encode as you suggested.

dhall/src/Dhall/Eval.hs

dhall/dhall.cabal

dhall/src/Dhall/Eval.hs

Gabriella439 · 2019-04-14T16:29:34Z

dhall/src/Dhall/Eval.hs

+    Merge x y ma     -> case (evalE x, evalE y, evalE <$> ma) of
+                          (VRecordLit m, VUnionLit k v _, _)
+                            | Just f <- Dhall.Map.lookup k m -> f `vApp` v
+                            | otherwise -> error "eval: impossible"


Instead of returning error, would it be possible to return the fallback case (i.e. VMerge x y ma)? Then the property test in Dhall.Test.QuickCheck could be re-enabled

Same comment for other uses of error

I prefer not being silent about type errors in evaluation. This is an important point for detecting obscure bugs in type checking. Also, once we compute past an ill-typed expression, totality of evaluation and soundness of conversion checking fail to hold.

BTW, I see now that Import.Types has an InternalError exception. Should I use that instead of these ad-hoc "impossible" errors? In this case I do intend to signal internal error, and not something like an obviously impossible branch. In Agda though, these are also called "impossible" errors.

Yeah, you can use the Dhall.Core.internalError function for this purpose. It provides a standard template for users to report implementation errors

However, I like error because it gives me line numbers, while throw InternalError doesn't. Is there a way to get line numbers with thrown exceptions?

Or just use error with a nicer message...

I used error with nicer message in new commit.

See at: dhall-lang#876 (review)

ocharles · 2019-04-15T17:03:05Z

I was curious to see how this performed with one project that is currently unusable with Dhall's current performance - replacing Nix with Dhall. The issue is at dhallix/nix-derivation#8. I updated the gcc branch to gcc-latest-dhall, but unfortunately we're still looking at 1m 47s to call dhall <<< ./gcc.dhall. Still, this is considerably better than master which currently takes 3m 30s.

AndrasKovacs · 2019-04-15T22:22:24Z

@ocharles: that's a very good benchmark, I'll keep it in mind. I did not expect dramatic speedup from this version, because the typechecker is not yet changed. I'm confident your example will get much faster after I do some work on type checking, which I plan to do relatively soon.

Gabriella439 · 2019-04-15T22:39:47Z

Yeah, I know that on Vanessa's example, 80% of the time was spent in the type-checking phase so a 25% increase in performance on that example exactly matches the best case possible improvement without changing type-checking.

ocharles · 2019-04-16T09:21:31Z

I did wonder if that were the case. As I know this does type check, I may try dropping type checking out to see how much time is spent normalising.

ocharles · 2019-04-16T12:58:42Z

Ok, I think I've disabled the main type checking, and I see that gcc.dhall normalisation goes from taking 23.821s to 10.563s. So that's a pretty good improvement! It seems that type checking is the real pain point in my work, so hopefully future work can bring that time down.

ysangkok · 2019-07-12T01:01:51Z

@AndrasKovacs the Discourse link in your PR description is down, do you know where the information that was there can be found? Thanks.

AndrasKovacs · 2019-07-12T12:35:56Z

@ysangkok the Discourse history was deleted a while ago accidentally. Unfortunately I can't find the page now. Perhaps someone with more web cache/archive expertise can find it.

AndrasKovacs force-pushed the nbe branch from 19e231d to c5f3abc Compare March 31, 2019 19:07

jneira requested a review from Gabriella439 April 8, 2019 08:35

Add first version of new evaluator

fd39ea6

- Dhall.Eval: new evaluator, conversion checker and normalizer. There is no standalone alpha normalizer yet. - There is a new option "new-normalize" for dhall executable, which uses the new normalizer. - Type checker is unchanged.

AndrasKovacs force-pushed the nbe branch 4 times, most recently from 0387b9b to fd5114b Compare April 12, 2019 16:17

AndrasKovacs force-pushed the nbe branch from fd5114b to 3505b7a Compare April 12, 2019 16:46

f-f mentioned this pull request Apr 13, 2019

Quoted identifiers in binary encoding dhall-lang/dhall-lang#462

Closed

Merge branch 'master' into nbe

e133a28

Gabriella439 reviewed Apr 14, 2019

View reviewed changes

Review changes

1ae4036

See at: dhall-lang#876 (review)

Merge branch 'master' into nbe

c43c2ec

Gabriella439 approved these changes Apr 17, 2019

View reviewed changes

Gabriella439 merged commit fcca883 into dhall-lang:master Apr 17, 2019

Gabriella439 mentioned this pull request Jul 15, 2019

Sort the fields of record projection during normalization #1111

Merged

sjakobi mentioned this pull request Jul 15, 2019

Make isNormalized consistent with normalize #1115

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add a new environment machine normalizer #876

Add a new environment machine normalizer #876

AndrasKovacs commented Mar 31, 2019 •

edited

Loading

AndrasKovacs commented Apr 1, 2019

jneira commented Apr 8, 2019 •

edited

Loading

AndrasKovacs commented Apr 8, 2019 •

edited

Loading

Gabriella439 commented Apr 9, 2019

Gabriella439 commented Apr 9, 2019

AndrasKovacs commented Apr 9, 2019

Gabriella439 commented Apr 10, 2019

AndrasKovacs commented Apr 12, 2019 •

edited

Loading

jneira commented Apr 12, 2019

f-f commented Apr 12, 2019

jneira commented Apr 14, 2019

Gabriella439 Apr 14, 2019

AndrasKovacs Apr 14, 2019 •

edited

Loading

Gabriella439 Apr 14, 2019

AndrasKovacs Apr 14, 2019 •

edited

Loading

AndrasKovacs Apr 14, 2019

Gabriella439 Apr 14, 2019

AndrasKovacs Apr 14, 2019 •

edited

Loading

Gabriella439 Apr 14, 2019

AndrasKovacs Apr 14, 2019

AndrasKovacs Apr 14, 2019

AndrasKovacs Apr 14, 2019

ocharles commented Apr 15, 2019 •

edited

Loading

AndrasKovacs commented Apr 15, 2019

Gabriella439 commented Apr 15, 2019

ocharles commented Apr 16, 2019

ocharles commented Apr 16, 2019

ysangkok commented Jul 12, 2019

AndrasKovacs commented Jul 12, 2019

Add a new environment machine normalizer #876

Add a new environment machine normalizer #876

Conversation

AndrasKovacs commented Mar 31, 2019 • edited Loading

AndrasKovacs commented Apr 1, 2019

jneira commented Apr 8, 2019 • edited Loading

AndrasKovacs commented Apr 8, 2019 • edited Loading

Gabriella439 commented Apr 9, 2019

Gabriella439 commented Apr 9, 2019

AndrasKovacs commented Apr 9, 2019

Gabriella439 commented Apr 10, 2019

AndrasKovacs commented Apr 12, 2019 • edited Loading

jneira commented Apr 12, 2019

f-f commented Apr 12, 2019

jneira commented Apr 14, 2019

Choose a reason for hiding this comment

AndrasKovacs Apr 14, 2019 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

AndrasKovacs Apr 14, 2019 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

AndrasKovacs Apr 14, 2019 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

ocharles commented Apr 15, 2019 • edited Loading

AndrasKovacs commented Apr 15, 2019

Gabriella439 commented Apr 15, 2019

ocharles commented Apr 16, 2019

ocharles commented Apr 16, 2019

ysangkok commented Jul 12, 2019

AndrasKovacs commented Jul 12, 2019

AndrasKovacs commented Mar 31, 2019 •

edited

Loading

jneira commented Apr 8, 2019 •

edited

Loading

AndrasKovacs commented Apr 8, 2019 •

edited

Loading

AndrasKovacs commented Apr 12, 2019 •

edited

Loading

AndrasKovacs Apr 14, 2019 •

edited

Loading

AndrasKovacs Apr 14, 2019 •

edited

Loading

AndrasKovacs Apr 14, 2019 •

edited

Loading

ocharles commented Apr 15, 2019 •

edited

Loading