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

[Li-yao Xia]

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-Injective.html#t:Injective
> _______________________________________________
> 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.
>