Hi Jack and Luke, It seems you can generalize this scheme, from deriving via a "canonical injection" to deriving via any user-supplied function. The class "Injective" could thus be replaced with a more general one: class Function a b f where apply :: a -> b Instead of writing instances "Injective a b", one would write instances "Function a b Inject" (the indices are in this order because I am imagining that a proper thing to do would be for the kind of f to depend on a and b), where Inject is a "(defunctionalized) symbol", concretely defined as a dummy data type: data Inject Then there will be a newtype to take a function (a -> b) with which to transform Eq dictionaries Eq b -> Eq a: Comap seems like a fitting name. So you could write: data Foo = Foo deriving Eq via (Comap Foo Bar Inject) Provided newtype Comap a b f = Comap a instance Eq b => Eq (Comap a b f) where (==) = (==) `on` apply @a @b @f instance Function Foo Bar Inject where apply = foo2bar One advantage of this generalization is that there is no longer a notion of globally canonical injection as with the Injective class, which is quite dubious to begin with. Instead, users can declare their own Inject symbol (or whatever name is appropriate) that makes sense only within their own projects. The singletons library has some applicable machinery here to compose functions while staying at the type level (this may have only rare applications). The Function class above is equivalent to a combination of SingI (implicitly construct a singleton value) and SingKind (unrefine a singleton to a plain type). Cheers, Li-yao On 4/5/20 2:23 AM, Jack Kelly wrote:

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-Injecti... _______________________________________________ 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.