Going further with a builtin-based prelude

[neongreen]

Groundwork

Let's pretend that we have implemented #800 and now we have the ability to supply type signatures and documentation for built-ins.

Let's further pretend that #835 got in and now all built-ins (like List/head) live in the Dhall prelude, pretty much like Int64# lives in the Haskell base even though it's a built-in.

While we're at it, let's make it so that List and friends can be both types and records, so that List and List.map are both accepted. (Don't know how.)

Magical prelude import syntax

Then let's implement syntax for importing the prelude, e.g. with prelude:

with prelude https://prelude.dhall-lang.org/v10.0.0/package.dhall sha256:blah

-- From now on *all* names that are not in scope are treated as coming
-- from https://prelude.dhall-lang.org/v10.0.0/package.dhall; this
-- includes Natural, List.map, etc
λ(f : Natural → Natural) → List.map Natural Natural f [1, 2, 3]

Any expression can have not more than one with prelude parent. (You can't say with prelude ... with prelude ....)

Note: downloading the whole prelude might be slow, unless we use HTTP/2 or consolidate the prelude into a few modules. It only has to be done once, though.

Magic is bad, but here's what we get in return

The prelude proposal provides a bunch of major benefits at once:

• IDEs can easily show you documentation for built-ins like Natural because they are not exactly built-ins anymore – they are defined entities, with documentation, tests, etc. This works out well for Haskell. Partly solves User documentation of built-in types and functions #766.

• Currently people mostly seem to import individual functions instead of let Prelude = .... You can't even have let List = https://prelude.dhall-lang.org/List/package.dhall because it's a parse error. Per-function imports are kinda annoying, and this proposal kills per-function imports in most cases.

• IDE plugins and syntax highlighters can highlight local definitions vs Prelude definitions without having to consult the Dhall language server, because now everything not explicitly defined with let somewhere above is a Prelude definition.

• Better ergonomics for heavy DSLs like dhall-kubernetes – I no longer need to type kubernetes. everywhere and I still know which bindings are local vs which come from dhall-kubernetes (assuming the idea about syntax highlighting is picked up).

As well as some minor benefits:

• Discussion: fallback import searches that add .dhall #680 ("fallback import searches that add .dhall") is not needed anymore.

• You can always say what version of Dhall standard is used by a piece of code.

• You can look at https://prelude.dhall-lang.org/v10.0.0/package.dhall and see exactly what builtins are at your disposal. Also useful in case of codebases with heavy use of custom builtins as per Proposal: "forward declarations" for custom built-ins #800, because now there's a natural place for them.

• We can make Dhall interpreter writers' lives easier – see Turn List.map into a builtin #741. Let's say we declare all prelude functions as something like let map = (builtin List/map : <type>) ? <non-builtin implementation>. Now every interpreter writer can either provide a fast List/map builtin, or spend effort on making the non-builtin implementation perform well, or do nothing.

  So, interpreter writers can start by implementing as few built-ins as possible, and then decide whether their effort would be better spent on implementing N builtins – or making the interpreter smarter. (And "do nothing" remains an option!)

Going further (optional): stripping keywords of their special status

It's not great that toMap, Some, merge are keywords (for a bunch of reasons). The proposal above won't help us get rid of them, unless we augment #800 with support for untyped builtins.

The idea is that you can say:

let builtin toMap : _

Then the interpreter will have to provide a typing judgment for the builtin during the typechecking phase.

Going further still: stripping operators of their special status

Mostly same as above. Since we want to prevent users from defining operators (?), we can specify that only builtins can be operators.

In its current incarnation, dhall format will not be able to format code without resolving imports (it needs to know operator precedences), which isn't great. However, e.g. Ormolu actually manages to format Haskell code without knowing operator precedences (tweag/ormolu#353), so dhall-lang/dhall-haskell#1496 + some heuristics might turn out to be good enough. Or we could hardcode information about existing operators into the formatter.

This will also let us fix things like #701 in a backwards-compatible manner.

How can List and List.map coexist?

I don't know how to allow List to be used as a type while still allowing List.map.

Perhaps we can go back to List/map but specify that foo/bar is a special form meaning modules.foo.bar (thanks to T::{x} for the inspiration). Then the prelude would look like this:

{ List = builtin List : Type -> Type
, Optional = builtin Optional : Type -> Type
, modules =
    { List = { map = ..., head = ..., ...}
    , Optional = {...}
    , ...
    }
}

This would make it impossible to provide your own List/foo names without overriding the prelude (which can be done by using a recursive merge). I don't know whether it's a good thing or a bad thing.

[neongreen]

More possible issues:

This breaks most/all Dhall code in existence.

• We'll have to introduce an implicit prelude and keep it around for a few release cycles.

Running Dhall code would require internet access in many more cases.

• Dhall interpreters will have to ship with a cache of recent preludes (which they should do anyway to avoid making a bad first impression).

[neongreen]

How would normalized forms look like?

Normalized forms for these two inputs will be equivalent:

with prelude https://prelude.dhall-lang.org/v10.0.0/package.dhall

List/map

let builtin List : Type → Type

let builtin List-fold : ∀(a : Type) → List a → ∀(list : Type) → ∀(cons : a → list → list) → ∀(nil : list) → list

in   λ(a : Type)
   → λ(b : Type)
   → λ(f : a → b)
   → λ(xs : List a)
   → List-fold
       a
       xs
       (List b)
       (λ(x : a) → λ(`as` : List b) → [ f x ] # `as`)
       ([] : List b)

I'm not sure how exactly builtins should be normalized so the second snippet might not be the final normalized form.

I have just realized that this would require that the signature of builtin List-fold is allowed to refer to builtin List. No idea how this might be implemented.

[neongreen]

Oh, I guess builtins will just be inlined since they have quasi-structural equality, just like union types are inlined. Then the final normalized form looks like:

  λ(a : Type)
→ λ(b : Type)
→ λ(f : a → b)
→ λ(xs : (builtin List : Type → Type) a)
→ (builtin List-fold 
       : ∀(a : Type)
       → (builtin List : Type → Type) a 
       → ∀(list : Type) 
       → ∀(cons : a → list → list)
       → ∀(nil : list)
       → list)
    a
    xs
    ((builtin List : Type → Type) b)
    (λ(x : a) → λ(`as` : (builtin List : Type → Type) b) → [ f x ] # `as`)
    ([] : (builtin List : Type → Type) b)

This is not pretty at all. Can we omit those type declarations? I guess we can't without type inference. But if we have type inference and if we are allowed to shorten builtin to something like !, it's not so bad anymore:

  λ(a : Type)
→ λ(b : Type)
→ λ(f : a → b)
→ λ(xs : !List a)
→ !List-fold 
    a
    xs
    (!List b)
    (λ(x : a) → λ(`as` : !List b) → [ f x ] # `as`)
    ([] : !List b)

This all might be going a bit too far 🤔

[neongreen]

I have never used dhall normalize and I don't think that without knowing its usecases I can decide on a good way to normalize builtin-heavy code.

E.g. I would have assumed that normalizing List.map to an unwieldy List/fold expression is pretty bad. Furthermore, inlining all union types and record types seems to make the code quite unreadable. In this case, maybe normalizing everything down to builtins isn't a bad thing either?

[neongreen]

What about literals?

The following judgments would hold:

1 : (builtin Natural : Type)

[ 1 ] : (builtin List : Type -> Type) (builtin Natural : Type)

"foo" : (builtin Text : Type)

This allows users of a Dhall interpreter to pick their own internal representation for Natural, List, Text, which might be useful for fine-tuning the interpreter without forking it – e.g. you might want to pick a different list type that better fits your usecase (dhall-lang/dhall-haskell#1574).

In fact, regardless of the fate of the Builtin-Based Prelude Proposal (henceforth BBPP), I think we should totally extend #800 to include builtin declarations for types so that we can embed custom data structures into Dhall and enjoy fast operations on them.

[neongreen]

@matheus23 thanks for the initial idea! It's all your fault I enjoyed sketching this out.

[neongreen]

Further still, this provides a cleaner path for backwards-incompatible changes to builtins.

Let's say that for some silly reason we have to change the behavior of Text/show. Standard v10 calls builtin Text/show in the prelude:

-- prelude.dhall

{ Text = builtin Text : Type
, modules =
    { Text =
        { show = builtin Text/show : Text -> Text
        , ... }

Standard v11 calls builtin Text/show_v2:

-- prelude.dhall

{ Text = builtin Text : Type
, modules =
    { Text =
        { show = builtin Text/show_v2 : Text -> Text
        , ... }

However, as long as the interpreter provides both builtins, it will actually support both versions of the standard – and you will be able to upgrade the interpreter while still sticking to an older version of the standard, behavior-wise.

We will also be able to deprecate and remove functions while still giving users a way to upgrade to a newer version of the standard gradually – i.e. "from now on all new modules should use standard v11" instead of "we have to upgrade everything to v11 or we can't use the new interpreter".

[neongreen]

It also looks like turning keywords/operators into untyped builtins will kill a lot of normalization opportunities – e.g. "a" ++ "b" can't be normalized to "ab" if ++ is defined via a builtin, and similarly toMap {a = 1} can't be normalized to [ { mapKey = "a", mapValue = 1 } ].

(But again, I don't know what people use normalization for.)

[Gabriella439]

Similar to my comment in #800 (comment) I think we should begin from requirements before considering the design

My understanding is that the requirements are what you listed underneath the "what we get in return" section, which I will summarize here:

• We would like to document built-ins the same way we document non-builtins

• We would like to make import lists less granular (e.g. make importing the Prelude as a whole more ergonomic)

• We would like to make language tooling more version-agnostic with respect to builtins

• We would like to make it easy to bring a package's contents into scope easily unqualified

For each requirement I'll first comment on whether I agree with the requirement and then comment on what I believe is the simplest solution that addresses the stated requirement

We would like to document built-ins

I believe the idiom of re-exporting built-ins from the Prelude satisfies this requirement, because we can document the re-exported built-in. For example: List/length

We would like to make import lists less granular

I question this requirement because I'm not convinced that granular imports are the norm. As a package consumer, I do commonly import the Prelude as a whole (or dhall-kubernetes as a whole, too). The few times that I do use granular imports are when I'm a package author, in order to avoid import cycles. For example the renderYAML utility from the Prelude is an example of a utility that relies on more granular imports to avoid cycles.

However, I don't believe the stated design would fix the latter issue: avoiding cyclic imports would still require people to use more granular imports when authoring packages.

We would like to make the language tooling more version agnostic

I think this is a good goal. More generally, it would be nice if we streamlined the process of adding new builtins to the language by having a uniform way to do so. However, I think #800 addresses a lot of this requirement already.

More convenient unqualified imports

I question this requirement because I'm not a fan of open imports. In my experience, open imports make it difficult for people unfamiliar with the code to tell where identifiers come from if you have multiple open imports in scope.

[Profpatsch]

We would like to make import lists less granular

I question this requirement because I'm not convinced that granular imports are the norm.

Ideally, in a form like

let prelude = https://… in 42;

The import would never be resolved in the first place.

Similarly, in

let prelude = https://… in prelude.List.map …

Only the files package.dhall, List/package.dhall and List/map.dhall would have to be requested at all.

I don’t know how feasible that is for the dhall standard, but it’s one of the big advantages of interleaving imports with evaluation (like how the nix or the bazel evaluator work).