{-# LANGUAGE LinearTypes #-}
module Proarrow.Category.Instance.Linear where

import Data.Kind (Type)
import Data.Void (Void)
import Prelude (Either(..))

import Proarrow.Core (UN, Is, CAT, Profunctor (..), dimapDefault, Promonad (..), CategoryOf(..), PRO)
import Proarrow.Category.Monoidal (Monoidal(..), SymMonoidal (..), MonoidalProfunctor (..))
import Proarrow.Profunctor.Corepresentable (Corepresentable(..))
import Proarrow.Adjunction (Adjunction(..))
import Proarrow.Profunctor.Composition ((:.:)(..))
import Proarrow.Object.Exponential (Closed(..))
import Proarrow.Object.BinaryCoproduct (HasBinaryCoproducts(..))
import Proarrow.Object.Initial (HasInitialObject(..))
import Proarrow.Functor (Functor(..))


type data LINEAR = L Type
type instance UN L (L a) = a

type Linear :: CAT LINEAR
data Linear a b where
  Linear :: (a %1 -> b) -> Linear (L a) (L b)

instance Profunctor Linear where
  dimap :: forall (c :: LINEAR) (a :: LINEAR) (b :: LINEAR) (d :: LINEAR).
(c ~> a) -> (b ~> d) -> Linear a b -> Linear c d
dimap = (c ~> a) -> (b ~> d) -> Linear a b -> Linear c d
Linear c a -> Linear b d -> Linear a b -> Linear c d
forall {k} (p :: PRO k k) (c :: k) (a :: k) (b :: k) (d :: k).
Promonad p =>
p c a -> p b d -> p a b -> p c d
dimapDefault
  (Ob a, Ob b) => r
r \\ :: forall (a :: LINEAR) (b :: LINEAR) r.
((Ob a, Ob b) => r) -> Linear a b -> r
\\ Linear{} = r
(Ob a, Ob b) => r
r
instance Promonad Linear where
  id :: forall (a :: LINEAR). Ob a => Linear a a
id = (UN L a %1 -> UN L a) -> Linear (L (UN L a)) (L (UN L a))
forall b b. (b %1 -> b) -> Linear (L b) (L b)
Linear \UN L a
x -> UN L a
x
  Linear a %1 -> b
f . :: forall (b :: LINEAR) (c :: LINEAR) (a :: LINEAR).
Linear b c -> Linear a b -> Linear a c
. Linear a %1 -> b
g = (a %1 -> b) -> Linear (L a) (L b)
forall b b. (b %1 -> b) -> Linear (L b) (L b)
Linear \a
x -> a %1 -> b
f (a %1 -> b
g a
x)
-- | Category of linear functions.
instance CategoryOf LINEAR where
  type (~>) = Linear
  type Ob (a :: LINEAR) = Is L a

instance Monoidal LINEAR where
  type Unit = L ()
  type L a ** L b = L (a, b)
  Linear a %1 -> b
f par :: forall (a :: LINEAR) (b :: LINEAR) (c :: LINEAR) (d :: LINEAR).
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
`par` Linear a %1 -> b
g = ((a, a) %1 -> (b, b)) -> Linear (L (a, a)) (L (b, b))
forall b b. (b %1 -> b) -> Linear (L b) (L b)
Linear \(a
x, a
y) -> (a %1 -> b
f a
x, a %1 -> b
g a
y)
  leftUnitor :: forall (a :: LINEAR). Obj a -> (Unit ** a) ~> a
leftUnitor (Linear a %1 -> b
f) = (((), a) %1 -> b) -> Linear (L ((), a)) (L b)
forall b b. (b %1 -> b) -> Linear (L b) (L b)
Linear \((), a
x) -> a %1 -> b
f a
x
  leftUnitorInv :: forall (a :: LINEAR). Obj a -> a ~> (Unit ** a)
leftUnitorInv (Linear a %1 -> b
f) = (a %1 -> ((), b)) -> Linear (L a) (L ((), b))
forall b b. (b %1 -> b) -> Linear (L b) (L b)
Linear \a
x -> ((), a %1 -> b
f a
x)
  rightUnitor :: forall (a :: LINEAR). Obj a -> (a ** Unit) ~> a
rightUnitor (Linear a %1 -> b
f) = ((a, ()) %1 -> b) -> Linear (L (a, ())) (L b)
forall b b. (b %1 -> b) -> Linear (L b) (L b)
Linear \(a
x, ()) -> a %1 -> b
f a
x
  rightUnitorInv :: forall (a :: LINEAR). Obj a -> a ~> (a ** Unit)
rightUnitorInv (Linear a %1 -> b
f) = (a %1 -> (b, ())) -> Linear (L a) (L (b, ()))
forall b b. (b %1 -> b) -> Linear (L b) (L b)
Linear \a
x -> (a %1 -> b
f a
x, ())
  associator :: forall (a :: LINEAR) (b :: LINEAR) (c :: LINEAR).
Obj a -> Obj b -> Obj c -> ((a ** b) ** c) ~> (a ** (b ** c))
associator Linear{} Linear{} Linear{} = (((b, b), b) %1 -> (b, (b, b)))
-> Linear (L ((b, b), b)) (L (b, (b, b)))
forall b b. (b %1 -> b) -> Linear (L b) (L b)
Linear \((b
x, b
y), b
z) -> (b
x, (b
y, b
z))
  associatorInv :: forall (a :: LINEAR) (b :: LINEAR) (c :: LINEAR).
Obj a -> Obj b -> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv Linear{} Linear{} Linear{} = ((b, (b, b)) %1 -> ((b, b), b))
-> Linear (L (b, (b, b))) (L ((b, b), b))
forall b b. (b %1 -> b) -> Linear (L b) (L b)
Linear \(b
x, (b
y, b
z)) -> ((b
x, b
y), b
z)

instance SymMonoidal LINEAR where
  swap' :: forall (a :: LINEAR) (b :: LINEAR).
Obj a -> Obj b -> (a ** b) ~> (b ** a)
swap' Linear{} Linear{} = ((b, b) %1 -> (b, b)) -> Linear (L (b, b)) (L (b, b))
forall b b. (b %1 -> b) -> Linear (L b) (L b)
Linear \(b
x, b
y) -> (b
y, b
x)

instance Closed LINEAR where
  type a ~~> b = L (UN L a %1 -> UN L b)
  curry' :: forall (a :: LINEAR) (b :: LINEAR) (c :: LINEAR).
Obj a -> Obj b -> ((a ** b) ~> c) -> a ~> (b ~~> c)
curry' Linear{} Linear{} (Linear a %1 -> b
f) = (b %1 -> b %1 -> b) -> Linear (L b) (L (b %1 -> b))
forall b b. (b %1 -> b) -> Linear (L b) (L b)
Linear \b
a b
b -> a %1 -> b
f (b
a, b
b)
  uncurry' :: forall (b :: LINEAR) (c :: LINEAR) (a :: LINEAR).
