[Haskell-cafe] How to expose if a constraint is satisfiable

[Anthony Clayden]

On Tue, 8 May 2018 at 12:20 AM, Clinton Mead <redirect at vodafone.co.nz>
wrote:

>
> Firstly, you refer to https://wiki.haskell.org/GHC/AdvancedOverlap.
> Unfortunately (unless I've missed something) these involve listing all the
> instances of parent classes. I'm trying to avoid that. Indeed if I have to
> explicitly list all the instances I might as well write them the normal way
> so I'm not sure what the point of any trickery is.
>

Yes that approach does need declaring instances of `ShowPred` (or in
general `XXXPred`), which doubles-up the instances for `Show` (or `XXX`).
That approach is making a closed world: for every type `t`, return either
`True` or `False` that it has an instance for `Show`.

I'm not sure what you mean by "write them the normal way"? Just declaring
`t` an instance of `Show` doesn't expose that in any way you can run
type-level functions over it.


> I also tried the associated types approach you suggested towards the end
> of your email previously. This works perfectly fine if you can edit the
> base class, but I can't edit say, "Applicative" or "Num".
>

Your O.P. talked about classes `A, B`, which I assumed you were writing
fresh. What is your use case for wanting `EitherSatisfied (Applicative t)
(Num t)` for the same `t`? (Those two classes want a `t` of different
kind/arity, for one thing.)


I did something like the following, but I ran into a problem:
>
> ...
> class Num t => MyNum t where
>   type IsNum t
> instance Num t => MyNum t where
>   type IsNum t = Satisfied
>

No that won't work (as others have pointed out). That `MyNum t` instance
makes every type an instance of `MyNum`, so `(IsNum t)` always returns
`Satisfied`. And it'll always compile because the instance constraint `Num
t` is ignored for associated types. (Note that an Assoc type is just
syntactic sugar for a type family, and you can't put constraints on TF
equations.)



> Any suggestions going forward from here?
>

I'm puzzled what it is you're trying to do. Your O.P. on the cafe talked
about satisfying one or both of two constraints. Neither that nor your
StackOverflow original question 'Reducing satisfied constraints to ordinary
types' mentioned you want to use this for `Prelude` classes. Which specific
classes? There is a ghc extension coming along soon which supports some
limited froms of implications over types and instances. I'm not going to
suggest it until I know what you're trying to do.

I have a nervous feeling that you nurse incorrect expectations. This

instance Num t => MyNum t where

_does not_ say "if `t` is an instance of `Num`, it's thereby an instance of
`MyNum`". It says "every `t` is an instance of `MyNum`; if I use some
method from `MyNum` on some particular type `t0`, validate that also `Num
t0`".

There's a deep reason why Haskell works like that. See my added note to the
SO answer.

AntC
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20180508/761e808a/attachment.html>