Create a gist now

Instantly share code, notes, and snippets.

What would you like to do?
Representing internal applications of indexed datatypes in generic-deriving
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?
{-# 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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment