FFreeDup.hs

{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE UndecidableInstances #-}
module FFreeDup where
import Data.Bifunctor
import Control.Monad (ap)

type f ~> g = forall x. f x -> g x

class (forall g. Functor g => Functor (ff g)) => FFunctor ff where
  ffmap :: (Functor g, Functor h) => (g ~> h) -> (ff g x -> ff h x)

class FFunctor ff => FMonad ff where
  fpure :: (Functor g) => g ~> ff g
  fbind :: (Functor g, Functor h) => (g ~> ff h) -> ff g a -> ff h a

-- | The free 'FMonad' for a @'FFunctor' ff@.  
data FFree ff g x = FPure (g x) | FFree (ff (FFree ff g) x)

deriving instance (Functor g, Functor (ff (FFree ff g))) => Functor (FFree ff g)

instance (FFunctor ff) => FFunctor (FFree ff) where
  ffmap gh (FPure gx) = FPure (gh gx)
  ffmap gh (FFree fmx) = FFree (ffmap (ffmap gh) fmx)

instance (FFunctor ff) => FMonad (FFree ff) where
  fpure = FPure
  fbind k (FPure gx) = k gx
  fbind k (FFree fmmx) = FFree (ffmap (fbind k) fmmx)

{-

Trail (FFree ff)
 ~ FFree ff (a,) ()
 ~ (a,()) + ff (FFree ff (a,)) ()

-}

---------------------------

newtype Dup g x = MkDup (g (g x))
  deriving Functor

instance FFunctor Dup where
  ffmap :: (Functor g, Functor h) => (g ~> h) -> Dup g x -> Dup h x
  ffmap gh (MkDup ggx) = MkDup (gh . fmap gh $ ggx)

-- | FD ~ FFree Dup
data FD g x = FPure' (g x) | FFree' (FD g (FD g x))
  deriving Functor

instance FFunctor FD where
  ffmap gh (FPure' gx) = FPure' (gh gx)
  ffmap gh (FFree' fmx) = FFree' (ffmap gh . fmap (ffmap gh) $ fmx)

instance FMonad FD where
  fpure = FPure'
  fbind k (FPure' gx) = k gx
  fbind k (FFree' mmx) = FFree' (fbind k . fmap (fbind k) $ mmx)

----------------------------

-- | T ~ FD (b,) a; T () ~ Trail FD
data T a b =
    Pure a b
      -- ~ (b,) a
  | Nest (T (T a b) b)
      -- ~ T (FD (b,) a) b
      -- ~ FD (b,) (FD (b,) a)
      -- ~ Dup (FD (b,)) a
      -- ~ Dup (FFree Dup (b,)) a

to :: T a b -> FD ((,) b) a
to (Pure a b) = FPure' (b,a)
to (Nest tt) = FFree' $ to (first to tt)

from :: FD ((,) b) a -> T a b
from (FPure' (b,a)) = Pure a b
from (FFree' mm) = Nest $ from (fmap from mm)

instance Functor (T a) where
  fmap = second

instance Bifunctor T where
  bimap f g (Pure a b) = Pure (f a) (g b)
  bimap f g (Nest tt) = Nest $ bimap (bimap f g) g tt

instance (a ~ ()) => Applicative (T a) where
  pure = Pure ()
  (<*>) = ap

instance (a ~ ()) => Monad (T a) where
  ma >>= k = tbind' k ma

-- Type-generalized (=<<)
tbind :: (b -> T () b') -> T r b -> T r b'
tbind k = from . dbind (to . k) . to

-- tbind in terms of FD
dbind :: (b -> FD ((,) b') ()) -> FD ((,) b) r -> FD ((,) b') r
dbind k = fbind (plug . first k)

plug :: Functor f => (f (), c) -> f c
plug (f1, c) = c <$ f1

{-

dbind k mb
 = fbind (plug . first k) mb
 = fbind (\(b,c) -> c <$ k b)) mb
         ^-------------------^ = k'

fbind k' (FPure' (b,())
 = k' (b,())
 = () <$ k b
 = k b

fbind k' (FFree' mm)
 = FFree' (fbind k' . fmap (fbind k') $ mm)

Pure b () >>= k
  = from $ dbind (to . k) (to (Pure b ()) 
  = from $ fbind (to . k)' (FPure b ())
  = from $ (to . k) b
  = k b

Nest tt >>= k
  = from $ dbind (to . k) (to (Nest tt))
  = from $ dbind (to . k) $ FFree' (to . fmap to $ tt)
  = from $ fbind (to . k)' (FFree' (to . fmap to $ tt))
  = from $ FFree' (fbind (to . k)' . fmap (fbind (to . k)') . to . first to $ tt)
  = from $ FFree' (fbind (to . k)' . to . first (fbind (to . k)' . to) $ tt)
  = Nest $ from . fmap from . fbind (to . k)' . to . first (fbind (to . k)' . to) $ tt
  = Nest $ from . fbind (to . k)' . to . first (from . fbind (to . k)' . to) $ tt
  = Nest $ from . dbind (to . k) . to . first (from . dbind (to . k) . to) $ tt
  = Nest $ tbind k . first (tbind k) $ tt
-}

tbind' :: (b -> T () b') -> T r b -> T r b'
tbind' k (Pure r b) = first (const r) (k b)
tbind' k (Nest tt) = Nest $ tbind k . first (tbind k) $ tt

-- | Free magma monad
data Bin b = Tip b | Node (Bin b) (Bin b)
  deriving Functor

instance Applicative Bin where
  pure = Tip
  (<*>) = ap

instance Monad Bin where
  Tip b >>= k = k b
  Node e1 e2 >>= k = Node (e1 >>= k) (e2 >>= k)

toBin :: T a b -> (a, Bin b)
toBin (Pure a b) = (a, Tip b)
toBin (Nest tt) =
  let (tLeft, rightBin) = toBin tt
      (a, leftBin) = toBin tLeft
  in (a, Bin leftBin rightBin)

fromBin :: (a, Bin b) -> T a b
fromBin (a, Tip b) = Pure a b
fromBin (a, Bin e1 e2) = Nest $ fromBin (fromBin a e1) e2

{-

bbind :: (b -> ((), Bin b')) -> (a, Bin b) -> (a, Bin b')
bbind k (a, mb) = (a, mb >>= snd . k)
bbind k = second (>>= snd . k)

[ bbind (toBin . k) (toBin ma) === toBin (tbind' k ma) ]

Case analysis on ma

1. ma = Pure a b

bbind (toBin . k) (toBin (Pure a b))
  = bbind (toBin . k) (a, Tip b)
  = (a, Tip b >>= toBin . k)
  = (a, k b)
  = first (const a) (toBin (k b))
  = toBin (first (const a) (k b))
  = toBin (tbind' k (Pure a b))

2. ma = Nest tt

bbind (toBin . k) (toBin (Nest tt))
  = let (t1, br) = toBin tt
        (a, bl) = toBin t1
    in bbind (toBin . k) (a, Bin bl br)
  = let (t1, br) = toBin tt
        (a, bl) = toBin t1
    in (a, Bin (bl >>= snd . toBin . k) (br >>= snd . toBin . k))
  = let (t1, br') = second (>>= snd . toBin . k) $ toBin tt
        (a, bl') = second (>>= snd . toBin . k) $ toBin t1
    in (a, Bin bl' br')
  = let (t1, br') = bbind (toBin . k) $ toBin tt
        (a, bl') = bbind (toBin . k) $ toBin t1
    in (a, Bin bl' br')
  -- By structural induction --
  = let (t1, br') = toBin (tbind' k tt)
        (a, bl') = toBin (tbind' k t1)
    in (a, Bin bl' br')
  = let (e1, br') = first (tbind' k) $ toBin (tbind' k tt)
        (a, bl') = toBin e1
    in (a, Bin bl' br')
  = let (e1, br') = toBin $ tbind' k (first (tbind' k) tt)
        (a, bl') = toBin e1
    in (a, Bin bl' br')
  = toBin $ Nest $ tbind' k (first (tbind' k) tt)
  = toBin $ tbind' k (Nest tt)
-}