The old list-based implementation was tuned for Morte and more efficient for
type-checking typical Morte expressions (such as Church-encoded bytes), that had
multiple occurrences of the same key. I'm still not sure why it was more
efficient, though, but it may have been due to better use of laziness.
However, these sorts of expressions are rare in idiomatic Dhall code, so we use
the more direct approach using a `Map` for faster lookup of the outer keys and
a `Seq` for faster indexing into the elements associated with a given key.
In other words, instead of writing:
let f (x : Natural) = x + 1
in ...
... you must now write:
let f = λ(x : Natural) → x + 1
in ...
The reason for this is two-fold:
* The implementation is much simpler, which matters for porting Dhall to other
languages
* This is more consistent with handlers for the newly added `apply` notation,
where the handlers have to be expressed as anonymous functions
Example usage:
let handlers = { Left = Natural/even, Right = \(x : Bool) -> x }
in let union = < Left = +2 | Right : Bool >
in apply handlers union : Bool
Note that I haven't even implemented union literals, so this can't even be used,
yet!
This lets you access the field of a union if it has exactly one alternative.
The basic idea is that a subsequent change will provide an operator for merging
pattern matches with the following pseudo-type:
a : Type, b : Type, r : Type |- (\/) : (a → r) → (b → r) → (a \/ b → r)
For example:
(\/)
: (< foo : Bool > → Integer)
→ (< bar : Text > → Integer)
→ (< foo : Bool | bar : Text > → Integer)
You can then combine `(\/)` in conjunction with field access to implement
pattern matching:
let example : < foo : Bool | bar : Natural > → Bool =
(λ(x : < foo : Bool >) → x.foo )
\/ (λ(x : < bar : Natural >) → Natural/even (x.bar))
in example
There are two main reasons that I'm removing `(++)`:
* I would like to use `(++)` instead of `(<>)` for combining `Text` so that
`<>` can be used for the empty sum type
* `(++)` leads to quadratic time complexity when used repeatedly. `List/concat`
is the preferred API for combining lists
The original motivation for adding `Text/concat` was to work around the
quadratic time complexity of using `(<>)` repeatedly, but this is no longer an
issue now that Dhall uses `Builder` internally to represent `Text`
The simpler approach still permitted variable capture. For example, this would
break:
\x -> (\y -> (\x -> y)) x
That should reduce to:
\x -> \x -> x@1 -- ... not even expressible under the simpler system
... but it actually reduced to:
\x -> \x -> x
This also required disabling multi-`let` since in the process of fixing this I
realized that this expression is ambiguous:
\(x : Type) ->
let x : Type = Bool
let f (y : x) = y
in f -- ^ Which `x` does this refer to
... because it's supposed to be semantically equivalent to:
\(x : Type) ->
( \(x : Type)
-> \(f : forall (y : x) -> x)
-> f -- ^ This refers to the inner `x : Type`
)
Bool
(\(y : x) -> y)
-- ^ ... but this refers to the outer `x : Type`
Now the code only permits a single `let` binding in each `let ... in` expression
