content: {-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}
  
  module PointlessP.Functors where
  
  import PointlessP.Combinators
  
  -- Data types as fixed points of functors - PolyP style
  
  class (Functor f) => FunctorOf f d | d -> f
      where inn' :: f d -> d
  	  out' :: d -> f d
  
  -- Bridge to data types as explicit fixed points
  
  newtype (Functor f) => Mu f = Mu {unMu :: f (Mu f)}
  
  instance (Functor f) => FunctorOf f (Mu f)
      where inn' = Mu
  	  out' = unMu
  
  --infixr 5 :+:
  --infixr 6 :*:
  --infixr 9 :@:
  
  -- Functors
  
  newtype Id x        = Id {unId :: x}
  newtype Const t x   = Const {unConst :: t}
  data (PSum g h) x    = Inl (g x) | Inr (h x)
  data (PProd g h) x    = PProd (g x) (h x)
  newtype (PApp g h) x = Comp {unComp :: g (h x)}
  
  -- Maps
  
  instance Functor Id
      where fmap f (Id x) = Id (f x)
  
  instance Functor (Const t)
      where fmap f (Const x) = Const x
  
  instance (Functor g, Functor h) => Functor (PSum g h)
      where fmap f (Inl x) = Inl (fmap f x)
  	  fmap f (Inr x) = Inr (fmap f x)
  
  instance (Functor g, Functor h) => Functor (PProd g h)
      where fmap f (PProd x y) = PProd (fmap f x) (fmap f y)
  
  instance (Functor g, Functor h) => Functor (PApp g h)
      where fmap f (Comp x) = Comp (fmap (fmap f) x)
  
  -- From functors to sums of products
  
  class Rep a b | a -> b
      where to :: a -> b
  	  from :: b -> a
  
  instance Rep (Id x) x
      where to (Id x) = x
  	  from x = Id x
  
  instance Rep (Const t x) t
      where to (Const t) = t
  	  from t = Const t
  
  instance (Rep (g x) y, Rep (h x) z) => Rep ((PSum g h) x) (Either y z)
      where to (Inl a) = Left (to a)
  	  to (Inr a) = Right (to a)
  	  from (Left a) = Inl (from a)
  	  from (Right a) = Inr (from a)
  
  instance (Rep (g x) y, Rep (h x) z) => Rep ((PProd g h) x) (y, z)
      where to (PProd a b) = (to a, to b)
  	  from (a, b) = PProd (from a) (from b)
  
  instance (Functor g, Rep (h x) y, Rep (g y) z) => Rep ((PApp g h) x) z
      where to (Comp x) = to (fmap to x) 
  	  from y = Comp (fmap from (from y))
  
  -- We also need the (obvious) representation of type functors
  
  instance Rep [a] [a]
      where to = id
  	  from = id
  
  -- The out and inn functions
  
  out :: (FunctorOf f d, Rep (f d) fd) => d -> fd
  out = to . out'
  
  inn :: (FunctorOf f d, Rep (f d) fd) => fd -> d
  inn = inn' . from
  
  ouT :: (FunctorOf f d, Rep (f d) fd) => d -> d -> fd
  ouT _ = to . out'
  
  inN :: (FunctorOf f d, Rep (f d) fd) => d -> fd -> d
  inN _ = inn' . from
  
  -- Auxiliary definitions
  
  instance FunctorOf (PSum (Const One) (PProd (Const a) Id)) [a] 
      where inn' (Inl (Const _))          = []
  	  inn' (Inr (PProd (Const x) (Id xs))) = x:xs
  	  out' []     = Inl (Const _L)
  	  out' (x:xs) = Inr (PProd (Const x) (Id xs))
  
  nil :: One -> [a]
  nil = inn . inl
  
  cons :: (a,[a]) -> [a]
  cons = inn . inr
  
  instance FunctorOf (PSum (Const One) Id) Int
      where inn' (Inl (Const _)) = 0
  	  inn' (Inr (Id n)) = n+1
  	  out' 0     = Inl (Const _L)
  	  out' (n+1) = Inr (Id n)
  
  zero :: One -> Int
  zero = inn . inl
  
  suck :: Int -> Int
  suck = inn . inr 
  
  instance FunctorOf (PSum (Const One) (Const One)) Bool
      where inn' (Inl _) = True
  	  inn' (Inr _) = False
  	  out' True  = Inl _L
  	  out' False = Inr _L
  
  true :: One -> Bool
  true = inn . inl
  
  false :: One -> Bool
  false = inn . inr
  
  fix :: (a->a) -> a
  fix f = f (fix f)
  