[Haskell-cafe] More experiments with ATs

[Sjoerd Visscher]

On Jul 3, 2010, at 4:39 PM, Andrew Coppin wrote:

> class Container c => Functor c where
>   fmap :: (Functor cx, Functor cy, Element cx ~ x, Element cy ~ y) => (x -> y) -> (cx -> cy)
> 
> However, this fails horribly: The type signature fails to mention c.

You have to mention c, this means an extra argument to fmap. But if you do that you also get the opportunity to restrict what x and y can be. 

As you'll have to pass around this extra argument, it will usually be easier to just pass around the map function though.

> type family F f a :: *
> class RFunctor f where
>   (%) :: f a b -> (a -> b) -> F f a -> F f b

Then you can make ByteString an instance using a GADT:

> data BSFunctor :: * -> * -> * where
>   BS :: BSFunctor Word8 Word8
> type instance F BSFunctor Word8 = B.ByteString
> instance RFunctor BSFunctor where
>   BS % f = B.map f

Regular functors are still instances as well of course.

> data Ftor :: (* -> *) -> * -> * -> * where
>   Ftor :: Functor f => Ftor f a b
> type instance F (Ftor f) a = f a
> instance RFunctor (Ftor f) where
>   Ftor % f = fmap f

Set can be an instance too:

> data SetFunctor :: * -> * -> * where
>   SetF :: (Ord a, Ord b) => SetFunctor a b
> type instance F SetFunctor a = Set.Set a
> instance RFunctor SetFunctor where
>   SetF % f = Set.map f

Or Strings. Let's do 3 functors in one take:

> data StringFunctor :: * -> * -> * where
>   EachChar :: StringFunctor Char Char
>   EachWord :: StringFunctor String String
>   EachLine :: StringFunctor String String
> type instance F StringFunctor a = String
> instance RFunctor StringFunctor where
>   EachChar % f = map f
>   EachWord % f = unwords . map f . words
>   EachLine % f = unlines . map f . lines

And finally the identity functor and functor composition.

> data Id a b = Id
> type instance F Id a = a
> instance RFunctor Id where
>   Id % f = f
>   
> data (:.:) :: (* -> * -> *) -> (* -> * -> *) -> * -> * -> * where
>   (:.:) :: (RFunctor g, RFunctor h) => g (F h a) (F h b) -> h a b -> (g :.: h) a b
> type instance F (g :.: h) a = F g (F h a)
> instance RFunctor (g :.: h) where
>   (g :.: h) % f = g % (h % f)

Functor composition requires UndecidableInstances, because of the nested type family application. Perhaps one day GHC will be able to tell that this is structural recursion, and therefore not undecidable.

This is a variation on what I'm doing in data-category 0.2, which is not done yet, but you can take a look here:
http://github.com/sjoerdvisscher/data-category/

greetings,
Sjoerd Visscher