Add Natural/equal and Natural/lessThan primitives

[nikita-volkov]

This majorly addresses the issue of AST and memory consumption blow up in algorithms relying on those functions.

This fixes some problems discovered in dhall-lang/dhall-lang#1420.

[nikita-volkov]

The CI fails because it relies on a submodule dependency on Prelude from https://github.com/dhall-lang/dhall-lang. I have made the required PR there for the tests to pass. This submodule dependency is actually recursive, because the mentioned PR also has a breaking CI due to a dependency on this repo.

I see several ways of addressing this:

1. Remove the submodule dependency on the Prelude here and just inline whatever is needed for the tests here.
2. Update Prelude to avoid imitating the primitives in variable names (as is currently done with Natural/equal and Natural/lessThan and which is causing the problem) and update the submodule reference to it here.
3. Update dhall to allow shadowing of primitive names, thus making it backward compatible with older preludes.

[winitzki]

In my view, there is not a lot of benefit in adding lots of primitives. The real problem is the general blowup of normal forms, which is a property of the pure λ-calculus (System Fω) which Dhall implements. In λ-calculus, the beta-normal form must always evaluate under lambda, and this means no let-expressions may be left unsubsituted. A direct consequence is that many ordinary-looking programs will be huge normal forms. See also here: dhall-lang/dhall-lang#1385

Adding primitives for Natural/equal may help in one specific use case but will not help in any other cases. We cannot just keep adding primitives for each use case. There should be a better solution where the normal forms do not explode.

[nikita-volkov]

I agree that normal form caused memory blow up is a major problem and that even with these added primitives it persists due to other reasons. However I suggest reviewing these primitives in isolation from the memory blow up problem because they are useful for performance regardless. Subtracting one-by-one down to zero for comparison is just terrible for performance regardless of the ASTs.

[Gabriella439]

Yeah, the current system is not a great system. Normally the sequencing I would use in the past was:

• open a pull request against https://github.com/dhall-lang/dhall-lang/ to standardize the behavior (e.g. the new builtins)
  • this includes any updates to the Prelude and test suite and standard implementation
  • this initially fails because there isn't a matching change to dhall-haskell
• open a pull request against https://github.com/dhall-lang/dhall-haskell to implement the standardized behavior
  • this would use the open pull request as the dhall-lang submodule, so CI would pass
• update the dhall-lang PR to reference the Haskell PR
  • now CI passes
  • merge the PR
• update the dhall-haskell PR to reference dhall-lang master
  • merge the PR
• update dhall-lang (in another PR) to reference dhall-haskell master

I'm open to fixes/improvements to that. Generally, my intuition is that whatever process we design should treat dhall-lang as the source of truth, meaning that it should be possible to open and merge a pull request against dhall-lang without a matching change to dhall-haskell (although it's still desirable/useful to implement the change in dhall-haskell just to flesh out potential issues).

One possible way to fix that would be to expand the dhall-lang/standard implementation so that the Prelude CI check is tested against the standard implementation instead of testing against dhall-haskell. If we did that then the sequence of steps would be cleaner:

• open a pull request against dhall-lang to standardize the behavior
• optional: in parallel open a pull request against dhall-haskell implementing the behavior as a sanity check
• merge the dhall-lang pull request
• update the dhall-haskell pull request to reference dhall-lang master
• merge the dhall-haskell pull request

If we were to go that route the main engineering work involved would be to implement enough of the semantics to resolve, type check, normalize, and pretty-print the Prelude. The big current omissions in the standard semantics (if I remember correctly) are import resolution and pretty-printing.

[Gabriella439]

Also, regarding builtins, I think we should err on the side of having more builtins (although we should still choose them judiciously) rather than relying on implementations to be clever optimizers. My reasoning is that

• we cannot guarantee that a standards-compliant interpreter implements such an optimization
• it's easier for implementers to support new builtins rather than to implement such optimizations
• it's not clear to me that the proposed optimization reliably works

In particular, pattern matching and optimizing against a specific normal form might not work if the expression is evaluated in the wrong order. As a concrete example, suppose we have a contrived optimization that recognizes an expression of the form:

λ(x : T) → e₀

… and optimizes it to something more efficient. We run the risk of an expression like this:

(λ(x : T) → e₀) e₁

… being evaluated in the wrong order and reduced to:

e₀[x := e₁]

… before the optimization triggers. While any given implementation might not get that wrong, I'd be concerned about all implementations avoiding that potential performance pitfall.

[winitzki]

to expand the dhall-lang/standard implementation so that the Prelude CI check is tested against the standard implementation instead of testing against dhall-haskell

I'm not sure I follow this. I am not aware that there is another implementation of Dhall within dhall-lang/standard; I thought it contained only documentation. Is there executable code in dhall-lang that fully implements the Dhall standard?

If we are talking about the documentation in dhall-lang then indeed the import system is not as fully documented as the semantics. At some point I started to rewrite the standard document about the import system, but I didn't complete that work. If that's interesting I could go back to that.

[winitzki]

Subtracting one-by-one down to zero for comparison is just terrible for performance regardless of the ASTs.

Comparison of Natural is implemented by subtracting just twice; not subtracting one-by-one down to zero.

I would also like to try refactoring the existing dhall-haskell code around primitives, so that it becomes much easier to add and maintain new primitives. At the moment there are lots of different places where code must be added to support a new primitive.

[nikita-volkov]

I'm open to fixes/improvements to that. Generally, my intuition is that whatever process we design should treat dhall-lang as the source of truth, meaning that it should be possible to open and merge a pull request against dhall-lang without a matching change to dhall-haskell (although it's still desirable/useful to implement the change in dhall-haskell just to flesh out potential issues).

How about merging these into a monorepo? The current recursive dependency structure proves that these repositories are coupled. Also if we assume that the tooling around the language standard (all the standard executables) needs to always be in sync with the standard (which seems reasonable) it becomes only natural for them to be versioned and controlled in the same space. This will also let us resolve the highlighted problems of the current distribution system pretty easily.