Add `WithDefault` construct

[gallais]

It's folklore that we can encode default implicit values in a DTT with instance
arguments that may be explicitly applied. We should add this construct to the
stdlib (I just have something else to do right now so I'm posting this so that
I don't forget about it).

Comments on the name of the constructor / field are welcome.

module Default where

record WithDefault (A : Set) (a : A) : Set where
  constructor give
  field value : A
open WithDefault

instance
  default : ∀ {A a} → WithDefault A a
  default {a = a} = give a

open import Agda.Builtin.Nat

inc : Nat → {{step : WithDefault Nat 1}} → Nat
inc m {{step}} = m + step .value

open import Agda.Builtin.Equality

_ : inc 2 ≡ 3
_ = refl

_ : inc 2 {{step = give 3}} ≡ 5
_ = refl

[jamesmckinna]

Commenting on this long after it seemed marooned in the history; any likelihood of it being picked up again?

I offer the following (opinionated!), for the sake of discussion:

On naming:

• re: the type name, I'd be happier with Default {A : Set} (a : A) instead of WithDefault A a, which seems 'noisier'? And one can always use Function.Base._∋_ if necessary...;
• re: field name, value seems fine, but I'm (personally) fond of ⟦_⟧ for This Kind Of Thing...;
• re: constructor name, do we need one? I guess we do for overriding the default, as in the second test example, so why not override, to drive the point home? Accordingly,

record Default (a : A) : Set where
  constructor override
  field ⟦_⟧ : A
open Default

instance
  default : Default a
  default {a = a} = override a

inc : Nat → {{Default 1}} → Nat
inc m {{step}} = m + ⟦ step ⟧

_ : inc 2 ≡ 3
_ = refl

_ : inc 2 {{override 3}} ≡ 5
_ = refl

Otherwise (without a named constructor) I suppose one has to write something (or: some where clause shenanigans) such as

_ : let ⟦ override ⟧ = 3 in inc 2 {{override}} ≡ 5
_ = refl

Alternatively (cf. defaulting as a scoped effect a la Koka), one could perhaps imagine a default as a local 'variable', which might lead instead to constructor set and field accessor get, for example?

[gallais]

We do have something in http://agda.github.io/agda-stdlib/v2.0/Data.Default.html

[jamesmckinna]

Oh... should have checked, but seeing as the issue was still open, and hadn't been closed automatically by #1556 ... I guess add that weeding out open issues should be an admin task, too ;-)