[Haskell-cafe] Check a lack of a constraint?
olf at aatal-apotheke.de
Tue Jul 13 23:09:30 UTC 2021
> Hello cafe,
> Is it possible in Haskell to check a lack of a certain constraint?
> For example,
> foo :: C => a
> foo = undefined
> Here `foo` can only be compiled if called with C satisfied. How do I write the
> opposite, so that `foo` is only possible to use when C is not satisfied?
> With best regards.
Indeed I found myself wanting this, too. Such a feature might reduce
the amount of overlapping instances, but of course it bears the danger
that others pointed out.
For example, suppose you have a type
T :: (* -> *)
and the library author of T already defined an instance
instance C a => C (T a).
Now suppose you have a concrete type A which you know can never have a
(lawful) C A instance, but you can define an instance C (T A). The
latter would be formally overlapping with the former, even if you know
that the former will never be implemented.
Thus, instead of local non-satisfiability, a token for the proof that
an instance can not exist might be more useful (and more safe). This
would correspond to case 2 in Sylvain Henry's GHC proposal. I have no
idea, however, how such a proof can be presented [*] in a way that can
not be circumvented by a third author and lead to unsoundness.
As a concrete example, I defined an instance
MonadParsec (StateT String Maybe)
which makes a wonderfully fast parser that you can swap in for a
Megaparsec parser, but it is overlapping because of
MonadParsec Maybe => MonadParsec (StateT s Maybe)
although it is absurd to try to make Maybe an instance of MonadParsec.
Another example: Think about why the mtl library has an instance
MonadFoo m => MonadFoo (BarT m)
for every pair (Foo,Bar) of transformers.
(And there are quadratically many of these!)
It is precisely because a catch-all instance like
(MonadTrans t, MonadFoo m) => MonadFoo (t m)
will be overlapping as long as we can't rule out MonadFoo (t m) by
[*] The logically natural way would be to have a Void constraint, so
that we can say:
MonadParsec Maybe => Void
More information about the Haskell-Cafe