Add a new environment machine normalizer

[AndrasKovacs]

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]

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

[jneira]

@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]

@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]

@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]

@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]

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]

@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

[AndrasKovacs]

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]

wow appveyor has reached the 1 hour limit build 😟

[f-f]

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

[jneira]

@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

[Gabriella439]

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.

[AndrasKovacs]

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).

[Gabriella439]

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

[AndrasKovacs]

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

[AndrasKovacs]

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

[Gabriella439]

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

[AndrasKovacs]

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.

[Gabriella439]

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

[AndrasKovacs]

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?

[AndrasKovacs]

Or just use error with a nicer message...

[AndrasKovacs]

I used error with nicer message in new commit.

[ocharles]

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]

@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]

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]

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]

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]

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

[AndrasKovacs]

@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.