{-# LANGUAGE
    ConstraintKinds
  , GADTs
  , TemplateHaskell
  , UndecidableInstances
  , QuantifiedConstraints
  #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Functor.Cofree
-- License     :  BSD-style (see the file LICENSE)
--
-- Maintainer  :  sjoerd@w3future.com
-- Stability   :  experimental
-- Portability :  non-portable
--
-- A cofree functor is right adjoint to a forgetful functor.
-- In this package the forgetful functor forgets class constraints.
-----------------------------------------------------------------------------
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


-- | The cofree functor for constraint @c@.
data Cofree c b where
  Cofree :: c a => (a -> b) -> a -> Cofree c b


-- | Derive the instance of @`Cofree` c a@ for the class @c@.
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 = leftAdjunct id@
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 f = counit . f@
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


-- * Products

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 ())