The primary reason for this change is to make it easier to describe these values
both in documentation and in informal communication between developers.
Before, you'd have to say things like:
* A value of type `Maybe` (incorrect)
* A `Maybe` value (sounds weird)
* A value of type `Maybe a` for some `a` (correct, but very verbose)
Now you can say an `Optional` value and the meaning is precise and clear
A secondary reason for this change is to keep the terminology close to the
intended use of the language for configuration files. Describing fields as
`Optional` instead of `Maybe` makes a lot of sense for configurations.
The disadvantage is that some uses of `Optional` don't make sense. For example,
consider the type of `List/head`:
List/head : ∀(a : Type) → List a → Optional a
It seems weird to say that the result of `List/head` is `Optional`. However,
many languages (such as Java/Scala/F#/Swift) already use this name or `Option` and
they get along just fine.
Dhall was failing to parse `++` because the `+` operator was being parsed with
higher priority. The fix is to switch the order in which the two operator
parses are tried
The old implementation produces better error messages because it preserves the
original order in which variables were bound. For example, if you wrote:
λ(a : Type) → λ(x : a) → y
... under the `Map`-based implementation, that would give the following
out-of-order `Context` when displaying the error message:
Context:
x : a
a : Type
... but with the old list-based implementation, the correct order is presented:
Context:
a : Type
x : a
