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:
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.