{-# 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)
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