[Haskell-cafe] How to expose if a constraint is satisfiable
anthony_clayden at clear.net.nz
Tue May 8 06:19:45 UTC 2018
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>
>>> 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
type instance ShowPred (a, b) = And (ShowPred a) (ShowPred b) --
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`
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
> "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.
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Haskell-Cafe