Extend merge to work on Optionals (#860)

… as discussed in #463.

standard/beta-normalization.md

@@ -1283,6 +1283,30 @@ matching label:
     merge t u ⇥ v
 
 
+`Optional`s are handled as if they were union values of type
+`< None | Some : A >`:
+
+
+    t ⇥ { Some = f, … }   o ⇥ Some a   f a ⇥ b
+    ──────────────────────────────────────────
+    merge t o : T ⇥ b
+
+
+    t ⇥ { Some = f, … }   o ⇥ Some a   f a ⇥ b
+    ──────────────────────────────────────────
+    merge t o ⇥ b
+
+
+    t ⇥ { None = v, … }   o ⇥ None A
+    ────────────────────────────────
+    merge t o : T ⇥ v
+
+
+    t ⇥ { None = v, … }   o ⇥ None A
+    ────────────────────────────────
+    merge t o ⇥ v
+
+
 If the handler or union are abstract, then normalize each subexpression:
 
 

standard/type-inference.md

@@ -718,11 +718,28 @@ An implementation could simply loop over the inferred record type.
     Γ ⊢ merge t₀ u₀ : T₀
 
 
+`Optional`s can also be `merge`d as if they had type `< None | Some : A >`:
+
+
+    Γ ⊢ o : Optional A
+    o ⇥ None A
+    Γ ⊢ merge t < None | Some : A >.None : T
+    ────────────────────────────────────────
+    Γ ⊢ merge t o : T
+
+
+    Γ ⊢ o : Optional A
+    o ⇥ Some a
+    Γ ⊢ merge t (< None | Some : A >.Some a) : T
+    ────────────────────────────────────────────
+    Γ ⊢ merge t o : T
+
+
 If the first argument of a `merge` expression is not a record then that is a
 type error.
 
-If the second argument of a `merge` expression is not a union then that is a
-type error.
+If the second argument of a `merge` expression is not a union or an `Optional`
+then that is a type error.
 
 If you `merge` an empty union without a type annotation then that is a type
 error.

tests/normalization/success/unit/MergeNoneA.dhall

@@ -0,0 +1 @@
+merge { None = False, Some = \(b : Bool) -> b } (None Bool)

tests/normalization/success/unit/MergeNoneB.dhall

@@ -0,0 +1 @@
+False

tests/normalization/success/unit/MergeSomeA.dhall

@@ -0,0 +1 @@
+merge { None = False, Some = \(b : Bool) -> b } (Some True)

tests/normalization/success/unit/MergeSomeB.dhall

@@ -0,0 +1 @@
+True

tests/type-inference/success/unit/MergeNoneA.dhall

@@ -0,0 +1 @@
+merge { None = False, Some = \(b : Bool) -> b } (None Bool)

tests/type-inference/success/unit/MergeNoneB.dhall

@@ -0,0 +1 @@
+Bool

tests/type-inference/success/unit/MergeSomeA.dhall

@@ -0,0 +1 @@
+merge { None = False, Some = \(b : Bool) -> b } (Some True)

tests/type-inference/success/unit/MergeSomeB.dhall

@@ -0,0 +1 @@
+Bool