Created
October 10, 2012 22:02
-
-
Save nfrisby/3868766 to your computer and use it in GitHub Desktop.
Representing internal applications of indexed datatypes in generic-deriving
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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? |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# 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