{-# LANGUAGE CPP                 #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE LambdaCase          #-}
{-# LANGUAGE ScopedTypeVariables #-}

-- |
--   Module:     Control.Varying.Core
--   Copyright:  (c) 2015 Schell Scivally
--   License:    MIT
--   Maintainer: Schell Scivally <schell@takt.com>
--
--   Varying values represent values that change over a given domain.
--
--   A varying value takes some input as its domain (e.g. time, place, etc)
--   and when run using 'runVarT' it produces a value and a new varying value.
--   This pattern is known as an automaton and `varying` uses this pattern at its
--   core. With the additon of monadic event sequencing, 'varying' makes it easy
--   to construct complicated signals that control program and data flow.
module Control.Varying.Core
  ( -- * Types and Typeclasses
    Var
  , VarT(..)
    -- * Creating vars
    -- $creation
  , done
  , var
  , arr
  , varM
  , mkState
    -- * Composing vars
    -- $composition
  , (<<<)
  , (>>>)
    -- * Adjusting and accumulating
  , delay
  , accumulate
    -- * Sampling vars (running and other entry points)
    -- $running
  , scanVar
  , stepMany
    -- * Debugging and tracing vars in flight
  , vtrace
  , vstrace
  , vftrace
  , testVarOver
    -- * Proofs of the Applicative laws
    -- $proofs
  ) where

import           Control.Applicative
import           Control.Arrow
import           Control.Category
import           Control.Monad
import           Control.Monad.Fix
import           Control.Monad.IO.Class
import           Data.Functor.Contravariant
import           Data.Functor.Identity
import           Debug.Trace
import           Prelude                    hiding (id, (.))

--------------------------------------------------------------------------------
-- Core datatypes
--------------------------------------------------------------------------------
-- | A continuously varying value, with effects.
-- It's a kind of <https://en.wikipedia.org/wiki/Mealy_machine Mealy machine>
-- (an automaton).
newtype VarT m a b
  = VarT
  { runVarT :: a -> m (b, VarT m a b) }
  -- ^ Run a @VarT@ computation with an input value of
  -- type 'a', yielding a step - a value of type 'b'
  -- and a new computation for yielding the next step.


-- | A var parameterized with Identity that takes input of type @a@
-- and gives output of type @b@. This is the pure, effect-free version of
-- 'VarT'.
type Var a b = VarT Identity a b

--------------------------------------------------------------------------------
-- Typeclass instances
--------------------------------------------------------------------------------
-- | You can transform the output value of any var:
--
-- >>> let v = 1 >>> fmap (*3) (accumulate (+) 0)
-- >>> testVarOver v [(),(),()]
-- 3
-- 6
-- 9
instance Applicative m => Functor (VarT m b) where
  fmap f v = VarT $ (g <$>) . runVarT v
    where g (b, vb) = (f b, f <$> vb)

-- | A var is a category.
--
-- @
--   id = var id
--   f . g = g >>> f
-- @
--
-- or
--
-- >  f . g = f <<< g
--
-- >>> let v = accumulate (+) 0 . 1
-- >>> testVarOver v [(),(),()]
-- 1
-- 2
-- 3
instance Monad m => Category (VarT m) where
    id = var id
    f0 . g0 = VarT $ \a -> do
      (b, g) <- runVarT g0 a
      (c, f) <- runVarT f0 b
      return (c, f . g)

-- | Vars are applicative.
--
-- >>> let v = (,) <$> pure True <*> pure "Applicative"
-- >>> testVarOver v [()]
-- (True,"Applicative")
--
-- Note - checkout the <$proofs proofs>
instance Applicative m => Applicative (VarT m a) where
    pure = done
    vf <*> vx = VarT $ \a ->
      g <$> runVarT vf a <*> runVarT vx a
      where g (f, vf1) (x, vx1) = (f x, vf1 <*> vx1)

-- | Vars are arrows, which means you can use proc notation, among other
-- meanings.
--
-- >>> :set -XArrows
-- >>> :{
-- let v = proc t -> do
--           x <- accumulate (+) 0 -< t
--           y <- accumulate (+) 1 -< t
--           returnA -< x + y
-- in testVarOver v [1,1,1]
-- >>> :}
-- 3
-- 5
-- 7
--
-- which is equivalent to
--
-- >>> let v = (+) <$> accumulate (+) 0 <*> accumulate (+) 1
-- >>> testVarOver v [1,1,1]
-- 3
-- 5
-- 7
instance Monad m => Arrow (VarT m) where
  arr = var
  first v = VarT $ \(b, d) -> g d <$> runVarT v b
    where g d (c, v') = ((c, d), first v')

instance MonadPlus m => ArrowZero (VarT m) where
  zeroArrow = varM $ const mzero

instance MonadPlus m => ArrowPlus (VarT m) where
  VarT f <+> VarT g = VarT $ \a -> f a `mplus` g a

-- |
instance Monad m => ArrowChoice (VarT m) where
  left f  = f +++ arr id
  right f = arr id +++ f
  f +++ g = (f >>> arr Left) ||| (g >>> arr Right)
  f ||| g = VarT $ \case
    Left b -> do
      (d, f1) <- runVarT f b
      return (d, f1 ||| g)
    Right c -> do
      (d, g1) <- runVarT g c
      return (d, f ||| g1)

-- | Inputs can depend on outputs as long as no time-travel is required.
--
-- This isn't the best example but it does make a good test case:
--
-- >>> :{
-- let
--   testVar :: VarT IO Double (Maybe Double)
--   testVar = proc val -> do
--     rec _ <- returnA -< 0.5
--     returnA -< Just 5.0
-- in
--   testVarOver testVar [5.0]
-- >>> :}
-- Just 5.0
instance MonadFix m => ArrowLoop (VarT m) where
  loop vmbdcd = VarT $ \b -> fmap fst $ mfix $ \(~(_, d)) -> do
    ((c1, d1), vmbdcd1) <- runVarT vmbdcd (b, d)
    return ((c1, loop vmbdcd1), d1)

-- | VarT with its input and output parameters flipped.
newtype FlipVarT m b a = FlipVarT { unFlipVarT :: VarT m a b }

-- | A VarT is contravariant when the type arguments are flipped.
instance Monad m => Contravariant (FlipVarT m b) where
  contramap f (FlipVarT vmab) = FlipVarT $ VarT $ \c -> do
    (b, vmab1) <- runVarT vmab $ f c
    return (b, unFlipVarT $ contramap f $ FlipVarT vmab1)

#if __GLASGOW_HASKELL__ >= 804
-- | Vars can be semigroups
--
-- >>> let v = var (const "Hello ") <> var (const "World!")
-- >>> testVarOver v [()]
-- "Hello World!"
instance (Applicative m, Semigroup b) => Semigroup (VarT m a b) where
  (<>) = liftA2 (<>)
#endif

-- | Vars can be monoids
--
-- >>> let v = var (const "Hello ") `mappend` var (const "World!")
-- >>> testVarOver v [()]
-- "Hello World!"
instance (Applicative m, Monoid b) => Monoid (VarT m a b) where
  mempty = pure mempty
  mappend = liftA2 mappend

-- | Vars can be written as numbers.
--
-- >>> let v = 1 >>> accumulate (+) 0
-- >>> testVarOver v [(),(),()]
-- 1
-- 2
-- 3
instance (Monad m, Num b) => Num (VarT m a b) where
    (+) = liftA2 (+)
    (-) = liftA2 (-)
    (*) = liftA2 (*)
    abs = fmap abs
    signum = fmap signum
    fromInteger = pure . fromInteger

-- | Vars can be written as floats.
--
-- >>> let v = pi >>> accumulate (*) 1 >>> arr round
-- >>> testVarOver v [(),(),()]
-- 3
-- 10
-- 31
instance (Monad m, Floating b) => Floating (VarT m a b) where
    pi = pure pi
    exp = fmap exp
    log = fmap log
    sin = fmap sin; sinh = fmap sinh; asin = fmap asin; asinh = fmap asinh
    cos = fmap cos; cosh = fmap cosh; acos = fmap acos; acosh = fmap acosh
    atan = fmap atan; atanh = fmap atanh

-- | Vars can be written as fractionals.
--
-- >>> let v = 2.5 >>> accumulate (/) 10
-- >>> testVarOver v [(),(),()]
-- 4.0
-- 1.6
-- 0.64
instance (Monad m, Fractional b) => Fractional (VarT m a b) where
    (/) = liftA2 (/)
    fromRational = pure . fromRational
--------------------------------------------------------------------------------
-- $creation
-- You can create a pure var by lifting a function @(a -> b)@
-- with 'var':
--
-- > arr (+1) == var (+1) :: VarT m Int Int
--
-- 'var' is a parameterized version of 'arr'.
--
-- You can create a monadic var by lifting a monadic computation
-- @(a -> m b)@ using 'varM':
--
-- @
-- getsFile :: VarT IO FilePath String
-- getsFile = varM readFile
-- @
--
-- You can create either with the raw constructor. You can also create your
-- own combinators using the raw constructor, as it allows you full control
-- over how vars are stepped and sampled:
--
-- > delay :: Monad m => b -> VarT m a b -> VarT m a b
-- > delay b v = VarT $ \a -> return (b, go a v)
-- >     where go a v' = VarT $ \a' -> do (b', v'') <- runVarT v' a
-- >                                      return (b', go a' v'')
-- >
--------------------------------------------------------------------------------
-- | Lift a pure computation to a var. This is 'arr' parameterized over the
-- @a `VarT m` b@ arrow.
var :: Applicative m => (a -> b) -> VarT m a b
var f = VarT $ \a -> pure (f a, var f)

-- | Lift a monadic computation to a var. This is
-- <http://hackage.haskell.org/package/arrow-list-0.7/docs/Control-Arrow-Kleisli-Class.html#v:arrM arrM>
-- parameterized over the @a `VarT m` b@ arrow.
varM :: Monad m => (a -> m b) -> VarT m a b
varM f = VarT $ \a -> do
    b <- f a
    return (b, varM f)

-- | Lift a constant value to a var.
done :: Applicative m => b -> VarT m a b
done = var . const

-- | Create a var from a state transformer.
mkState :: Monad m
        => (a -> s -> (b, s)) -- ^ state transformer
        -> s -- ^ intial state
        -> VarT m a b
mkState f s = VarT $ \a -> do
  let (b', s') = f a s
  return (b', mkState f s')
--------------------------------------------------------------------------------
-- $composition
-- You can compose vars together using Category's '>>>' and '<<<'. The "right
-- plug" ('>>>') takes the output from a var on the left and "plugs" it into
-- the input of the var on the right. The "left plug" does the same thing in
-- the opposite direction. This allows you to write vars that read
-- naturally.
--------------------------------------------------------------------------------
--------------------------------------------------------------------------------
-- Adjusting and accumulating
--------------------------------------------------------------------------------
-- | Accumulates input values using a folding function and yields
-- that accumulated value each sample. This is analogous to a stepwise foldl.
--
-- >>> testVarOver (accumulate (++) []) $ words "hey there man"
-- "hey"
-- "heythere"
-- "heythereman"
--
-- >>> print $ foldl (++) [] $ words "hey there man"
-- "heythereman"
accumulate :: Monad m => (c -> b -> c) -> c -> VarT m b c
accumulate f b = VarT $ \a -> do
    let b' = f b a
    return (b', accumulate f b')

-- | Delays the given var by one sample using the argument as the first
-- sample.
--
-- >>> testVarOver (delay 0 id) [1,2,3]
-- 0
-- 1
-- 2
--
-- This enables the programmer to create vars that depend on
-- themselves for values. For example:
--
-- >>> let v = delay 0 v + 1 in testVarOver v [1,1,1]
-- 1
-- 2
-- 3
delay :: Monad m => b -> VarT m a b -> VarT m a b
delay b v = VarT $ \a -> return (b, go a v)
    where go a v' = VarT $ \a' -> do (b', v'') <- runVarT v' a
                                     return (b', go a' v'')
--------------------------------------------------------------------------------
-- $running
-- To sample a var simply run it in the desired monad with
-- 'runVarT'. This will produce a sample value and a new var.
--
-- >>> :{
-- do let v0 = accumulate (+) 0
--    (b, v1) <- runVarT v0 1
--    print b
--    (c, v2) <- runVarT v1 b
--    print c
--    (d,  _) <- runVarT v2 c
--    print d
-- >>> :}
-- 1
-- 2
-- 4
--------------------------------------------------------------------------------
-- | Iterate a var over a list of input until all input is consumed,
-- then iterate the var using one single input. Returns the resulting
-- output value and the new var.
--
-- >>> let Identity (outputs, _) = stepMany (accumulate (+) 0) [1,1,1] 1
-- >>> print outputs
-- 4
stepMany :: (Monad m) => VarT m a b -> [a] -> a -> m (b, VarT m a b)
stepMany v [] e     = runVarT v e
stepMany v (e:es) x = snd <$> runVarT v e >>= \v1 -> stepMany v1 es x

-- | Run the var over the input values, gathering the output values in a
-- list.
--
-- >>> let Identity (outputs, _) = scanVar (accumulate (+) 0) [1,1,1,1]
-- >>> print outputs
-- [1,2,3,4]
scanVar :: Monad m => VarT m a b -> [a] -> m ([b], VarT m a b)
scanVar v = foldM f ([], v)
    where f (outs, v') a = do (b, v'') <- runVarT v' a
                              return (outs ++ [b], v'')
--------------------------------------------------------------------------------
-- Testing and debugging
--------------------------------------------------------------------------------
-- | Trace the sample value of a var and pass it along as output. This is
-- very useful for debugging graphs of vars. The (v|vs|vf)trace family of
-- vars use 'Debug.Trace.trace' under the hood, so the value is only traced
-- when evaluated.
--
-- >>> let v = id >>> vtrace
-- >>> testVarOver v [1,2,3]
-- 1
-- 1
-- 2
-- 2
-- 3
-- 3
vtrace :: (Applicative a, Show b) => VarT a b b
vtrace = vstrace ""


-- | Trace the sample value of a var with a prefix and pass the sample along
-- as output. This is very useful for debugging graphs of vars.
--
-- >>> let v = id >>> vstrace "test: "
-- >>> testVarOver v [1,2,3]
-- test: 1
-- 1
-- test: 2
-- 2
-- test: 3
-- 3
vstrace :: (Applicative a, Show b) => String -> VarT a b b
vstrace s = vftrace ((s ++) . show)

-- | Trace the sample value using a custom show-like function. This is useful
-- when you would like to debug a var that uses values that don't have show
-- instances.
--
-- >>> newtype NotShowableInt = NotShowableInt { unNotShowableInt :: Int }
-- >>> let v = id >>> vftrace (("NotShowableInt: " ++) . show . unNotShowableInt)
-- >>> let as = map NotShowableInt [1,1,1]
-- >>> bs <- fst <$> scanVar v as
-- >>> -- We need to do something to evaluate these output values...
-- >>> print $ sum $ map unNotShowableInt bs
-- NotShowableInt: 1
-- NotShowableInt: 1
-- NotShowableInt: 1
-- 3
vftrace :: Applicative a => (b -> String) -> VarT a b b
vftrace f = var $ \b -> trace (f b) b

-- | Run a var in IO over some input, printing the output each step. This is
-- the function we've been using throughout this documentation.
testVarOver :: (Monad m, MonadIO m, Show b)
            => VarT m a b -> [a] -> m ()
testVarOver v xs = fst <$> scanVar v xs >>= mapM_ (liftIO . print)
--------------------------------------------------------------------------------
-- $proofs
-- ==Identity
-- > pure id <*> va = va
--
-- > -- Definition of pure
-- > VarT (\_ -> pure (id, pure id)) <*> v
--
-- > -- Definition of <*>
-- > VarT (\x -> do
-- >   (f, vf') <- runVarT (VarT (\_ -> pure (id, pure id))) x
-- >   (a, va') <- runVarT va x
-- >   pure (f a, vf' <*> va'))
--
-- > -- Newtype
-- > VarT (\x -> do
-- >   (f, vf') <- (\_ -> pure (id, pure id)) x
-- >   (a, va') <- runVarT va x
-- >   pure (f a, vf' <*> va'))
--
-- > -- Application
-- > VarT (\x -> do
-- >   (f, vf') <- pure (id, pure id)
-- >   (a, va') <- runVarT va x
-- >   pure (f a, vf' <*> va'))
--
-- > -- pure x >>= f = f x
-- > VarT (\x -> do
-- >   (a, va') <- runVarT va x
-- >   pure (id a, pure id <*> va'))
--
-- > -- Definition of id
-- > VarT (\x -> do
-- >   (a, va') <- runVarT va x
-- >   pure (a, pure id <*> va'))
--
-- > -- Coinduction
-- > VarT (\x -> do
-- >   (a, va') <- runVarT va x
-- >   pure (a, va'))
--
-- > -- f >>= pure = f
-- > VarT (\x -> runVarT va x)
--
-- > -- Eta reduction
-- > VarT (runVarT va)
--
-- > -- Newtype
-- > va
-- >
--
-- ==Composition
-- > pure (.) <*> u <*> v <*> w = u <*> (v <*> w)
--
-- > -- Definition of pure
-- > VarT (\_ -> pure ((.), pure (.))) <*> u <*> v <*> w
--
-- > -- Definition of <*>
-- > VarT (\x -> do
-- >   (h, t)  <- runVarT (VarT (\_ -> pure ((.), pure (.)))) x
-- >   (f, u') <- runVarT u x
-- >   pure (h f, t <*> u')) <*> v <*> w
--
-- > -- Newtype
-- > VarT (\x -> do
-- >   (h, t)  <- (\_ -> pure ((.), pure (.))) x
-- >   (f, u') <- runVarT u x
-- >   pure (h f, t <*> u')) <*> v <*> w
--
-- > -- Application
-- > VarT (\x -> do
-- >   (h, t)  <- pure ((.), pure (.)))
-- >   (f, u') <- runVarT u x
-- >   pure (h f, t <*> u')) <*> v <*> w
--
-- > -- pure x >>= f = f x
-- > VarT (\x -> do
-- >   (f, u') <- runVarT u x
-- >   pure ((.) f, pure (.) <*> u')) <*> v <*> w
--
-- > -- Definition of <*>
-- > VarT (\x -> do
-- >   (h, t) <-
-- >     runVarT
-- >       (VarT (\y -> do
-- >         (f, u') <- runVarT u y
-- >         pure ((.) f, pure (.) <*> u'))) x
-- >   (g, v') <- runVarT v x
-- >   pure (h g, t <*> v')) <*> w
--
-- > -- Newtype
-- > VarT (\x -> do
-- >   (h, t) <-
-- >     (\y -> do
-- >       (f, u') <- runVarT u y
-- >       pure ((.) f, pure (.) <*> u')) x
-- >   (g, v') <- runVarT v x
-- >   pure (h g, t <*> v')) <*> w
--
-- > -- Application
-- > VarT (\x -> do
-- >   (h, t) <- do
-- >     (f, u') <- runVarT u x
-- >     pure ((.) f, pure (.) <*> u')
-- >   (g, v') <- runVarT v x
-- >   pure (h g, t <*> v')) <*> w
--
-- > -- (f >=> g) >=> h = f >=> (g >=> h)
-- > VarT (\x -> do
-- >   (f, u') <- runVarT u x
-- >   (h, t)  <- pure ((.) f, pure (.) <*> u')
-- >   (g, v') <- runVarT v x
-- >   pure (h g, t <*> v')) <*> w
--
-- > -- pure x >>= f = f x
-- > VarT (\x -> do
-- >   (f, u') <- runVarT u x
-- >   (g, v') <- runVarT v x
-- >   pure ((.) f g, pure (.) <*> u' <*> v')) <*> w
--
-- > -- Definition of <*>
-- > VarT (\x -> do
-- >   (h, t) <-
-- >     runVarT
-- >       (VarT (\y -> do
-- >         (f, u') <- runVarT u y
-- >         (g, v') <- runVarT v y
-- >         pure ((.) f g, pure (.) <*> u' <*> v'))) x
-- >   (a, w') <- runVarT w x
-- >   pure (h a, t <*> w'))
--
-- > -- Newtype
-- > VarT (\x -> do
-- >   (h, t) <-
-- >     (\y -> do
-- >       (f, u') <- runVarT u y
-- >       (g, v') <- runVarT v y
-- >       pure ((.) f g, pure (.) <*> u' <*> v')) x
-- >   (a, w') <- runVarT w x
-- >   pure (h a, t <*> w'))
--
-- > -- Application
-- > VarT (\x -> do
-- >   (h, t) <- do
-- >     (f, u') <- runVarT u x
-- >     (g, v') <- runVarT v x
-- >     pure ((.) f g, pure (.) <*> u' <*> v'))
-- >   (a, w') <- runVarT w x
-- >   pure (h a, t <*> w'))
--
-- > -- (f >=> g) >=> h = f >=> (g >=> h)
-- > VarT (\x -> do
-- >   (f, u') <- runVarT u x
-- >   (g, v') <- runVarT v x
-- >   (h, t)  <- pure ((.) f g, pure (.) <*> u' <*> v'))
-- >   (a, w') <- runVarT w x
-- >   pure (h a, t <*> w'))
--
-- > -- pure x >>= f = f x
-- > VarT (\x -> do
-- >   (f, u') <- runVarT u x
-- >   (g, v') <- runVarT v x
-- >   (a, w') <- runVarT w x
-- >   pure ((.) f g a, pure (.) <*> u' <*> v' <*> w'))
--
-- > -- Definition of .
-- > VarT (\x -> do
-- >   (f, u') <- runVarT u x
-- >   (g, v') <- runVarT v x
-- >   (a, w') <- runVarT w x
-- >   pure (f (g a), pure (.) <*> u' <*> v' <*> w'))
--
-- > -- Coinduction
-- > VarT (\x -> do
-- >   (f, u') <- runVarT u x
-- >   (g, v') <- runVarT v x
-- >   (a, w') <- runVarT w x
-- >   pure (f (g a), u' <*> (v' <*> w')))
--
-- > -- pure x >>= f = f
-- > VarT (\x -> do
-- >   (f, u') <- runVarT u x
-- >   (g, v') <- runVarT v x
-- >   (a, w') <- runVarT w x
-- >   (b, vw) <- pure (g a, v' <*> w')
-- >   pure (f b, u' <*> vw))
--
-- > -- (f >=> g) >=> h = f >=> (g >=> h)
-- > VarT (\x -> do
-- >   (f, u') <- runVarT u x
-- >   (b, vw) <- do
-- >     (g, v') <- runVarT v x
-- >     (a, w') <- runVarT w x
-- >     pure (g a, v' <*> w')
-- >   pure (f b, u' <*> vw))
--
-- > -- Abstraction
-- > VarT (\x -> do
-- >   (f, u') <- runVarT u x
-- >   (b, vw) <-
-- >     (\y -> do
-- >       (g, v') <- runVarT v y
-- >       (a, w') <- runVarT w y)
-- >       pure (g a, v' <*> w')) x
-- >   pure (f b, u' <*> vw))
--
-- > -- Newtype
-- > VarT (\x -> do
-- >   (f, u') <- runVarT u x
-- >   (b, vw) <-
-- >     runVarT
-- >       (VarT (\y -> do
-- >         (g, v') <- runVarT v y
-- >         (a, w') <- runVarT w y)
-- >         pure (g a, v' <*> w')) x
-- >   pure (f b, u' <*> vw))
--
-- > -- Definition of <*>
-- > VarT (\x -> do
-- >   (f, u') <- runVarT u x
-- >   (b, vw) <- runVarT (v <*> w) x
-- >   pure (f b, u' <*> vw))
--
-- > -- Definition of <*>
-- > u <*> (v <*> w)
--
--
-- ==Homomorphism
-- > pure f <*> pure a = pure (f a)
--
-- > -- Definition of pure
-- > VarT (\_ -> pure (f, pure f)) <*> pure a
--
-- > -- Definition of pure
-- > VarT (\_ -> pure (f, pure f)) <*> VarT (\_ -> pure (a, pure a))
--
-- > -- Definition of <*>
-- > VarT (\x -> do
-- >   (f', vf') <- runVarT (VarT (\_ -> pure (f, pure f))) x
-- >   (a', va') <- runVarT (VarT (\_ -> pure (a, pure a))) x
-- >   pure (f' a', vf' <*> va'))
--
-- > -- Newtype
-- > VarT (\x -> do
-- >   (f', vf') <- (\_ -> pure (f, pure f)) x
-- >   (a', va') <- runVarT (VarT (\_ -> pure (a, pure a))) x
-- >   pure (f' a', vf' <*> va'))
--
-- > -- Application
-- > VarT (\x -> do
-- >   (f', vf') <- pure (f, pure f)
-- >   (a', va') <- runVarT (VarT (\_ -> pure (a, pure a))) x
-- >   pure (f' a', vf' <*> va'))
--
-- > -- pure x >>= f = f x
-- > VarT (\x -> do
-- >   (a', va') <- runVarT (VarT (\_ -> pure (a, pure a))) x
-- >   pure (f a', pure f <*> va'))
--
-- > -- Newtype
-- > VarT (\x -> do
-- >   (a', va') <- (\_ -> pure (a, pure a)) x
-- >   pure (f a', pure f <*> va'))
--
-- > -- Application
-- > VarT (\x -> do
-- >   (a', va') <- pure (a, pure a)
-- >   pure (f a', pure f <*> va'))
--
-- > -- pure x >>= f = f x
-- > VarT (\x -> pure (f a, pure f <*> pure a))
--
-- > -- Coinduction
-- > VarT (\x -> pure (f a, pure (f a)))
--
-- > -- Definition of pure
-- > pure (f a)
--
--
-- ==Interchange
-- > u <*> pure y = pure ($ y) <*> u
--
-- > -- Definition of <*>
-- > VarT (\x -> do
-- >   (f, u') <- runVarT u x
-- >   (a, y') <- runVarT (pure y) x
-- >   pure (f a, u' <*> y'))
--
-- > -- Definition of pure
-- > VarT (\x -> do
-- >   (f, u') <- runVarT u x
-- >   (a, y') <- runVarT (VarT (\_ -> pure (y, pure y))) x
-- >   pure (f a, u' <*> y'))
--
-- > -- Newtype
-- > VarT (\x -> do
-- >   (f, u') <- runVarT u x
-- >   (a, y') <- (\_ -> pure (y, pure y)) x
-- >   pure (f a, u' <*> y'))
--
-- > -- Application
-- > VarT (\x -> do
-- >   (f, u') <- runVarT u x
-- >   (a, y') <- pure (y, pure y))
-- >   pure (f a, u' <*> y'))
--
-- > -- pure x >>= f = f
-- > VarT (\x -> do
-- >   (f, u') <- runVarT u x
-- >   pure (f y, u' <*> pure y))
--
-- > -- Coinduction
-- > VarT (\x -> do
-- >   (f, u') <- runVarT u x
-- >   pure (f y, pure ($ y) <*> u'))
--
-- > -- Definition of $
-- > VarT (\x -> do
-- >   (f, u') <- runVarT u x
-- >   pure (($ y) f, pure ($ y) <*> u')
--
-- > -- pure x >>= f = f
-- > VarT (\x -> do
-- >   (g, y') <- pure (($ y), pure ($ y))
-- >   (f, u') <- runVarT u x
-- >   pure (g f, y' <*> u')
--
-- > -- Abstraction
-- > VarT (\x -> do
-- >   (g, y') <- (\_ -> pure (($ y), pure ($ y))) x
-- >   (f, u') <- runVarT u x
-- >   pure (g f, y' <*> u')
--
-- > -- Newtype
-- > VarT (\x -> do
-- >   (g, y') <- runVarT (VarT (\_ -> pure (($ y), pure ($ y)))) x
-- >   (f, u') <- runVarT u x
-- >   pure (g f, y' <*> u')
--
-- > -- Definition of <*>
-- > VarT (\_ -> pure (($ y), pure ($ y))) <*> u
--
-- > -- Definition of pure
-- > pure ($ y) <*> u