New subject: Encoding superclass relationships as a constraint?

7 Jun 2017

      Using ExistentialQuantification, it’s possible to create a rather
generic type that packages some arbitrary dictionary up at runtime:

    data Some ctx = forall a. ctx a => Some a

This is nice, but it’s not very interesting. It would be nice if we
could define a Show instance for our type, and a naïve implementation
is trivial:

    instance Show (Some Show) where
      show (Some x) = show x

However, this isn’t very useful in practice, since it means we can only
show values of precisely the type (Some Show), which are better
represented as values of type String. However, we might reasonably have
some class with Show as a superclass:

    class Show a => Foo a
    instance Foo ()

...and we might want to show values of type (Some Foo). However, this
won’t work with the naïve implementation, since Foo is not the same as
Show.

Clearly, what we want is some instance like this:

    instance (ctx ≈> Show) => Show (Some ctx)

...where (a ≈> b) can be read “a implies b”. Unfortunately, as far as I
can tell, this isn’t actually possible in any general way.

The closest thing I was able to come up with was a less general solution
using Edward Kmett’s constraints package. It’s possible to write (≈>)
with some manual boilerplate:

    import Data.Constraint
    import Data.Constraint.Forall

    class Class (ctx a) (ctx' a) => Class1' ctx ctx' a
    instance Class (ctx a) (ctx' a) => Class1' ctx ctx' a

    type Class1 ctx ctx' = Forall (Class1' ctx ctx')
    type a ≈> b = Class1 b a

...and then it’s possible to write that Show instance:

    instance (ctx ≈> Show) => Show (Some ctx) where
      show (Some (x :: a)) = case inst @(Class1' Show ctx) @a of
        Sub Dict -> case (cls :: ctx a :- Show a) of
          Sub Dict -> show x

However, this means users have to manually implement Class instances for
their classes. Using the above example of Foo, a user would have to
write the following instance:

    instance Class (Show a) (Foo a) where cls = Sub Dict

With that instance, we can properly show values of type (Some Foo):

    ghci> Some () :: Some Foo
    ()

But this instance is both trivial and annoying, since it means the
machinery leaks out of the implementation code and into the code that
uses it. I’m wondering if there’s any way to do this more generally, and
if not, if there’s any reason it could not or should not be supported
by GHC itself.

Alexis

Encoding superclass relationships as a constraint?

Alexis King

Li-yao Xia

tags

participants (2)