Being the default value is not the same as being actively set
to a value which happens to match the default. `Maybe` as a type
constructor enriching an existing type with a default value is not
satisfactory: what this default value means is not documented in the
type.

When designing a command line interface, it is quite often necessary to provide default values for some of the flags.

Sometimes there is only one sensible choice and it is simply picked when initialising the record of options. In Agda for instance we set the default verbosity to 1 (the bigger the number, the more detailed the debugging information) and ask for the empty context (the more specific the context, the more irrelevant information is filtered out).

Other times, there are multiple sensible choices and they may be incompatible.
In Agda, both guardedness checking and sized types can be used to program with
codata. But combining the two makes the system unsound. By default we want
users to be able to use both so both are turned on. However if they use the
`--safe` flag, they should only be allowed to use at most one. We want
to shout at the user if they actively turn both on and declare the module
should be safe. So we need to distinguish between the flags being set to
the default and them being actively set to a value which happens to match the
default.

We could be using `Maybe` as the type constructor extending a type
with a default value. However the design choices are now scattered in a
lot of different places:

- sensible defaults are set in the initial record value,
- the choice to use
`Maybe`to add a neutral default value is made explicit in the type, - but this default value is declared somewhere else e.g. in a cleanup function computing the final set of options,
- if we collapse
`Maybe a`to`a`in multiple locations, we need to be consistent and make sure that we use the same default everywhere.

data WithDefault k (a :: k) where Default :: WithDefault k a Value :: k -> WithDefault k a

When we write WithDefault Bool 'True we explicitly
tell the reader that our `Maybe`-looking optional type will default
to `True` unless the value has been set. We can start by writing
the function which let us set a value. In case it's been set already we
simply ignore the new value.

setDefault :: k -> WithDefault k a -> WithDefault k a setDefault k v = case v of Default -> Value k _ -> v

Now that we can set the value, it's only natural to want to also get it.
In case it still is the `Default`, we need to be able to produce the
term-level value which corresponds to the type level one. To do that we need
some extra machinery.

The hasochistic device that allows us to connect term and type levels is naturally the notion of singletons. We postulate the existence of a data family of singletons, that is to say that to each type-level constructor should correspond a term-level one indexed by it.

data family Sing k (a :: k)

We say that a type-level value is `Known` if we can obtain a singleton
for it. We also assume that if a value is known then we are able to erase a
singleton for it down to its mere term level value.

class Known k (a :: k) | a -> k where sing :: Sing k a erase :: Sing k a -> k

Now that we have the ability to turn a type-level value into a term level one,
we can write a function out of `WithDefault`. It is essentially the
function `fromMaybe` except that we do not need to specify what to do
in case we find our `Nothing`-like constructor: provided that the
type-level value is `Known`, the type itself tells us what the output
should be.

collapseDefault :: forall k a. Known k a => WithDefault k a -> k collapseDefault x = case x of Default -> erase (sing :: Sing k a) Value v -> v

So what do instances of these data and class definitions look like?

Using a Generalized Algebraic DataType (GADT), we define the singleton
for booleans like so: `STrue` is the term-level constructor
reflecting the type-level `'True` whilst `SFalse` corresponds
to `'False`. This makes both `'True` and `'False`
known booleans: we have singletons for them and can easily produce the
underlying `Bool`.

data instance Sing Bool b where STrue :: Sing Bool 'True SFalse :: Sing Bool 'False instance Known Bool 'True where sing = STrue erase _ = True instance Known Bool 'False where sing = SFalse erase _ = False

Using these instances, we can already write some examples. Evaluating the following expression yields the expected list [False,True,True]

bool :: [Bool] bool = collapseDefault <$> [ Value False , Value True , Default :: WithDefault Bool 'True ]

We are not limited to ground types: we can give instances for polymorphic
container types by assuming we have instances for the elements they store.
This is where the fact that `Sing` is a data family of singletons
shines: we have a unique name for all of these constructs. Let us define
the following singleton datatype for `Maybe`:

data instance Sing (Maybe a) m where SNothing :: Sing (Maybe a) 'Nothing SJust :: Sing a v -> Sing (Maybe a) ('Just v)

The type-level constructor `'Nothing` is evidently known: its
singleton is `SNothing` and it erases to the term level value
`Nothing`.

instance Known (Maybe a) 'Nothing where sing = SNothing erase _ = Nothing

We can only say that `'Just v` is known if `v` itself
already is. We obtain the right singleton by using the assumption
that `v` is known to obtain a singleton for it and wrap it
in an `SJust` constructor. Erasure is defined in a similar
manner: we output `Just` and use `erase` to compute
its content.

instance Known a v => Known (Maybe a) ('Just v) where sing = SJust sing erase (SJust v) = Just (erase v)

We have similar instances for lists and pairs.

Unfortunately the current setup means we cannot state that we expect to
be given a string but will happily default to "Hello" if we are not given
anything. GHC does provide us with `Symbol`, the kind of type-level
strings. So we ought to be able to also support default values for various
string types such as `Text`.

The trick here is to decorrelate the kind of the type-level value and the
type it represents. Instead of the `WithDefault` type we defined
earlier, we use the following more general one as our core representation.
The original `WithDefault` is the special case where kind and type
do match up.

data WithDefault k (a :: l) where Default :: WithDefault k a Value :: k -> WithDefault k a

This change needs to be propagated through all the families, classes,
instance declarations, and functions. The interested reader can check
the Haskell file. We choose
to focus here on the `Text` instance.

We can't quite define an enumerated type providing a constructor for each
string in existence. However the kind people at GHC's HQ are already doing
this for us:
`GHC.TypeLits`
gives us access to `KnownSymbol`. Our data instance for `Text`
is capturing a constraint of the form `KnownSymbol s` as the notion
of singleton for `s`.

data instance Sing Text (s :: Symbol) where SText :: KnownSymbol s => Sing Text s

Using the GHC-provided function `symbolVal`, we can obtain a
`String` corresponding to a given `KnownSymbol`. As a
consequence, if `s` is a known symbol, we can trivially build
a proof that it is a `Known Text` too.

instance KnownSymbol s => Known Text (s :: Symbol) where sing = SText erase = pack . symbolVal

Although the instance declarations are now a bit more verbose, the user experience is virtually the same. And we now support string literals. The following test showcasing all of the instances mentioned in this post evaluates to the list [[(True,Just "Hello World")],[(False,Nothing)]]:

test :: [[(Bool, Maybe Text)]] test = collapseDefault <$> [ Default :: WithDefault [(Bool, Maybe Text)] '[ '( 'True , 'Just "Hello World") ] , Value [(False, Nothing)] ]

We have seen that we can define an optional type indexed by the value
it should default to. Using standard type-level trickery we can write
the function collapsing the `Default` constructor to the value
specified in the type. Although this most general version works well,
it requires fairly recent `LANGUAGE` extensions so
we are not using it in the Agda codebase,
limiting ourselves to the special case of the `Bool` version.

Last update: 2024 04