module Control.Computation (

    -- * Arrows

    module Control.Arrow,

    -- * Computations

    Computation (
        type Unit,
        type Pair,
        type Function,
        type DropResult,
        (###),
        assocLeft,
        assocRight,
        padFst,
        padSnd,
        dropFst,
        dropSnd,
        swap,
        curry,
        apply
    ),
    mapFst,
    mapSnd,
    precomp,
    postcomp,
    uncurry,
    inFst,
    inSnd,
    outFst,
    outSnd,

    -- * Nested pairs

    map1,
    map2,
    map3,
    map4,
    in1,
    in2,
    in3,
    in4,
    out1,
    out2,
    out3,
    out4,
    construct,
    destruct,
    (+:+),
    (-:-),

    -- * Pure computations

    Pure,

    -- * Links between computation types

    Link (type Source, type Target, linkMap, unitInside, pairInside),

    -- * Connected computation types

    Connected (type (==>), type (<==), inject, extract),
    up,
    down

) where

-- Prelude

import           Prelude hiding (id, (.), curry, uncurry)
import qualified Prelude

-- Control

import Control.Category
import Control.Arrow

-- GHC

import GHC.Exts (Constraint)

-- Fixities

infixr 3 ###
infixr 5 +:+
infixr 5 -:-

-- * Computations

class ArrowChoice p => Computation p where

    type Unit p :: *

    type Pair p :: * -> * -> *

    type Function p :: * -> * -> *

    type DropResult p a :: Constraint

    (###) :: (a `p` c) -> (b `p` d) -> (Pair p a b `p` Pair p c d)

    assocLeft :: Pair p a (Pair p b c) `p` Pair p (Pair p a b) c

    assocRight :: Pair p (Pair p a b) c `p` Pair p a (Pair p b c)

    padFst :: a `p` (Pair p (Unit p) a)

    padSnd :: a `p` (Pair p a (Unit p))

    dropFst :: DropResult p a => Pair p (Unit p) a `p` a

    dropSnd :: DropResult p a => Pair p a (Unit p) `p` a

    swap :: Pair p a b `p` Pair p b a

    curry :: Pair p a b `p` c -> a `p` Function p b c

    apply :: Pair p (Function p a b) a `p` b

{-FIXME:
    We do not have a curry operator for (->). This decision was first made for
    simplicity.

    However, it has a more important justification. We cannot implement a curry
    operator for (->) in the case of Resourceful. A morphism of type α ~> β is a
    natural transformation of type ∀ R . α R → β R, if we mean ∀ to stand for
    natural transformation. A value of type α -> β inside the Resourceful
    category is also of such a type. More precisely, a value of type α -> β for
    a resource type R is of type ∀ Q . α Q → β Q, and so its type is independent
    of R. Application (realized by arr apply) is still possible with this.
    However, currying is not, as it would have to have the following type:

        (∀ R . α R × β R → γ R) → (∀ R . α R → (∀ Q . β Q → γ Q))

    This is not possible. If (->) inside Resourceful would properly correspond
    to an end, then we could turn a (α → β) R into an (α → β) Q for every
    r : Q → R by using A r, but with ∀ Q, we would have to transform also to such
    (α → β) Q where there is no r : Q → R.

    What structure do we still have for (->)? Is (->) even a contravariant and
    covariant functor? In any case, we have distributivity, since we can
    generate the canonical distributivity transformations from the corresponding
    transformations for (->) via arr. Are these so-gained transformations correct?
-}
{-FIXME:
    Consider adding rules for the Computation class, like it is done for the
    Arrow class. To make the rules actually fire, we have to make this module
    Trustworthy.
-}

mapFst :: Computation p => a `p` b -> Pair p a c `p` Pair p b c
mapFst comp1 = comp1 ### id

mapSnd :: Computation p => b `p` c -> Pair p a b `p` Pair p a c
mapSnd comp2 = id ### comp2

precomp :: Computation p => a `p` b -> Function p b c `p` Function p a c
precomp comp = curry (mapSnd comp >>> apply)

postcomp :: Computation p => b `p` c -> Function p a b `p` Function p a c
postcomp comp = curry (apply >>> comp)

uncurry :: Computation p => a `p` Function p b c -> Pair p a b `p` c
uncurry comp = mapFst comp >>> apply

inFst :: Computation p => a `p` Function p b c -> Pair p a b `p` c
inFst comp = uncurry comp

inSnd :: Computation p => b `p` Function p a c -> Pair p a b `p` c
inSnd comp = swap >>> uncurry comp

outFst :: Computation p => Pair p a b `p` c -> a `p` Function p b c
outFst comp = curry comp

outSnd :: Computation p => Pair p a b `p` c -> b `p` Function p a c
outSnd comp = curry (swap >>> comp)

-- * Nested pairs

map1 :: Computation p
     => a `p` b
     -> Pair p a t `p` Pair p b t
map1 = mapFst

map2 :: Computation p
     => b `p` c
     -> Pair p a (Pair p b t) `p` Pair p a (Pair p c t)
map2 = mapSnd . mapFst

map3 :: Computation p
     => c `p` d
     -> Pair p a (Pair p b (Pair p c t)) `p` Pair p a (Pair p b (Pair p d t))
map3 = mapSnd . mapSnd . mapFst

map4 :: Computation p
     => d `p` e
     -> Pair p a (Pair p b (Pair p c (Pair p d t))) `p`
        Pair p a (Pair p b (Pair p c (Pair p e t)))
map4 = mapSnd . mapSnd . mapSnd . mapFst

in1 :: Computation p
    => a `p` Function p t r
    -> Pair p a t `p` r
in1 = inFst

in2 :: Computation p
    => b `p` Function p t (Function p a r)
    -> Pair p a (Pair p b t) `p` r
in2 = inSnd . inFst

in3 :: Computation p
    => c `p` Function p t (Function p b (Function p a r))
    -> Pair p a (Pair p b (Pair p c t)) `p` r
in3 = inSnd . inSnd . inFst

in4 :: Computation p
    => d `p` Function p t (Function p c (Function p b (Function p a r)))
    -> Pair p a (Pair p b (Pair p c (Pair p d t))) `p` r
in4 = inSnd . inSnd . inSnd . inFst

out1 :: Computation p
     => Pair p a t `p` r
     -> a `p` Function p t r
out1 = outFst

out2 :: Computation p
     => Pair p a (Pair p b t) `p` r
     -> b `p` Function p t (Function p a r)
out2 = outFst . outSnd

out3 :: Computation p
     => Pair p a (Pair p b (Pair p c t)) `p` r
     -> c `p` Function p t (Function p b (Function p a r))
out3 = outFst . outSnd . outSnd

out4 :: Computation p
     => Pair p a (Pair p b (Pair p c (Pair p d t))) `p` r
     -> d `p` Function p t (Function p c (Function p b (Function p a r)))
out4 = outFst . outSnd . outSnd . outSnd

construct :: Computation p => (Unit p `p` a) -> (b `p` Pair p a b)
construct constructor = padFst >>> mapFst constructor

destruct :: (Computation p, DropResult p b)
         => (a `p` Unit p)
         -> (Pair p a b `p` b)
destruct destructor = mapFst destructor >>> dropFst

(+:+) :: Computation p => (Unit p `p` a) -> (b `p` t) -> (b `p` Pair p a t)
constructor +:+ comp = comp >>> construct constructor

(-:-) :: (Computation p, DropResult p t)
      => (a `p` Unit p)
      -> (t `p` b)
      -> (Pair p a t `p` b)
destructor -:- comp = destruct destructor >>> comp

-- * Pure computations

type Pure = (->)

instance Computation Pure where

    type Unit Pure = ()

    type Pair Pure = (,)

    type Function Pure = (->)

    type DropResult Pure a = ()

    (###) = (***)

    assocLeft ~(val1, ~(val2, val3)) = ((val1, val2), val3)

    assocRight ~(~(val1, val2), val3) = (val1, (val2, val3))

    padFst val = ((), val)

    padSnd val = (val, ())

    dropFst ~(_, val) = val

    dropSnd ~(val, _) = val

    swap ~(val1, val2) = (val2, val1)

    curry = Prelude.curry

    apply = Prelude.uncurry ($)

-- * Links between computation types

class (Computation (Source l), Computation (Target l)) => Link l where

    type Source l :: * -> * -> *

    type Target l :: * -> * -> *

    linkMap :: Source l a b -> Target l (l a) (l b)

    unitInside :: Target l (Unit (Target l))
                           (l (Unit (Source l)))

    pairInside :: Target l (Pair (Target l) (l a) (l b))
                           (l (Pair (Source l) a b))

-- * Connected computation types

{-NOTE:

    For the temporal case, we not only need a subclass of Computation, but also
    subclasses of Connected and Link. The one for Connected, would probably
    differ only from Connected by additional constraints of (==>) and (<==)
    being instances of the temporal Link class, and by informally stated
    additional laws that describe the interaction between processes and the
    adjunction.
-}

class (Link (p ==> q), Source (p ==> q) ~ p, Target (p ==> q) ~ q,
       Link (p <== q), Source (p <== q) ~ q, Target (p <== q) ~ p) =>
      Connected p q where

    data p ==> q :: * -> *

    data p <== q :: * -> *

    inject :: a `p` (p <== q) ((p ==> q) a)

    extract :: (p ==> q) ((p <== q) b) `q` b

up :: Connected p q => a `p` (p <== q) b -> (p ==> q) a `q` b
up comp1 = linkMap comp1 >>> extract

down :: Connected p q => (p ==> q) a `q` b -> a `p` (p <== q) b
down comp2 = inject >>> linkMap comp2

instance Computation p => Connected p p where

    newtype (p ==> p) a = SelfUp { unSelfUp :: a }

    newtype (p <== p) a = SelfDown { unSelfDown :: a }

    inject = arr (SelfUp >>> SelfDown)

    extract = arr (unSelfUp >>> unSelfDown)

instance Computation p => Link (p ==> p) where

    type Source (p ==> p) = p

    type Target (p ==> p) = p

    linkMap comp = arr unSelfUp >>> comp >>> arr SelfUp

    unitInside = arr SelfUp

    pairInside = arr unSelfUp ### arr unSelfUp >>> arr SelfUp

instance Computation p => Link (p <== p) where

    type Source (p <== p) = p

    type Target (p <== p) = p

    linkMap comp = arr unSelfDown >>> comp >>> arr SelfDown

    unitInside = arr SelfDown

    pairInside = arr unSelfDown ### arr unSelfDown >>> arr SelfDown