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
