Interesting Bits from Rotten Bananas pt. I

RB.hs

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}

module RB where


data F a
  = Lam a (a -> a)
  | Pi a (a -> a)
  | App a a
  | Star
  | Box

class ExpFunctor f where
  xmap :: (a -> b) -> (b -> a) -> f a -> f b

xmapF :: Functor f => (a -> b) -> (b -> a) -> f a -> f b
xmapF = const . fmap

instance ExpFunctor F where
  xmap _ _ Box        = Box
  xmap _ _ Star       = Star
  xmap f _ (App a a') = App (f a) (f a')
  xmap f g (Pi a h)   = Pi (f a) (f . h . g)
  xmap f g (Lam a h)  = Lam (f a) (f . h . g)

newtype O f g e = Comp { deComp :: f (g e) }

instance (Functor f, Functor g) => Functor (O f g) where
  fmap f = Comp . fmap (fmap f) . deComp

instance (ExpFunctor f, ExpFunctor g) => ExpFunctor (O f g) where
  xmap f g = Comp . xmap (xmap f g) (xmap g f) . deComp

newtype Nu f = Nu { old :: f (Nu f) }

class Cata f t | t -> f where
  cata :: (f a -> a) -> t -> a

class Ana f t | t -> f where
  ana :: (a -> f a) -> a -> t

instance Functor f => Cata f (Nu f) where
  cata f = f . fmap (cata f) . old

instance Functor f => Ana f (Nu f) where
  ana f = Nu . fmap (ana f) . f

newtype Square f a = Square { unSquare :: f (f a) }

instance Contravariant f => Functor (Square f) where
  fmap f = Square . cofmap (cofmap f) . unSquare