Currently the empty of Monoid is specified as a nullary function rather than a plain value. Is there a plausible use case that benefits from empty being a function or requires it to be a function?
At the moment, I'm tempted to specify empty as a plain value in a use case of monoid.