Obj b -> Obj c -> (a ~> (b ~~> c)) -> (a ** b) ~> c
uncurry' Linear{} Linear{} (Linear a %1 -> b
f) = ((a, b) %1 -> b) -> Linear (L (a, b)) (L b)
forall b b. (b %1 -> b) -> Linear (L b) (L b)
Linear \(a
a, b
b) -> a %1 -> b
f a
a b
b
  Linear a %1 -> b
f ^^^ :: forall (b :: LINEAR) (y :: LINEAR) (x :: LINEAR) (a :: LINEAR).
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
^^^ Linear a %1 -> b
g = ((b %1 -> a) %1 -> a %1 -> b)
-> Linear (L (b %1 -> a)) (L (a %1 -> b))
forall b b. (b %1 -> b) -> Linear (L b) (L b)
Linear \b %1 -> a
h a
x -> a %1 -> b
f (b %1 -> a
h (a %1 -> b
g a
x))


type Forget :: PRO LINEAR Type
data Forget a b where
  Forget :: (a -> b) -> Forget (L a) b
instance Profunctor Forget where
  dimap :: forall (c :: LINEAR) (a :: LINEAR) b d.
(c ~> a) -> (b ~> d) -> Forget a b -> Forget c d
dimap (Linear a %1 -> b
f) b ~> d
g (Forget a -> b
h) = (a -> d) -> Forget (L a) d
forall b b. (b -> b) -> Forget (L b) b
Forget \a
x -> b ~> d
b -> d
g (a -> b
h (a %1 -> b
f a
x))
  (Ob a, Ob b) => r
r \\ :: forall (a :: LINEAR) b r. ((Ob a, Ob b) => r) -> Forget a b -> r
\\ Forget{} = r
(Ob a, Ob b) => r
r
instance Corepresentable Forget where
  type Forget %% a = UN L a
  coindex :: forall (a :: LINEAR) b. Forget a b -> (Forget %% a) ~> b
