{-# LANGUAGE
ConstraintKinds
, GADTs
, TemplateHaskell
, UndecidableInstances
, QuantifiedConstraints
#-}
module Data.Functor.Cofree where
import Control.Monad
import Control.Comonad
import Data.Functor.Identity
import Data.Functor.Compose
import Language.Haskell.TH.Syntax
import Data.Functor.Cofree.Internal
data Cofree c b where
Cofree :: c a => (a -> b) -> a -> Cofree c b
deriveCofreeInstance :: Name -> Q [Dec]
deriveCofreeInstance :: Name -> Q [Dec]
deriveCofreeInstance = Name -> Name -> Name -> Q [Dec]
deriveCofreeInstance' ''Cofree 'Cofree
counit :: Cofree c b -> b
counit :: forall (c :: * -> Constraint) b. Cofree c b -> b
counit (Cofree a -> b
k a
a) = a -> b
k a
a
leftAdjunct :: c a => (a -> b) -> a -> Cofree c b
leftAdjunct :: forall (c :: * -> Constraint) a b.
c a =>
(a -> b) -> a -> Cofree c b
leftAdjunct = (a -> b) -> a -> Cofree c b
forall (c :: * -> Constraint) a b.
c a =>
(a -> b) -> a -> Cofree c b
Cofree
unit :: c b => b -> Cofree c b
unit :: forall (c :: * -> Constraint) b. c b => b -> Cofree c b
unit = (b -> b) -> b -> Cofree c b
forall (c :: * -> Constraint) a b.
c a =>
(a -> b) -> a -> Cofree c b
leftAdjunct b -> b
forall a. a -> a
id
rightAdjunct :: (a -> Cofree c b) -> a -> b
rightAdjunct :: forall a (c :: * -> Constraint) b. (a -> Cofree c b) -> a -> b
rightAdjunct a -> Cofree c b
f = Cofree c b -> b
forall (c :: * -> Constraint) b. Cofree c b -> b
counit (Cofree c b -> b) -> (a -> Cofree c b) -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Cofree c b
f
instance Functor (Cofree c) where
fmap :: forall a b. (a -> b) -> Cofree c a -> Cofree c b
fmap a -> b
f (Cofree a -> a
k a
a) = (a -> b) -> a -> Cofree c b
forall (c :: * -> Constraint) a b.
c a =>
(a -> b) -> a -> Cofree c b
Cofree (a -> b
f (a -> b) -> (a -> a) -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> a
k) a
a
instance Comonad (Cofree c) where
extract :: forall a. Cofree c a -> a
extract = Cofree c a -> a
forall (c :: * -> Constraint) b. Cofree c b -> b
counit
duplicate :: forall a. Cofree c a -> Cofree c (Cofree c a)
duplicate (Cofree a -> a
k a
a) = (a -> Cofree c a) -> a -> Cofree c (Cofree c a)
forall (c :: * -> Constraint) a b.
c a =>
(a -> b) -> a -> Cofree c b
Cofree ((a -> a) -> a -> Cofree c a
forall (c :: * -> Constraint) a b.
c a =>
(a -> b) -> a -> Cofree c b
leftAdjunct a -> a
k) a
a
instance (forall x. c (Identity x), forall x. c (Compose (Cofree c) (Cofree c) x))
=> Applicative (Cofree c) where
pure :: forall a. a -> Cofree c a
pure = (Identity a -> a) -> Identity a -> Cofree c a
forall (c :: * -> Constraint) a b.
c a =>
(a -> b) -> a -> Cofree c b
leftAdjunct Identity a -> a
forall a. Identity a -> a
runIdentity (Identity a -> Cofree c a) -> (a -> Identity a) -> a -> Cofree c a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Identity a
forall a. a -> Identity a
Identity
<*> :: forall a b. Cofree c (a -> b) -> Cofree c a -> Cofree c b
(<*>) = Cofree c (a -> b) -> Cofree c a -> Cofree c b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap
instance (forall x. c (Identity x), forall x. c (Compose (Cofree c) (Cofree c) x))
=> Monad (Cofree c) where
return :: forall a. a -> Cofree c a
return = a -> Cofree c a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
Cofree c a
m >>= :: forall a b. Cofree c a -> (a -> Cofree c b) -> Cofree c b
>>= a -> Cofree c b
g = (Compose (Cofree c) (Cofree c) b -> b)
-> Compose (Cofree c) (Cofree c) b -> Cofree c b
forall (c :: * -> Constraint) a b.
c a =>
(a -> b) -> a -> Cofree c b
leftAdjunct (Cofree c b -> b
forall (w :: * -> *) a. Comonad w => w a -> a
extract (Cofree c b -> b)
-> (Compose (Cofree c) (Cofree c) b -> Cofree c b)
-> Compose (Cofree c) (Cofree c) b
-> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Cofree c (Cofree c b) -> Cofree c b
forall (w :: * -> *) a. Comonad w => w a -> a
extract (Cofree c (Cofree c b) -> Cofree c b)
-> (Compose (Cofree c) (Cofree c) b -> Cofree c (Cofree c b))
-> Compose (Cofree c) (Cofree c) b
-> Cofree c b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Compose (Cofree c) (Cofree c) b -> Cofree c (Cofree c b)
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose) (Cofree c (Cofree c b) -> Compose (Cofree c) (Cofree c) b
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (Cofree c (Cofree c b) -> Compose (Cofree c) (Cofree c) b)
-> Cofree c (Cofree c b) -> Compose (Cofree c) (Cofree c) b
forall a b. (a -> b) -> a -> b
$ (a -> Cofree c b) -> Cofree c a -> Cofree c (Cofree c b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Cofree c b
g Cofree c a
m)
convert :: (c (w a), Comonad w) => w a -> Cofree c a
convert :: forall (c :: * -> Constraint) (w :: * -> *) a.
(c (w a), Comonad w) =>
w a -> Cofree c a
convert = (w a -> a) -> w a -> Cofree c a
forall (c :: * -> Constraint) a b.
c a =>
(a -> b) -> a -> Cofree c b
leftAdjunct w a -> a
forall (w :: * -> *) a. Comonad w => w a -> a
extract
type Product c m n = Cofree c (m, n)
product :: c a => (a -> m) -> (a -> n) -> a -> Product c m n
product :: forall (c :: * -> Constraint) a m n.
c a =>
(a -> m) -> (a -> n) -> a -> Product c m n
product a -> m
m a -> n
n = (a -> (m, n)) -> a -> Cofree c (m, n)
forall (c :: * -> Constraint) a b.
c a =>
(a -> b) -> a -> Cofree c b
leftAdjunct (\a
a -> (a -> m
m a
a, a -> n
n a
a))
outL :: Product c m n -> m
outL :: forall (c :: * -> Constraint) m n. Product c m n -> m
outL = (m, n) -> m
forall a b. (a, b) -> a
fst ((m, n) -> m)
-> (Cofree c (m, n) -> (m, n)) -> Cofree c (m, n) -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Cofree c (m, n) -> (m, n)
forall (c :: * -> Constraint) b. Cofree c b -> b
counit
outR :: Product c m n -> n
outR :: forall (c :: * -> Constraint) m n. Product c m n -> n
outR = (m, n) -> n
forall a b. (a, b) -> b
snd ((m, n) -> n)
-> (Cofree c (m, n) -> (m, n)) -> Cofree c (m, n) -> n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Cofree c (m, n) -> (m, n)
forall (c :: * -> Constraint) b. Cofree c b -> b
counit
type TerminalObject c = Cofree c ()
terminal :: c a => a -> TerminalObject c
terminal :: forall (c :: * -> Constraint) a. c a => a -> TerminalObject c
terminal = (a -> ()) -> a -> Cofree c ()
forall (c :: * -> Constraint) a b.
c a =>
(a -> b) -> a -> Cofree c b
leftAdjunct (() -> a -> ()
forall a b. a -> b -> a
const ())