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

[Clinton Mead]

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.

instance Print Int where print = show
instance Print Char where print = show

Seems not much more work than:

instance ShowPred Int = HTrue
instance ShowPred Bool = HTrue

etc so why use "ShowPred" at all?

>
> I'm puzzled what it is you're trying to do.
>

I'm trying to select instances based on whether constraints are fulfilled.

For example:

class Join m where
  join :: m (m a) -> m a

instance Monad m => Join m where
  join x = x >>= id

instance Comonad m => Join m where
  join = extract

Obviously I can't do this, but 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'

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

If I'm in a room, I can quite correctly assert things do exist if I can see
them. But I can't assert things can't exist. Asserting things don't exist
would violate the open world assumption, but only asserting when they do
exist should not.

"IsSatisfied" only needs to assert when the constraint is satisfied, it
doesn't need to assert when it isn't, 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. I
just need a way to entice GHC to do that.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20180508/a21a2a91/attachment.html>