coindex (Forget a -> b
f) = (Forget %% a) ~> b
a -> b
f
  cotabulate :: forall (a :: LINEAR) b. Ob a => ((Forget %% a) ~> b) -> Forget a b
cotabulate = ((Forget %% a) ~> b) -> Forget a b
(UN L a -> b) -> Forget (L (UN L a)) b
forall b b. (b -> b) -> Forget (L b) b
Forget
  corepMap :: forall (a :: LINEAR) (b :: LINEAR).
(a ~> b) -> (Forget %% a) ~> (Forget %% b)
corepMap (Linear a %1 -> b
f) UN L a
x = a %1 -> b
f a
UN L a
x
instance MonoidalProfunctor Forget where
  lift0 :: Forget Unit Unit
lift0 = (() -> ()) -> Forget (L ()) ()
forall b b. (b -> b) -> Forget (L b) b
Forget \() -> ()
  lift2 :: forall (x1 :: LINEAR) x2 (y1 :: LINEAR) y2.
Forget x1 x2 -> Forget y1 y2 -> Forget (x1 ** y1) (x2 ** y2)
lift2 (Forget a -> x2
f) (Forget a -> y2
g) = ((a, a) -> (x2, y2)) -> Forget (L (a, a)) (x2, y2)
forall b b. (b -> b) -> Forget (L b) b
Forget \(a
x, a
y) -> (a -> x2
f a
x, a -> y2
g a
y)


data Ur a where
  Ur :: a -> Ur a

unur :: Ur a %1 -> a
unur :: forall a. Ur a %1 -> a
unur (Ur a
a) = a
a

instance Functor Ur where
  map :: forall a b. (a ~> b) -> Ur a ~> Ur b
map a ~> b
f (Ur a
a) = b -> Ur b
forall a. a -> Ur a
Ur (a ~> b
a -> b
f a
a)

type Free :: PRO Type LINEAR
data Free a b where
  Free :: (Ur a %1 -> b) -> Free a (L b)
instance Profunctor Free where
  dimap :: forall c a (b :: LINEAR) (d :: LINEAR).
(c ~> a) -> (b ~> d) -> Free a b -> Free c d
dimap c ~> a
f (Linear a %1 -> b
g) (Free Ur a %1 -> b
h) = (Ur c %1 -> b) -> Free c (L b)
forall a b. (Ur a %1 -> b) -> Free a (L b)
Free \(Ur c
x) -> a %1 -> b
g (Ur a %1 -> b
h (a -> Ur a
forall a. a -> Ur a
Ur (c ~> a
c -> a
f c
x)))
  (Ob a, Ob b) => r
r \\ :: forall a (b :: LINEAR) r. ((Ob a, Ob b) => r) -> Free a b -> r
\\ Free{} = r
(Ob a, Ob b) => r
r
instance Corepresentable Free where
  type Free %% a = L (Ur a)
  coindex :: forall a (b :: LINEAR). Free a b -> (Free %% a) ~> b
coindex (Free Ur a %1 -> b
f) = (Ur a %1 -> b) -> Linear (L (Ur a)) (L b)
forall b b. (b %1 -> b) -> Linear (L b) (L b)
Linear Ur a %1 -> b
f
  cotabulate :: forall a (b :: LINEAR). Ob a => ((Free %% a) ~> b) -> Free a b
cotabulate (Linear a %1 -> b
f) = (Ur a %1 -> b) -> Free a (L b)
forall a b. (Ur a %1 -> b) -> Free a (L b)
Free a %1 -> b
Ur a %1 -> b
f
  corepMap :: forall a b. (a ~> b) -> (Free %% a) ~> (Free %% b)
corepMap a ~> b
f = (Ur a %1 -> Ur b) -> Linear (L (Ur a)) (L (Ur b))
forall b b. (b %1 -> b) -> Linear (L b) (L b)
Linear \(Ur a
a) -> b -> Ur b
forall a. a -> Ur a
Ur (a ~> b
a -> b
f a
a)
instance MonoidalProfunctor Free where
  lift0 :: Free Unit Unit
lift0 = (Ur () %1 -> ()) -> Free () (L ())
forall a b. (Ur a %1 -> b) -> Free a (L b)
Free \(Ur ()) -> ()
  lift2 :: forall x1 (x2 :: LINEAR) y1 (y2 :: LINEAR).
