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

[Clinton Mead]

Hi Anthony

Perhaps I've misunderstood, but there's a few issues with the approaches
you suggest:

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.

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". I did something like
the following, but I ran into a problem:

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleInstances #-}

data Satisfied

class Num t => MyNum t where
  type IsNum t
instance Num t => MyNum t where
  type IsNum t = Satisfied

data D = D

f :: IsNum t ~ Satisfied => t -> ()
f _ = ()

main = print $ f D

Ideally this should not compile, but unfortunately it happily compiles,
showing that GHC generates an "IsNum" type family instance for "D", despite
the fact that "Num D" is not satisfied.

Any suggestions going forward from here?


On Mon, May 7, 2018 at 9:11 PM, Anthony Clayden <
anthony_clayden at clear.net.nz> wrote:

> > It's occurred to me that one could write a class C t which is satisfied
>
> > whenever (A t) or (B t) is satisfied like so:
>
> Hi Clinton, this sounds like you might want "Choosing a type-class instance based on the context"
> https://wiki.haskell.org/GHC/AdvancedOverlap
>
>
> > ---
> >
> > data Satisfied
> >
> > type family IsSatisfiable :: Constraint -> Type
>
> That type family is doing the same job as auxiliary class `ShowPred` on that wiki page.
>
> Rather than all the machinery you give for the disjunction, you could use another type family:
>
> type family EitherSatisfied :: Type -> Type -> Type
> instance EitherSatisfied Satisfied tb = Satisfied
> instance EitherSatisfied ta Satisfied = Satisfied
>
> Those two instances do overlap (as you expected); and they exhibit confluence, aka coincident overlap (they produce the same result); so that's fine.
>
> But you haven't given any instances for `IsSatisfiable`. How do you expect to get from the Constraint to the `Satisfied` type?
>
> You say
>
> > IsSatisfiable c = Satisfied -- (if c is satisfiable)
>
> What are you going to put for `c`? If you follow that wiki page, you'll need to in effect repeat every instance decl for classes `A, B`:
>
> instance A Int where ...
>
> type instance IsSatisfiable (A Int) = Satisfied
>
> (The wiki page was written before there were type families, so type class `ShowPred` has a Functional Dependency giving a type-level Boolean result.)
> Your `C t` class becomes
>
> class EitherSatisfied ( IsSatisfiable (A t)) ( IsSatisfiable (B t)) ~ Satisfied => C t where ...
>
> ----
>
> Nowadays there's a better way: make Associated Types for the two classes, give them a default instance:
>
> class A t where
>   type APred t
>   type instance APred t = Satisfied
>   ...
>
> class B t where
>   type BPred t
>
>   type instance BPred t = Satisfied
>   ...
>
>
> Now every instance defined for `A, B` in effect automatically gives you
> `APred, BPred` instances. Then
>
> class EitherSatisifed (APred t) (BPred t) ~ Satisfied => C t where ...
>
>
> AntC
>
>
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20180507/4460d66f/attachment.html>