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

[Anthony Clayden]

On Tue, 8 May 2018 at 2:00 PM, Clinton Mead <redirect at vodafone.co.nz> wrote:

> On Tue, May 8, 2018 at 11:17 AM, Anthony Clayden <
> anthony_clayden at clear.net.nz> wrote:
>
>>
>> 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.
>>
>
> By normal way as in if I need to list every instance as "ShowPred", I
> might as well just scrap "ShowPred" and just write them directly as
> instances of "Print". i.e.
>

No you haven't got it: there's a default/fallback instance for `Print` that
applies if `ShowPred` comes out `False`. Also if you have `True/False` you
can do Boolean logic over the result:

type instance ShowPred [a] = ShowPred a
         -- implication
type instance ShowPred (a, b) = And (ShowPred a) (ShowPred b)       --
conjunction

including either/or logic, which is where your O.P. started. (Although we
seem to have come a long way from that.) So turning to your latest example
...


>> I'm puzzled what it is you're trying to do.
>>
>
> I'm trying to select instances based on whether constraints are fulfilled.
>
> ... consider:
>
> class Join' m (IsSatisfied m) (IsSatisfied m) => Join m where
>   join :: m (m a) -> m a
>
> instance  Join' m (IsSatisfied m) (IsSatisfied m) => Join m where
>   join = join'
>

?? I think that context needs something like

instance Join' m (IsMonad m) (IsComonad m) => Join m where ...


> instance Monad m => Join' m Satisfied t2 where
>   join' x = x >>= id
>
> instance Comonad m => Join' m t1 Satisfied where
>   join' = extract
>
> instance Comonad m => Join' m Satisfied Satisfied where
>   join' = extract
>

So if some `m0` is both a `Comonad` and a `Monad`, you want to prefer the
`Comonad` method. If `m0` is a `Monad` but not a `Comonad`, use the `Monad`
method.

You've just invoked a closed world: you're relying on the compiler
determining some `m0` is _not_ a `Comonad`.

Technically: your instances for `Join'` overlap. So the compiler's
inference selection must determine which is the more specific, given some
particular `m0` with its `t1, t2` result from `IsSatisfied`. It can select
head `Join' m Satisfied t2` only if it can prove `t2` is apart from
`Satisfied`.

...
>

> "IsSatisfied" only needs to assert when the constraint is satisfied, it
> doesn't need to assert when it isn't, ...
>

Yes it does for what you're asking to do.


so I don't think it violates the open world assumption. Also GHC has this
> information to give an answer to IsSatisfied, it simply has to try to solve
> the constraint and if it succeeds reduce it to Satisfied, and if it doesn't
> it just does nothing.
>

To the contrary: what you want it to do is select a different instance.


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