Dhall-lang: Deprecating Optional/fold

[sjakobi]

Since https://github.com/dhall-lang/dhall-lang/pull/860 we can use merge to destructure Optionals instead of the less ergonomic Optional/fold. Since Optional/fold is one of the more complex builtins, I think it would be beneficial to get rid of it.

Here's a proposal for a roadmap for removing it:

1. v13: Standardize merge for Optionals

2. v15: Change Prelude.Optional.fold to use merge

3. v17: Remove Optional/fold as a builtin

4. Some point in the future: Consider removing Prelude.Optional.fold.

Thoughts?

[SiriusStarr]

I agree that there's little reason to have it with merge for consuming Optionals. The only advantage (I can think of) to Optional/fold is that it can be partially applied more readily, but you can always wrap merge in a lambda if you need that behavior.

[Gabriel439]

@sjakobi: We could also remove Optional/build as a built-in while we are at it. The only reason it was added was for consistency (since every other */fold function had a matching */build function)

However, I think we should consider keeping Prelude.Optional.fold indefinitely. There's essentially no cost to keeping things in the Prelude. I'm more in favor of aggressively removing things from the standard than the Prelude to ease porting new language bindings.

Also, some people might be interested in preserving Prelude.Optional.fold purely from a pedagogical point of view.

[sjakobi]

Removing Optional/build too makes sense to me. Here's a patch for Prelude.Optional.build:

--- a/Prelude/Optional/build
+++ b/Prelude/Optional/build
@@ -9,7 +9,14 @@ let build
           → optional
         )
       → Optional a
-    = Optional/build
+    =   λ(a : Type)
+      → λ ( f
+          :   ∀(optional : Type)
+            → ∀(some : a → optional)
+            → ∀(none : optional)
+            → optional
+          )
+      → f (Optional a) (λ(x : a) → Some x) (None a)

 let example0 =
         assert

Does this updated roadmap seem alright? I'll prepare a proper migration plan for docs.dhall-lang.org in that case.

1. v13: Standardize merge for Optionals

2. v15:

   • Change Prelude.Optional.fold to use merge
   • Update Prelude.Optional.build with the patch above
   • Update other Prelude functions to remove usage of Optional/fold and Optional/build

3. v17: Remove the Optional/fold and Optional/build builtins

[Gabriel439]

@sjakobi: Yeah, that roadmap looks good to me!