[Haskell-cafe] Looking for a library for DerivingVia idioms

[Jack Kelly]

Hello Cafe,

Here is a problem a friend (CC'd - please include him in replies) and I
wanted to solve using DerivingVia. We have a solution (below). I'm
wondering whether a library for these newtypes exists, and if not,
whether it should.

This email is Literate Haskell.

The problem: given two types `Foo` and `Bar`, and an injection
`foo2bar :: Foo -> Bar`, use DerivingVia to derive instances for
`Foo` in terms of `Bar`.

> {-# LANGUAGE DerivingVia, MultiParamTypeClasses #-}
> {-# LANGUAGE ScopedTypeVariables, TypeOperators #-}
>
> import Data.Function (on)
> import Data.Coerce (coerce)
>
> data Foo = Foo deriving Eq via (Foo `InjectedInto` Bar)
> data Bar = Bar deriving Eq
>
> foo2bar :: Foo -> Bar
> foo2bar Foo = Bar

Section 4.3 of the DerivingVia paper[1] shows how to use a newtype
wrapper to derive instances for one type in terms of another, so long as
their generic representation is the same. We can use the same technique.

We need a newtype that's representationally equal to `a`, to pass to
DerivingVia:

> newtype InjectedInto a b = InjectedInto a

We also need a class, so that we can find our injection given the type:

> class Injective a b where
>   -- Law: to x = to y => x = y
>   to :: a -> b
>
> instance Injective Foo Bar where
>   to = foo2bar

We need an instance that uses the InjectedInto newtype:

> instance (Eq b, Injective a b) => Eq (a `InjectedInto` b) where
>   (==) = (==) `on` (to :: a -> b) . coerce

The `deriving Eq via (Foo `InjectedInto` Bar)` above compiled
successfully, so everything seems to work well. I'm wondering:

1. Is a library collecting useful DerivingVia wrappers?

2. If not, suppose I wanted to stand up such a library. Is there a
   canonical library providing classes like `Injection`? I found the
   `type-iso` package, which provides an `Injective` typeclass[2], but
   it has few revdeps and a dubious instance
   Default a => Injective (Maybe b) (Either a b).

3. What about DerivingVia for types not of kind `Type`? It might be
   possible to repeat this structure one level up for `Eq1` &c. Is it
   worth supporting `Eq1` etc in a world with QuantifiedConstraints?

4. Is there a better name than `InjectedInto`? It doesn't scan
   well. A type operator, perhaps?

Thanks for reading. I look foward to your responses.

-- Jack

[1]: https://www.kosmikus.org/DerivingVia/deriving-via-paper.pdf
[2]: https://hackage.haskell.org/package/type-iso-1.0.1.0/docs/Data-Types-Injective.html#t:Injective