Import Prelude instead of vendoring the Prelude

[Gabriella439]

This uses Dhall's import system to fetch the Prelude so that we don't have
to keep a local copy of it

[sellout]

Looks like this uncovered some caching issue?

[Gabriella439]

@sellout: Actually, it was the other way around. The caching was working correctly, and the mismatch identified an issue with the uncached version.

The root cause was a violation of the standard in the β-normalization logic. The standard doesn't include the type annotation as part of a non-empty list, meaning that the type annotation is treated as an ordinary type annotation and not one specific to lists. This implies that a non-empty list with a type annotation should normalize to one without a type annotation.

The binary encoding logic was correctly stripping the type annotation from non-empty lists, but the ordinary normalization logic was not, which led to a test failure. The Prelude decoded from the cache didn't have the type annotation but the expected test output did. The expected test output was wrong because the type annotation wasn't supposed to be there.

[f-f]

We should probably adjust the nixpkgs derivations to account for this? The current assumption is that there was a folder called "Prelude" in this repo: https://github.com/NixOS/nixpkgs/blob/master/pkgs/development/interpreters/dhall/default.nix#L14

/cc @Profpatsch

[Profpatsch]

Is this a problem in practice? The folder still exists and dhall handles the import transparently, right?

[f-f]

@Profpatsch yes, but one would not have the files locally anymore (which is the point of using a Nix install instead of pinning a commit hash from github)

[Profpatsch]

Hm. I think a user might still want the nix output, to use the “official” version of Prelude that comes with the dhall release. No surprises about invalid syntax or other breaking features then.

[Gabriella439]

I'm a little unclear about what is proposed on either side, so I'll restate what I think you both are saying and then chime in with my own thoughts

I think @f-f is proposing that pkgs.dhall.prelude should point to the language-agnostic Prelude (i.e. the one here:

https://github.com/dhall-lang/dhall-lang/tree/master/Prelude

On the other hand, I think @Profpatsch is proposing that pkgs.dhall.prelude should point to the one that the Haskell implementation tests against here:

https://github.com/dhall-lang/dhall-haskell/tree/master/Prelude

... which imports a specific revision of the language-agnostic Prelude. My understanding is that the reasoning is that the Prelude attached to the Haskell implementation of Dhall should be the Haskell-specific one, whereas the language-agnostic prelude belongs somewhere else.

Now, for my own thoughts:

Part of the issue here is that the Haskell implementation took over the top-level pkgs.dhall attribute, even though Nixpkgs will eventually support other Dhall implementations (such as dhall-clj). One way we can fix this is that pkgs.dhall can have one passthru attribute for each language binding. In other words, one would still be able to install pkgs.dhall (which will still default to the Haskell implementation for backwards compatibility), but one could also install pkgs.dhall.haskell or pkgs.dhall.clojure to be more specific about which language implementation they wish to select.

Under that scenario, you could have all three of pkgs.dhall.prelude, pkgs.dhall.haskell.prelude, and pkgs.dhall.clojure.prelude. pkgs.dhall.prelude would point to the latest release of the language-agnostic Prelude, and pkgs.dhall.haskell.prelude would point to the Prelude that the Haskell implementation builds against and pkgs.dhall.clojure.prelude would point to the Prelude that the Clojure implementation builds against.

[Profpatsch]

I’m open to all of these.

[f-f]

Thanks @Gabriel439, good summary.
I don't plan in making a cli tool out of the clojure implementation so we won't have it in nixpkgs, but other implementations might want to be there, so I like the naming scheme being proposed here 👍

My reasoning for having the language-agnostic Prelude inpkgs.dhall.prelude is the following: the current one here in this repo is just a pointer, so when you install the derivation you won't have the actual Prelude files. Which means that if you're offline:

• you can't inspect the implementation of any Prelude function
• if you didn't run dhall importing the local Prelude at least once (for the caching of pinned expressions to work) you won't be able to import the Prelude

[Profpatsch]

you can't inspect the implementation of any Prelude function

You are right, that was one of the reasons I added the prelude in the first place.

I like Gabriel’s proposal. I’ll submit a PR implementing it.

[Profpatsch]

I’ve got a proposal PR in NixOS/nixpkgs#49116.

Instead of just adding the prelude, I think it’s time to push the dhall libraries as a package set.
We could even “compile” them by building up a cache of parsed and normalized binary forms that can be used by the interpreter.