
But by doing so I am changing type equality to the same as having "type
family F a :: * -> *"
F' a x ~ F' b y <=> F' a ~ F' b /\ x ~ y (equality for ADTs)
and I would like this "decomposition rule not to apply" so.
Thanks though,
hugo
On Tue, Mar 18, 2008 at 1:12 AM, Ryan Ingram
On 3/17/08, Hugo Pacheco
wrote: type family G a :: * -> * type instance G Int = Either () -- you forgot this line
instance Functor (G Int) where fmap f (Left ()) = Left () fmap f (Right x) = Right (f x)
One thing that you don't seem to be clear about is that there is something slightly magic going on in this Functor definition; you are not declaring Functor (G Int) but rather Functor (whatever (G Int) turns into). This is using a GHC extension "TypeSynonymInstances". The extension allows you to use type synonyms when declaring instances, but only if they are fully applied, and the compiler is simply applying the substitution for you.
That is to say, this code is no different than the following:
type family G a :: * -> * type instance G Int = Either () instance Functor (Either ()) where fmap f (Left ()) = Left () fmap f (Right x) = Right (f x)
Once you declare a more complicated type function, such as type family F a x :: * this extension can no longer come into play.
You can get around this restriction with a newtype:
type family F a x :: * type instance F Int x = Either () x
newtype F' a b = F' (F a b)
instance Functor (F' Int) where fmap f (F' (Left ())) = F' (Left ()) fmap f (F' (Right x)) = F' (Right $ f x)