Representing internal applications of indexed datatypes in generic-deriving

discussion

The elimination of Functor from @Generic1@ is the benefit provided by @:\@:@,
in exchange for the cost of a slight complication in the @:\@:@ instances. It
enables @Generic1@ to be used even if those internally applied types are not
@Functors@, which in particular allows internal application of GADTs. This is
the motivation for removing the @Functor@ constraints from @Generic1@
instances.

On the other hand, I can only think of one interesting generic function on
types of kind (* -> *) that doesn't inherently require @Functor@ on the
internally applied types:

  @type-equality:Data.Type.Equality.EqT@,

and that's not a huge motivator, is it? Also, it's quite complicated to do
generically -- I'm still working on it in PVGD.

Other possible classes that don't obviously require @Functor@ of the applied
types include @Eq@ and 'Enum', but it turns out that the benefit of @:\@:@ is
wasted on them.

Here's why. Let the @* -> *@ flavours of these classes be @Eq1@ and
@Enum1@. The @:.:@ instance (and hence the @:\@:@ instance) for @Eq1@ does
actually require that @t@ be a @Functor@: it uses @zip@ and @foldMap@, which
implies @Functor@. As far as I understand, @Enum1@ cannot support GADTs, only
@Enum@ can because the instance selection depends on the argument type of the
GADT being enumerated (cf the relevant instances in "Generic Programming with
Indexed Datatypes" by Magalhaes and Jeuring). So neither @Eq1@ nor @Enum1@ can
support GADTs, and hence derive no actual benefit from @:\@:@.

So…

What are the generic functions used on GADTs?

Do any of them not require the internally applied types to be covariant?

Is @EqT@ the only one? Is it compelling?

NewGDApp.hs

{-# LANGUAGE TypeFamilies, TypeOperators, ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving, FlexibleContexts, UndecidableInstances #-}

module NewGDApp where

import GHC.Generics hiding ((:.:)) -- I'm proposing an alternative to @:.:@.



-- Only for representations of constructor arguments, ie the leaves of @:*:@.                                                                                        
type family UnRep1 (rep :: * -> *) (p :: *) :: *
class UnGeneric1 (rep :: * -> *) where
  fromUn1 :: rep       p -> UnRep1 rep p
  toUn1   :: UnRep1 rep p ->       rep p

type instance UnRep1 Par1     p = p
type instance UnRep1 (K1 i c) p = c
type instance UnRep1 (Rec1 f) p = f p
instance UnGeneric1 Par1     where fromUn1 = unPar1 ; toUn1 = Par1
instance UnGeneric1 (K1 i c) where fromUn1 = unK1   ; toUn1 = K1
instance UnGeneric1 (Rec1 f) where fromUn1 = unRec1 ; toUn1 = Rec1



-- My proposed alternative to @:.:@.                                                                                                                                  
infixr 7 :@:
newtype (t :@: rep) p = App1 {unApp1 :: t (UnRep1 rep p)}
deriving instance Eq   (t (UnRep1 rep p)) => Eq   ((t :@: rep) p)
deriving instance Show (t (UnRep1 rep p)) => Show ((t :@: rep) p)

type instance UnRep1 (t :@: rep) p = t (UnRep1 rep p)
instance UnGeneric1 (t :@: rep) where fromUn1 = unApp1 ; toUn1 = App1



-- Like @:.:@, @:\@:@ is still a @Functor@ if @t@ and @rep@ are @Functor@s.                                                                                               
instance (Functor t, Functor rep, UnGeneric1 rep) => Functor (t :@: rep) where
  fmap f = App1 . fmap (wrap (fmap f)) . unApp1 where
    wrap g = fromLeaf1 . g . (id :: forall x. rep x -> rep x) . toLeaf1






data MyList f a = MyNil | MyCons [f a] (MyList f a)

-- If @:.:@ were used instead of @:\@:@, this instance would require @Functor                                                                                         
-- f@.                                                                                                                                                                
instance Generic1 (MyList f) where
  type Rep1 (MyList f) = U1 :+:
    [] :@: f :@: Par1 :*: Rec1 (MyList f)
  from1 MyNil = L1 U1
  from1 (MyCons x y) = R1 $ App1 x :*: Rec1 y
  to1 (L1 U1) = MyNil
  to1 (R1 (App1 x :*: Rec1 y)) = MyCons x y