Free x1 x2 -> Free y1 y2 -> Free (x1 ** y1) (x2 ** y2)
lift2 (Free Ur x1 %1 -> b
f) (Free Ur y1 %1 -> b
g) = (Ur (x1, y1) %1 -> (b, b)) -> Free (x1, y1) (L (b, b))
forall a b. (Ur a %1 -> b) -> Free a (L b)
Free \(Ur (x1
x, y1
y)) -> (Ur x1 %1 -> b
f (x1 -> Ur x1
forall a. a -> Ur a
Ur x1
x), Ur y1 %1 -> b
g (y1 -> Ur y1
forall a. a -> Ur a
Ur y1
y))

unlift2Free :: Free %% (x ** y) ~> (Free %% x) ** (Free %% y)
unlift2Free :: forall x y. (Free %% (x ** y)) ~> ((Free %% x) ** (Free %% y))
unlift2Free = (Ur (x, y) %1 -> (Ur x, Ur y))
-> Linear (L (Ur (x, y))) (L (Ur x, Ur y))
forall b b. (b %1 -> b) -> Linear (L b) (L b)
Linear \(Ur (x
x, y
y)) -> (x -> Ur x
forall a. a -> Ur a
Ur x
x, y -> Ur y
forall a. a -> Ur a
Ur y
y)

unlift2Forget :: (Ob x, Ob y) => Forget %% (x ** y) ~> (Forget %% x) ** (Forget %% y)
unlift2Forget :: forall (x :: LINEAR) (y :: LINEAR).
(Ob x, Ob y) =>
(Forget %% (x ** y)) ~> ((Forget %% x) ** (Forget %% y))
unlift2Forget = (Forget %% (x ** y)) ~> ((Forget %% x) ** (Forget %% y))
(UN L x, UN L y) -> (UN L x, UN L y)
forall a. Ob a => a -> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id


instance Adjunction Free Forget where
  unit :: forall (a :: LINEAR). Ob a => (:.:) Forget Free a a
unit = (UN L a -> UN L a) -> Forget (L (UN L a)) (UN L a)
forall b b. (b -> b) -> Forget (L b) b
Forget UN L a -> UN L a
forall a. Ob a => a -> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id Forget a (UN L a) -> Free (UN L a) a -> (:.:) Forget Free a a
forall {i} {j} {k} (p :: PRO i j) (a :: i) (b :: j) (q :: PRO j k)
       (c :: k).
p a b -> q b c -> (:.:) p q a c
:.: (Ur (UN L a) %1 -> UN L a) -> Free (UN L a) (L (UN L a))
forall a b. (Ur a %1 -> b) -> Free a (L b)
Free Ur (UN L a) %1 -> UN L a
forall a. Ur a %1 -> a
unur
  counit :: (Free :.: Forget) :~> (~>)
counit (Free Ur a %1 -> b
f :.: Forget a -> b
g) a
a = a -> b
g (Ur a %1 -> b
f (a -> Ur a
forall a. a -> Ur a
Ur a
a))


instance HasBinaryCoproducts LINEAR where
  type L a || L b = L (Either a b)
  lft' :: forall (a :: LINEAR) (b :: LINEAR). Obj a -> Obj b -> a ~> (a || b)
lft' Linear{} Linear{} = (b %1 -> Either b b) -> Linear (L b) (L (Either b b))
forall b b. (b %1 -> b) -> Linear (L b) (L b)
Linear b -> Either b b
forall a b. a -> Either a b
Left
  rgt' :: forall (a :: LINEAR) (b :: LINEAR). Obj a -> Obj b -> b ~> (a || b)
rgt' Linear{} Linear{} = (b %1 -> Either b b) -> Linear (L b) (L (Either b b))
forall b b. (b %1 -> b) -> Linear (L b) (L b)
Linear b -> Either b b
forall a b. b -> Either a b
Right
  Linear a %1 -> b
f ||| :: forall (x :: LINEAR) (a :: LINEAR) (y :: LINEAR).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| Linear a %1 -> b
g = (Either a a %1 -> b) -> Linear (L (Either a a)) (L b)
forall b b. (b %1 -> b) -> Linear (L b) (L b)
Linear \case
    Left a
x -> a %1 -> b
f a
x
    Right a
y -> a %1 -> b
g a
y

instance HasInitialObject LINEAR where
  type InitialObject = L Void
  initiate' :: forall (a :: LINEAR). Obj a -> InitialObject ~> a
initiate' Linear{} = (Void %1 -> b) -> Linear (L Void) (L b)
forall b b. (b %1 -> b) -> Linear (L b) (L b)
Linear Void %1 -> b
\case