This is to be pedantic in ensuring that a record type should type check if the
equivalent Boehm-Berarducci encoding type-checks. For example, the following
record type:
{ x : Type }
... is technically valid when Boehm-Berarducci-encoded:
∀(record : Type) → ∀(make : ∀(x : Type) → record) → record
... even if this is totally useless because you can't actually extract the
type from the record or use it as a type for another field.
Parsing `App` with source annotations was using a really inefficient form of
backtracking which greatly slowed down the speed of parsing. This change uses a
non-backtracking solution that still preserves source annotations which gives a
10x speed up on some small test programs like this one:
λ(n : Natural)
→ λ(a : Type)
→ λ(f : Natural → a)
→ List/build
a
( λ(list : Type)
→ λ(cons : a → list → list)
→ List/fold
{ index : Natural, value : {} }
( List/indexed
{}
( List/build
{}
( λ(list : Type)
→ λ(cons : {} → list → list)
→ Natural/fold n list (cons {=})
)
)
)
list
(λ(x : { index : Natural, value : {} }) → cons (f x.index))
)
There was a needless use of backtracking in the implementation of `exprA` that
incurred a significant performance cost. Left-factoring the `exprA` parser
improves speed significantly
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.
