{-# LANGUAGE LinearTypes #-}

module Proarrow.Category.Instance.Linear where

import Data.IORef (newIORef, readIORef, writeIORef)
import Data.Kind (Type)
import Data.Void (Void)
import Prelude (Either (..), undefined)

import Proarrow.Adjunction (Adjunction (..))
import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal (..))
import Proarrow.Category.Monoidal.Action (Costrong (..))
import Proarrow.Core (CAT, CategoryOf (..), Is, Profunctor (..), Promonad (..), UN, dimapDefault, type (+->))
import Proarrow.Functor (Functor (..))
import Proarrow.Monoid (Comonoid (..))
import Proarrow.Object.BinaryCoproduct (COPROD, Coprod (..), HasBinaryCoproducts (..))
import Proarrow.Object.BinaryProduct (HasBinaryProducts (..))
import Proarrow.Object.Copower (Copowered (..))
import Proarrow.Object.Dual (StarAutonomous (..))
import Proarrow.Object.Exponential (Closed (..))
import Proarrow.Object.Initial (HasInitialObject (..))
import Proarrow.Object.Power (Powered (..))
import Proarrow.Object.Terminal (HasTerminalObject (..))
import Proarrow.Profunctor.Composition ((:.:) (..))
import Proarrow.Profunctor.Identity (Id (..))
import Proarrow.Profunctor.Representable (RepCostar (..), Representable (..), dimapRep)
import System.IO.Unsafe (unsafeDupablePerformIO)
import Unsafe.Coerce (unsafeCoerce)

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

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

unLinear :: (L a ~> L b) %1 -> (a %1 -> b)
unLinear :: forall a b. ('L a ~> 'L b) %1 -> a %1 -> b
unLinear (Linear a %1 -> b
f) = a %1 -> b
a %1 -> b
f

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 :: 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 a b. (a %1 -> b) -> Linear ('L a) ('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 a b. (a %1 -> b) -> Linear ('L a) ('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 MonoidalProfunctor Linear where
  par0 :: Linear Unit Unit
par0 = Linear Unit Unit
Linear ('L ()) ('L ())
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: LINEAR). Ob a => Linear a a
id
  Linear a %1 -> b
f par :: forall (x1 :: LINEAR) (x2 :: LINEAR) (y1 :: LINEAR) (y2 :: LINEAR).
Linear x1 x2 -> Linear y1 y2 -> Linear (x1 ** y1) (x2 ** y2)
`par` Linear a %1 -> b
g = ((a, a) %1 -> (b, b)) -> Linear ('L (a, a)) ('L (b, b))
forall a b. (a %1 -> b) -> Linear ('L a) ('L b)
Linear \(a
x, a
y) -> (a %1 -> b
f a
x, a %1 -> b
g a
y)

-- | Tuples as monoidal tensor. Note that tuples are not the binary product in LINEAR.
instance Monoidal LINEAR where
  type Unit = L ()
  type L a ** L b = L (a, b)
  withOb2 :: forall (a :: LINEAR) (b :: LINEAR) r.
(Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 Ob (a ** b) => r
r = r
Ob (a ** b) => r
r
  leftUnitor :: forall (a :: LINEAR). Ob a => (Unit ** a) ~> a
leftUnitor = (((), UN 'L a) %1 -> UN 'L a)
-> Linear ('L ((), UN 'L a)) ('L (UN 'L a))
forall a b. (a %1 -> b) -> Linear ('L a) ('L b)
Linear \((), UN 'L a
x) -> UN 'L a
x
  leftUnitorInv :: forall (a :: LINEAR). Ob a => a ~> (Unit ** a)
leftUnitorInv = (UN 'L a %1 -> ((), UN 'L a))
-> Linear ('L (UN 'L a)) ('L ((), UN 'L a))
forall a b. (a %1 -> b) -> Linear ('L a) ('L b)
Linear \UN 'L a
x -> ((), UN 'L a
x)
  rightUnitor :: forall (a :: LINEAR). Ob a => (a ** Unit) ~> a
rightUnitor = ((UN 'L a, ()) %1 -> UN 'L a)
-> Linear ('L (UN 'L a, ())) ('L (UN 'L a))
forall a b. (a %1 -> b) -> Linear ('L a) ('L b)
Linear \(UN 'L a
x, ()) -> UN 'L a
x
  rightUnitorInv :: forall (a :: LINEAR). Ob a => a ~> (a ** Unit)
rightUnitorInv = (UN 'L a %1 -> (UN 'L a, ()))
-> Linear ('L (UN 'L a)) ('L (UN 'L a, ()))
forall a b. (a %1 -> b) -> Linear ('L a) ('L b)
Linear \UN 'L a
x -> (UN 'L a
x, ())
  associator :: forall (a :: LINEAR) (b :: LINEAR) (c :: LINEAR).
(Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator = (((UN 'L a, UN 'L b), UN 'L c) %1 -> (UN 'L a, (UN 'L b, UN 'L c)))
-> Linear
     ('L ((UN 'L a, UN 'L b), UN 'L c))
     ('L (UN 'L a, (UN 'L b, UN 'L c)))
forall a b. (a %1 -> b) -> Linear ('L a) ('L b)
Linear \((UN 'L a
x, UN 'L b
y), UN 'L c
z) -> (UN 'L a
x, (UN 'L b
y, UN 'L c
z))
  associatorInv :: forall (a :: LINEAR) (b :: LINEAR) (c :: LINEAR).
(Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv = ((UN 'L a, (UN 'L b, UN 'L c)) %1 -> ((UN 'L a, UN 'L b), UN 'L c))
-> Linear
     ('L (UN 'L a, (UN 'L b, UN 'L c)))
     ('L ((UN 'L a, UN 'L b), UN 'L c))
forall a b. (a %1 -> b) -> Linear ('L a) ('L b)
Linear \(UN 'L a
x, (UN 'L b
y, UN 'L c
z)) -> ((UN 'L a
x, UN 'L b
y), UN 'L c
z)

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

instance Closed LINEAR where
  type a ~~> b = L (UN L a %1 -> UN L b)
  withObExp :: forall (a :: LINEAR) (b :: LINEAR) r.
(Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp Ob (a ~~> b) => r
r = r
Ob (a ~~> b) => r
r
  curry :: forall (a :: LINEAR) (b :: LINEAR) (c :: LINEAR).
(Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
curry (Linear a %1 -> b
f) = (UN 'L a %1 -> UN 'L b %1 -> b)
-> Linear ('L (UN 'L a)) ('L (UN 'L b %1 -> b))
forall a b. (a %1 -> b) -> Linear ('L a) ('L b)
Linear \UN 'L a
a UN 'L b
b -> a %1 -> b
f (UN 'L a
a, UN 'L b
b)
  apply :: forall (a :: LINEAR) (b :: LINEAR).
(Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
apply = ((UN 'L a %1 -> UN 'L b, UN 'L a) %1 -> UN 'L b)
-> Linear ('L (UN 'L a %1 -> UN 'L b, UN 'L a)) ('L (UN 'L b))
forall a b. (a %1 -> b) -> Linear ('L a) ('L b)
Linear \(UN 'L a %1 -> UN 'L b
f, UN 'L a
a) -> UN 'L a %1 -> UN 'L b
f UN 'L a
a
  Linear a %1 -> b
f ^^^ :: forall (a :: LINEAR) (b :: LINEAR) (x :: LINEAR) (y :: 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 a b. (a %1 -> b) -> Linear ('L a) ('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 :: LINEAR +-> Type
data Forget a b where
  Forget :: (a -> b) -> Forget a (L b)
instance Profunctor Forget where
  dimap :: forall c a (b :: LINEAR) (d :: LINEAR).
(c ~> a) -> (b ~> d) -> Forget a b -> Forget c d
dimap = (c ~> a) -> (b ~> d) -> Forget a b -> Forget c d
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) (c :: k) (d :: j).
Representable p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimapRep
  (Ob a, Ob b) => r
r \\ :: forall a (b :: LINEAR) r. ((Ob a, Ob b) => r) -> Forget a b -> r
\\ Forget{} = r
(Ob a, Ob b) => r
r
instance Representable Forget where
  type Forget % a = UN L a
  index :: forall a (b :: LINEAR). Forget a b -> a ~> (Forget % b)
index (Forget a -> b
f) = a ~> (Forget % b)
a -> b
f
  tabulate :: forall (b :: LINEAR) a. Ob b => (a ~> (Forget % b)) -> Forget a b
tabulate = (a ~> (Forget % b)) -> Forget a b
(a -> UN 'L b) -> Forget a ('L (UN 'L b))
forall a a. (a -> a) -> Forget a ('L a)
Forget
  repMap :: forall (a :: LINEAR) (b :: LINEAR).
(a ~> b) -> (Forget % a) ~> (Forget % b)
repMap (Linear a %1 -> b
f) UN 'L a
x = a %1 -> b
f a
UN 'L a
x

-- | Forget is a lax monoidal functor
instance MonoidalProfunctor Forget where
  par0 :: Forget Unit Unit
par0 = (() -> ()) -> Forget () ('L ())
forall a a. (a -> a) -> Forget a ('L a)
Forget \() -> ()
  Forget x1 -> b
f par :: forall x1 (x2 :: LINEAR) y1 (y2 :: LINEAR).
Forget x1 x2 -> Forget y1 y2 -> Forget (x1 ** y1) (x2 ** y2)
`par` Forget y1 -> b
g = ((x1, y1) -> (b, b)) -> Forget (x1, y1) ('L (b, b))
forall a a. (a -> a) -> Forget a ('L a)
Forget \(x1
x, y1
y) -> (x1 -> b
f x1
x, y1 -> b
g y1
y)

-- | Forget is also a colax monoidal functor
instance MonoidalProfunctor (RepCostar Forget) where
  par0 :: RepCostar Forget Unit Unit
par0 = ((Forget % 'L ()) ~> ()) -> RepCostar Forget ('L ()) ()
forall {k} {j} (a :: k) (p :: k +-> j) (b :: j).
Ob a =>
((p % a) ~> b) -> RepCostar p a b
RepCostar (Forget % 'L ()) ~> ()
() -> ()
forall a. Ob a => a -> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id
  RepCostar (Forget % x1) ~> x2
f par :: forall (x1 :: LINEAR) x2 (y1 :: LINEAR) y2.
RepCostar Forget x1 x2
-> RepCostar Forget y1 y2 -> RepCostar Forget (x1 ** y1) (x2 ** y2)
`par` RepCostar (Forget % y1) ~> y2
g = ((Forget % 'L (UN 'L x1, UN 'L y1)) ~> (x2, y2))
-> RepCostar Forget ('L (UN 'L x1, UN 'L y1)) (x2, y2)
forall {k} {j} (a :: k) (p :: k +-> j) (b :: j).
Ob a =>
((p % a) ~> b) -> RepCostar p a b
RepCostar \(UN 'L x1
x, UN 'L y1
y) -> ((Forget % x1) ~> x2
UN 'L x1 -> x2
f UN 'L x1
x, (Forget % y1) ~> y2
UN 'L y1 -> y2
g UN 'L y1
y)

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

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

dupUr :: Ur a %1 -> Ur (Ur a)
dupUr :: forall a. Ur a %1 -> Ur (Ur a)
dupUr (Ur a
a) = Ur a -> Ur (Ur a)
forall a. a -> Ur a
Ur (a -> Ur a
forall a. a -> Ur a
Ur 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)

instance Comonoid (L (Ur a)) where
  counit :: 'L (Ur a) ~> Unit
counit = (Ur a %1 -> ()) -> Linear ('L (Ur a)) ('L ())
forall a b. (a %1 -> b) -> Linear ('L a) ('L b)
Linear \(Ur a
_) -> ()
  comult :: 'L (Ur a) ~> ('L (Ur a) ** 'L (Ur a))
comult = (Ur a %1 -> (Ur a, Ur a)) -> Linear ('L (Ur a)) ('L (Ur a, Ur a))
forall a b. (a %1 -> b) -> Linear ('L a) ('L b)
Linear \(Ur a
a) -> (a -> Ur a
forall a. a -> Ur a
Ur a
a, a -> Ur a
forall a. a -> Ur a
Ur a
a)

type Free :: Type +-> LINEAR
data Free a b where
  Free :: (a %1 -> Ur b) -> Free (L a) b
instance Profunctor Free where
  dimap :: forall (c :: LINEAR) (a :: LINEAR) b d.
(c ~> a) -> (b ~> d) -> Free a b -> Free c d
dimap = (c ~> a) -> (b ~> d) -> Free a b -> Free c d
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) (c :: k) (d :: j).
Representable p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimapRep
  (Ob a, Ob b) => r
r \\ :: forall (a :: LINEAR) b r. ((Ob a, Ob b) => r) -> Free a b -> r
\\ Free{} = r
(Ob a, Ob b) => r
r
instance Representable Free where
  type Free % a = L (Ur a)
  index :: forall (a :: LINEAR) b. Free a b -> a ~> (Free % b)
index (Free a %1 -> Ur b
f) = (a %1 -> Ur b) -> Linear ('L a) ('L (Ur b))
forall a b. (a %1 -> b) -> Linear ('L a) ('L b)
Linear a %1 -> Ur b
f
  tabulate :: forall b (a :: LINEAR). Ob b => (a ~> (Free % b)) -> Free a b
tabulate (Linear a %1 -> b
f) = (a %1 -> Ur b) -> Free ('L a) b
forall a b. (a %1 -> Ur b) -> Free ('L a) b
Free a %1 -> b
a %1 -> Ur b
f
  repMap :: forall a b. (a ~> b) -> (Free % a) ~> (Free % b)
repMap a ~> b
f = (Ur a %1 -> Ur b) -> Linear ('L (Ur a)) ('L (Ur b))
forall a b. (a %1 -> b) -> Linear ('L a) ('L b)
Linear \(Ur a
a) -> b -> Ur b
forall a. a -> Ur a
Ur (a ~> b
a -> b
f a
a)

-- | Free is a lax monoidal functor
instance MonoidalProfunctor Free where
  par0 :: Free Unit Unit
par0 = (() %1 -> Ur ()) -> Free ('L ()) ()
forall a b. (a %1 -> Ur b) -> Free ('L a) b
Free \() -> () -> Ur ()
forall a. a -> Ur a
Ur ()
  Free a %1 -> Ur x2
f par :: forall (x1 :: LINEAR) x2 (y1 :: LINEAR) y2.
Free x1 x2 -> Free y1 y2 -> Free (x1 ** y1) (x2 ** y2)
`par` Free a %1 -> Ur y2
g = ((a, a) %1 -> Ur (x2, y2)) -> Free ('L (a, a)) (x2, y2)
forall a b. (a %1 -> Ur b) -> Free ('L a) b
Free \(a
x, a
y) -> case (a %1 -> Ur x2
f a
x, a %1 -> Ur y2
g a
y) of (Ur x2
a, Ur y2
b) -> (x2, y2) -> Ur (x2, y2)
forall a. a -> Ur a
Ur (x2
a, y2
b)

-- | Free is also a colax monoidal functor
instance MonoidalProfunctor (RepCostar Free) where
  par0 :: RepCostar Free Unit Unit
par0 = ((Free % ()) ~> 'L ()) -> RepCostar Free () ('L ())
forall {k} {j} (a :: k) (p :: k +-> j) (b :: j).
Ob a =>
((p % a) ~> b) -> RepCostar p a b
RepCostar ((Ur () %1 -> ()) -> Linear ('L (Ur ())) ('L ())
forall a b. (a %1 -> b) -> Linear ('L a) ('L b)
Linear (\(Ur ()
_) -> ()))
  RepCostar (Linear a %1 -> b
f) par :: forall x1 (x2 :: LINEAR) y1 (y2 :: LINEAR).
RepCostar Free x1 x2
-> RepCostar Free y1 y2 -> RepCostar Free (x1 ** y1) (x2 ** y2)
`par` RepCostar (Linear a %1 -> b
g) = ((Free % (x1, y1)) ~> 'L (b, b))
-> RepCostar Free (x1, y1) ('L (b, b))
forall {k} {j} (a :: k) (p :: k +-> j) (b :: j).
Ob a =>
((p % a) ~> b) -> RepCostar p a b
RepCostar ((Ur (x1, y1) %1 -> (b, b)) -> Linear ('L (Ur (x1, y1))) ('L (b, b))
forall a b. (a %1 -> b) -> Linear ('L a) ('L b)
Linear \(Ur (x1
x, y1
y)) -> (a %1 -> b
f (x1 -> Ur x1
forall a. a -> Ur a
Ur x1
x), a %1 -> b
g (y1 -> Ur y1
forall a. a -> Ur a
Ur y1
y)))

instance Adjunction Free Forget where
  unit :: forall a. Ob a => (:.:) Forget Free a a
unit = (a -> Ur a) -> Forget a ('L (Ur a))
forall a a. (a -> a) -> Forget a ('L a)
Forget a -> Ur a
forall a. a -> Ur a
Ur Forget a ('L (Ur a)) -> Free ('L (Ur a)) a -> (:.:) Forget Free a a
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: (Ur a %1 -> Ur a) -> Free ('L (Ur a)) a
forall a b. (a %1 -> Ur b) -> Free ('L a) b
Free \Ur a
x -> Ur a
x
  counit :: (Free :.: Forget) :~> (~>)
counit (Free a %1 -> Ur b
f :.: Forget b -> b
g) = (a %1 -> b) -> Linear ('L a) ('L b)
forall a b. (a %1 -> b) -> Linear ('L a) ('L b)
Linear \a
a -> case a %1 -> Ur b
f a
a of Ur b
b -> b -> b
g b
b

instance HasBinaryCoproducts LINEAR where
  type L a || L b = L (Either a b)
  withObCoprod :: forall (a :: LINEAR) (b :: LINEAR) r.
(Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod Ob (a || b) => r
r = r
Ob (a || b) => r
r
  lft :: forall (a :: LINEAR) (b :: LINEAR). (Ob a, Ob b) => a ~> (a || b)
lft = (UN 'L a %1 -> Either (UN 'L a) (UN 'L b))
-> Linear ('L (UN 'L a)) ('L (Either (UN 'L a) (UN 'L b)))
forall a b. (a %1 -> b) -> Linear ('L a) ('L b)
Linear UN 'L a -> Either (UN 'L a) (UN 'L b)
forall a b. a -> Either a b
Left
  rgt :: forall (a :: LINEAR) (b :: LINEAR). (Ob a, Ob b) => b ~> (a || b)
rgt = (UN 'L b %1 -> Either (UN 'L a) (UN 'L b))
-> Linear ('L (UN 'L b)) ('L (Either (UN 'L a) (UN 'L b)))
forall a b. (a %1 -> b) -> Linear ('L a) ('L b)
Linear UN 'L b -> Either (UN 'L a) (UN 'L 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 a b. (a %1 -> b) -> Linear ('L a) ('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). Ob a => InitialObject ~> a
initiate = (Void %1 -> UN 'L a) -> Linear ('L Void) ('L (UN 'L a))
forall a b. (a %1 -> b) -> Linear ('L a) ('L b)
Linear \case {}

instance Costrong (COPROD LINEAR) (Coprod (Id :: CAT LINEAR)) where
  coact :: forall (a :: COPROD LINEAR) (x :: COPROD LINEAR)
       (y :: COPROD LINEAR).
(Ob a, Ob x, Ob y) =>
Coprod Id (Act a x) (Act a y) -> Coprod Id x y
coact (Coprod (Id (Linear a %1 -> b
uxuy))) = Id ('L (UN 'L (UN 'COPR x))) ('L (UN 'L (UN 'COPR y)))
-> Coprod
     Id
     ('COPR ('L (UN 'L (UN 'COPR x))))
     ('COPR ('L (UN 'L (UN 'COPR y))))
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Coprod p ('COPR a1) ('COPR b1)
Coprod (('L (UN 'L (UN 'COPR x)) ~> 'L (UN 'L (UN 'COPR y)))
-> Id ('L (UN 'L (UN 'COPR x))) ('L (UN 'L (UN 'COPR y)))
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id (Linear ('L a) ('L (UN 'L (UN 'COPR y)))
loop Linear ('L a) ('L (UN 'L (UN 'COPR y)))
-> Linear ('L (UN 'L (UN 'COPR x))) ('L a)
-> Linear ('L (UN 'L (UN 'COPR x))) ('L (UN 'L (UN 'COPR y)))
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: LINEAR) (c :: LINEAR) (a :: LINEAR).
Linear b c -> Linear a b -> Linear a c
. (UN 'L (UN 'COPR x) %1 -> a)
-> Linear ('L (UN 'L (UN 'COPR x))) ('L a)
forall a b. (a %1 -> b) -> Linear ('L a) ('L b)
Linear UN 'L (UN 'COPR x) %1 -> a
UN 'L (UN 'COPR x)
-> Either (UN 'L (UN 'COPR a)) (UN 'L (UN 'COPR x))
forall a b. b -> Either a b
Right))
    where
      loop :: Linear ('L a) ('L (UN 'L (UN 'COPR y)))
loop = (a %1 -> UN 'L (UN 'COPR y))
-> Linear ('L a) ('L (UN 'L (UN 'COPR y)))
forall a b. (a %1 -> b) -> Linear ('L a) ('L b)
Linear \a
ux -> case a %1 -> b
uxuy a
ux of Left UN 'L (UN 'COPR a)
x -> ('L (Either (UN 'L (UN 'COPR a)) (UN 'L (UN 'COPR x)))
 ~> 'L (UN 'L (UN 'COPR y)))
%1 -> Either (UN 'L (UN 'COPR a)) (UN 'L (UN 'COPR x))
%1 -> UN 'L (UN 'COPR y)
forall a b. ('L a ~> 'L b) %1 -> a %1 -> b
unLinear 'L (Either (UN 'L (UN 'COPR a)) (UN 'L (UN 'COPR x)))
~> 'L (UN 'L (UN 'COPR y))
Linear ('L a) ('L (UN 'L (UN 'COPR y)))
loop (UN 'L (UN 'COPR a)
-> Either (UN 'L (UN 'COPR a)) (UN 'L (UN 'COPR x))
forall a b. a -> Either a b
Left UN 'L (UN 'COPR a)
x); Right UN 'L (UN 'COPR y)
b -> UN 'L (UN 'COPR y)
b

data Top where
  Top :: a %1 -> Top

data With a b where
  With :: x %1 -> (x %1 -> a) -> (x %1 -> b) -> With a b

urWith :: Ur (With a b) %1 -> (Ur a, Ur b)
urWith :: forall a b. Ur (With a b) %1 -> (Ur a, Ur b)
urWith (Ur (With x
x x %1 -> a
f x %1 -> b
g)) = (a -> Ur a
forall a. a -> Ur a
Ur (x %1 -> a
f x
x), b -> Ur b
forall a. a -> Ur a
Ur (x %1 -> b
g x
x))

mkWith :: a -> b -> With a b
mkWith :: forall a b. a -> b -> With a b
mkWith a
a b
b = () -> (() %1 -> a) -> (() %1 -> b) -> With a b
forall a a b. a -> (a %1 -> a) -> (a %1 -> b) -> With a b
With () (\() -> a
a) (\() -> b
b)

instance HasTerminalObject LINEAR where
  type TerminalObject = L Top
  terminate :: forall (a :: LINEAR). Ob a => a ~> TerminalObject
terminate = (UN 'L a %1 -> Top) -> Linear ('L (UN 'L a)) ('L Top)
forall a b. (a %1 -> b) -> Linear ('L a) ('L b)
Linear UN 'L a -> Top
forall a. a -> Top
Top

instance HasBinaryProducts LINEAR where
  type L a && L b = L (With a b)
  withObProd :: forall (a :: LINEAR) (b :: LINEAR) r.
(Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd Ob (a && b) => r
r = r
Ob (a && b) => r
r
  fst :: forall (a :: LINEAR) (b :: LINEAR). (Ob a, Ob b) => (a && b) ~> a
fst = (With (UN 'L a) (UN 'L b) %1 -> UN 'L a)
-> Linear ('L (With (UN 'L a) (UN 'L b))) ('L (UN 'L a))
forall a b. (a %1 -> b) -> Linear ('L a) ('L b)
Linear \(With x
x x %1 -> UN 'L a
xa x %1 -> UN 'L b
_) -> x %1 -> UN 'L a
xa x
x
  snd :: forall (a :: LINEAR) (b :: LINEAR). (Ob a, Ob b) => (a && b) ~> b
snd = (With (UN 'L a) (UN 'L b) %1 -> UN 'L b)
-> Linear ('L (With (UN 'L a) (UN 'L b))) ('L (UN 'L b))
forall a b. (a %1 -> b) -> Linear ('L a) ('L b)
Linear \(With x
x x %1 -> UN 'L a
_ x %1 -> UN 'L b
xb) -> x %1 -> UN 'L b
xb x
x
  Linear a %1 -> b
f &&& :: forall (a :: LINEAR) (x :: LINEAR) (y :: LINEAR).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& Linear a %1 -> b
g = (a %1 -> With b b) -> Linear ('L a) ('L (With b b))
forall a b. (a %1 -> b) -> Linear ('L a) ('L b)
Linear \a
x -> a -> (a %1 -> b) -> (a %1 -> b) -> With b b
forall a a b. a -> (a %1 -> a) -> (a %1 -> b) -> With a b
With a
x a %1 -> b
f a %1 -> b
a %1 -> b
g

instance Powered LINEAR where
  type L a ^ n = L (n -> a)
  withObPower :: forall (a :: LINEAR) n r. Ob a => (Ob (a ^ n) => r) -> r
withObPower Ob (a ^ n) => r
r = r
Ob (a ^ n) => r
r
  power :: forall (a :: LINEAR) (b :: LINEAR) n.
(Ob a, Ob b) =>
(n -> a ~> b) -> a ~> (b ^ n)
power n -> a ~> b
f = (UN 'L a %1 -> n -> UN 'L b)
-> Linear ('L (UN 'L a)) ('L (n -> UN 'L b))
forall a b. (a %1 -> b) -> Linear ('L a) ('L b)
Linear \UN 'L a
x n
n -> ('L (UN 'L a) ~> 'L (UN 'L b)) %1 -> UN 'L a %1 -> UN 'L b
forall a b. ('L a ~> 'L b) %1 -> a %1 -> b
unLinear (n -> a ~> b
f n
n) UN 'L a
x
  unpower :: forall (b :: LINEAR) (a :: LINEAR) n.
Ob b =>
(a ~> (b ^ n)) -> n -> a ~> b
unpower (Linear a %1 -> b
f) n
n = (a %1 -> UN 'L b) -> Linear ('L a) ('L (UN 'L b))
forall a b. (a %1 -> b) -> Linear ('L a) ('L b)
Linear \a
x -> a %1 -> b
f a
x n
n

instance Copowered LINEAR where
  type n *. L a = L (Ur n, a)
  withObCopower :: forall (a :: LINEAR) n r. Ob a => (Ob (n *. a) => r) -> r
withObCopower Ob (n *. a) => r
r = r
Ob (n *. a) => r
r
  copower :: forall (a :: LINEAR) (b :: LINEAR) n.
(Ob a, Ob b) =>
(n -> a ~> b) -> (n *. a) ~> b
copower n -> a ~> b
f = ((Ur n, UN 'L a) %1 -> UN 'L b)
-> Linear ('L (Ur n, UN 'L a)) ('L (UN 'L b))
forall a b. (a %1 -> b) -> Linear ('L a) ('L b)
Linear \(Ur n
n, UN 'L a
a) -> ('L (UN 'L a) ~> 'L (UN 'L b)) %1 -> UN 'L a %1 -> UN 'L b
forall a b. ('L a ~> 'L b) %1 -> a %1 -> b
unLinear (n -> a ~> b
f n
n) UN 'L a
a
  uncopower :: forall (a :: LINEAR) n (b :: LINEAR).
Ob a =>
((n *. a) ~> b) -> n -> a ~> b
uncopower (Linear a %1 -> b
f) n
n = (UN 'L a %1 -> b) -> Linear ('L (UN 'L a)) ('L b)
forall a b. (a %1 -> b) -> Linear ('L a) ('L b)
Linear \UN 'L a
x -> a %1 -> b
f (n -> Ur n
forall a. a -> Ur a
Ur n
n, UN 'L a
x)

type Not a = a %1 -> ()

not :: (Not b %1 -> Not a) %1 -> a %1 -> b
not :: forall b a. (Not b %1 -> Not a) %1 -> a %1 -> b
not Not b %1 -> Not a
nbna a
a = Not (Not b) %1 -> b
forall a. Not (Not a) %1 -> a
dn \Not b
nb -> Not b %1 -> Not a
nbna Not b
nb a
a

not' :: (a %1 -> b) %1 -> Not b %1 -> Not a
not' :: forall a b. (a %1 -> b) %1 -> Not b %1 -> Not a
not' a %1 -> b
ab Not b
nb a
a = Not b
nb (a %1 -> b
ab a
a)

newtype Par a b = Par (Not (Not a, Not b))

mkPar :: a %1 -> b %1 -> Par a b
mkPar :: forall a b. a %1 -> b %1 -> Par a b
mkPar a
a b
b = Not (Not a, Not b) -> Par a b
forall a b. Not (Not a, Not b) -> Par a b
Par \(Not a
na, Not b
nb) -> case (Not a
na a
a, Not b
nb b
b) of ((), ()) -> ()

pairFst :: (a, b `Par` c) %1 -> (a, b) `Par` c
pairFst :: forall a b c. (a, Par b c) %1 -> Par (a, b) c
pairFst (a
a, Par Not (Not b, Not c)
f) = Not (Not (a, b), Not c) -> Par (a, b) c
forall a b. Not (Not a, Not b) -> Par a b
Par \(Not (a, b)
nab, Not c
nc) -> Not (Not b, Not c)
f (\b
b -> Not (a, b)
nab (a
a, b
b), Not c
nc)

pairSnd :: (a `Par` b, c) %1 -> a `Par` (b, c)
pairSnd :: forall a b c. (Par a b, c) %1 -> Par a (b, c)
pairSnd (Par Not (Not a, Not b)
f, c
c) = Not (Not a, Not (b, c)) -> Par a (b, c)
forall a b. Not (Not a, Not b) -> Par a b
Par \(Not a
na, Not (b, c)
nbc) -> Not (Not a, Not b)
f (Not a
na, \b
b -> Not (b, c)
nbc (b
b, c
c))

parAppL :: (a `Par` b) %1 -> Not a %1 -> b
parAppL :: forall a b. Par a b %1 -> Not a %1 -> b
parAppL (Par Not (Not a, Not b)
f) Not a
na = Not (Not b) %1 -> b
forall a. Not (Not a) %1 -> a
dn \Not b
nb -> Not (Not a, Not b)
f (Not a
na, Not b
nb)

parAppR :: (a `Par` b) %1 -> Not b %1 -> a
parAppR :: forall a b. Par a b %1 -> Not b %1 -> a
parAppR (Par Not (Not a, Not b)
f) Not b
nb = Not (Not a) %1 -> a
forall a. Not (Not a) %1 -> a
dn \Not a
na -> Not (Not a, Not b)
f (Not a
na, Not b
nb)

newtype Quest a = Quest (Not (Ur (Not a)))

notQuest :: Not (Quest a) %1 -> Ur (Not a)
notQuest :: forall a. Not (Quest a) %1 -> Ur (Not a)
notQuest Not (Quest a)
nqa = Not (Not (Ur (Not a))) %1 -> Ur (Not a)
forall a. Not (Not a) %1 -> a
dn \Not (Ur (Not a))
nuna -> Not (Quest a)
nqa (Not (Ur (Not a)) -> Quest a
forall a. Not (Ur (Not a)) -> Quest a
Quest Not (Ur (Not a))
nuna)

unitQuest :: a %1 -> Quest a
unitQuest :: forall a. a %1 -> Quest a
unitQuest a
a = Not (Ur (Not a)) -> Quest a
forall a. Not (Ur (Not a)) -> Quest a
Quest \(Ur Not a
na) -> Not a
na a
a

multQuest :: Quest (Quest a) %1 -> Quest a
multQuest :: forall a. Quest (Quest a) %1 -> Quest a
multQuest (Quest Not (Ur (Not (Quest a)))
f) = Not (Ur (Not a)) -> Quest a
forall a. Not (Ur (Not a)) -> Quest a
Quest \(Ur Not a
na) -> Not (Ur (Not (Quest a)))
f (Not (Quest a) -> Ur (Not (Quest a))
forall a. a -> Ur a
Ur (\(Quest Not (Ur (Not a))
nuna) -> Not (Ur (Not a))
nuna (Not a -> Ur (Not a)
forall a. a -> Ur a
Ur Not a
na)))

questPar :: Par (Quest a) (Quest b) %1 -> Quest (Either a b)
questPar :: forall a b. Par (Quest a) (Quest b) %1 -> Quest (Either a b)
questPar (Par Not (Not (Quest a), Not (Quest b))
f) = Not (Ur (Not (Either a b))) -> Quest (Either a b)
forall a. Not (Ur (Not a)) -> Quest a
Quest (\(Ur Not (Either a b)
g) -> Not (Not (Quest a), Not (Quest b))
f (\(Quest Not (Ur (Not a))
nuna) -> Not (Ur (Not a))
nuna (Not a -> Ur (Not a)
forall a. a -> Ur a
Ur (\a
a -> Not (Either a b)
g (a -> Either a b
forall a b. a -> Either a b
Left a
a))), \(Quest Not (Ur (Not b))
nunb) -> Not (Ur (Not b))
nunb (Not b -> Ur (Not b)
forall a. a -> Ur a
Ur (\b
b -> Not (Either a b)
g (b -> Either a b
forall a b. b -> Either a b
Right b
b)))))

-- LINEAR is not CompactClosed. And hence it is also not traced,
-- since any star autonomous category with a trace is compact closed.
instance StarAutonomous LINEAR where
  type Dual (L a) = L (Not a)
  dual :: forall (a :: LINEAR) (b :: LINEAR). (a ~> b) -> Dual b ~> Dual a
dual (Linear a %1 -> b
f) = ((b %1 -> ()) %1 -> a %1 -> ())
-> Linear ('L (b %1 -> ())) ('L (a %1 -> ()))
forall a b. (a %1 -> b) -> Linear ('L a) ('L b)
Linear (\b %1 -> ()
nb a
a -> b %1 -> ()
nb (a %1 -> b
f a
a))
  dualInv :: forall (a :: LINEAR) (b :: LINEAR).
(Ob a, Ob b) =>
(Dual a ~> Dual b) -> b ~> a
dualInv (Linear a %1 -> b
f) = (UN 'L b %1 -> UN 'L a) -> Linear ('L (UN 'L b)) ('L (UN 'L a))
forall a b. (a %1 -> b) -> Linear ('L a) ('L b)
Linear (\UN 'L b
b -> Not (Not (UN 'L a)) %1 -> UN 'L a
forall a. Not (Not a) %1 -> a
dn (\Not (UN 'L a)
na -> a %1 -> b
f a
Not (UN 'L a)
na UN 'L b
b))
  linDist :: forall (a :: LINEAR) (b :: LINEAR) (c :: LINEAR).
(Ob a, Ob b, Ob c) =>
((a ** b) ~> Dual c) -> a ~> Dual (b ** c)
linDist (Linear a %1 -> b
f) = (UN 'L a %1 -> (UN 'L b, UN 'L c) %1 -> ())
-> Linear ('L (UN 'L a)) ('L ((UN 'L b, UN 'L c) %1 -> ()))
forall a b. (a %1 -> b) -> Linear ('L a) ('L b)
Linear (\UN 'L a
a (UN 'L b
b, UN 'L c
c) -> a %1 -> b
f (UN 'L a
a, UN 'L b
b) UN 'L c
c)
  linDistInv :: forall (a :: LINEAR) (b :: LINEAR) (c :: LINEAR).
(Ob a, Ob b, Ob c) =>
(a ~> Dual (b ** c)) -> (a ** b) ~> Dual c
linDistInv (Linear a %1 -> b
f) = ((a, UN 'L b) %1 -> UN 'L c %1 -> ())
-> Linear ('L (a, UN 'L b)) ('L (UN 'L c %1 -> ()))
forall a b. (a %1 -> b) -> Linear ('L a) ('L b)
Linear (\(a
a, UN 'L b
b) UN 'L c
c -> a %1 -> b
f a
a (UN 'L b
b, UN 'L c
c))

-- | Double negation is possible with linear functions, though using `unsafeDupablePerformIO`.
-- Derived from https://gist.github.com/ant-arctica/7563282c57d9d1ce0c4520c543187932
-- TODO: only tested in GHCi, might get ruined by optimizations
dn :: Not (Not a) %1 -> a
dn :: forall a. Not (Not a) %1 -> a
dn Not (Not a)
nna =
  let ref :: IORef a
ref = IO (IORef a) -> IORef a
forall a. IO a -> a
unsafeDupablePerformIO (a -> IO (IORef a)
forall a. a -> IO (IORef a)
newIORef a
forall a. HasCallStack => a
undefined)
  in case Not (Not a)
nna ((a -> ()) %1 -> Not a
forall a b. (a -> b) %1 -> a %1 -> b
unsafeLinear (IORef a -> a -> ()
forall {a}. IORef a -> a -> ()
fill IORef a
forall {a}. IORef a
ref)) of () -> IO a -> a
forall a. IO a -> a
unsafeDupablePerformIO (IORef a -> IO a
forall a. IORef a -> IO a
readIORef IORef a
forall {a}. IORef a
ref)
  where
    fill :: IORef a -> a -> ()
fill IORef a
ref a
x = IO () -> ()
forall a. IO a -> a
unsafeDupablePerformIO (IORef a -> a -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef a
ref a
x)

unsafeLinear :: (a -> b) %1 -> (a %1 -> b)
unsafeLinear :: forall a b. (a -> b) %1 -> a %1 -> b
unsafeLinear = (ZonkAny 0 -> ZonkAny 1) -> (a -> b) %1 -> a %1 -> b
forall a b. a -> b
unsafeCoerce ZonkAny 0 -> ZonkAny 1
forall a b. a -> b
unsafeCoerce

unit :: L () ~> L (Par a (Not a))
unit :: forall a. 'L () ~> 'L (Par a (Not a))
unit = (() %1 -> Par a (a %1 -> ()))
-> Linear ('L ()) ('L (Par a (a %1 -> ())))
forall a b. (a %1 -> b) -> Linear ('L a) ('L b)
Linear \() -> Not (a %1 -> (), Not (a %1 -> ())) -> Par a (a %1 -> ())
forall a b. Not (Not a, Not b) -> Par a b
Par \(a %1 -> ()
na, Not (a %1 -> ())
nna) -> Not (a %1 -> ())
nna a %1 -> ()
na

counit :: L (Not a, a) ~> L ()
counit :: forall a. 'L (Not a, a) ~> 'L ()
counit = ((a %1 -> (), a) %1 -> ()) -> Linear ('L (a %1 -> (), a)) ('L ())
forall a b. (a %1 -> b) -> Linear ('L a) ('L b)
Linear \(a %1 -> ()
na, a
a) -> a %1 -> ()
na a
a

type p !~> q = forall a b. p a b %1 -> q a b

type NegComp :: (j +-> k) -> (i +-> j) -> (i +-> k)
data NegComp p q a c where
  NegComp :: (forall b. Par (p a b) (q b c)) %1 -> NegComp p q a c

newtype Neg p a b = Neg (Not (p b a))

getNeg :: Neg p a b %1 -> Not (p b a)
getNeg :: forall {k} {k} (p :: k -> k -> Type) (a :: k) (b :: k).
Neg p a b %1 -> Not (p b a)
getNeg (Neg Not (p b a)
f) = Not (p b a)
f

conv1 :: NegComp p q !~> Neg (Neg q :.: Neg p)
conv1 :: forall {k} {k} {k} (p :: k +-> k) (q :: k +-> k) (a :: k) (b :: k).
NegComp p q a b %1 -> Neg (Neg q :.: Neg p) a b
conv1 (NegComp forall (b :: k). Par (p a b) (q b b)
e) = Not ((:.:) (Neg q) (Neg p) b a) -> Neg (Neg q :.: Neg p) a b
forall {k} {k} (p :: k -> k -> Type) (a :: k) (b :: k).
Not (p b a) -> Neg p a b
Neg \(Neg Not (q b b)
nq :.: Neg Not (p a b)
np) -> case Par (p a b) (q b b)
forall (b :: k). Par (p a b) (q b b)
e of Par Not (Not (p a b), Not (q b b))
e' -> Not (Not (p a b), Not (q b b))
e' (Not (p a b)
np, Not (q b b)
nq)

conv2 :: Neg (Neg q :.: Neg p) !~> NegComp p q
conv2 :: forall {j} {i} {k} (q :: j -> i -> Type) (p :: k -> j -> Type)
       (a :: k) (b :: i).
Neg (Neg q :.: Neg p) a b %1 -> NegComp p q a b
conv2 (Neg Not ((:.:) (Neg q) (Neg p) b a)
f) = (forall (b :: j). Par (p a b) (q b b)) -> NegComp p q a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (q :: i +-> j) (c :: i).
(forall (b :: j). Par (p a b) (q b c)) -> NegComp p q a c
NegComp (Not (Not (p a b), Not (q b b)) -> Par (p a b) (q b b)
forall a b. Not (Not a, Not b) -> Par a b
Par (\(Not (p a b)
np, Not (q b b)
nq) -> Not ((:.:) (Neg q) (Neg p) b a)
f (Not (q b b) -> Neg q b b
forall {k} {k} (p :: k -> k -> Type) (a :: k) (b :: k).
Not (p b a) -> Neg p a b
Neg Not (q b b)
nq Neg q b b -> Neg p b a -> (:.:) (Neg q) (Neg p) b a
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: Not (p a b) -> Neg p b a
forall {k} {k} (p :: k -> k -> Type) (a :: k) (b :: k).
Not (p b a) -> Neg p a b
Neg Not (p a b)
np)))

asCocat :: (Neg p :.: Neg p !~> Neg p) -> p !~> NegComp p p
asCocat :: forall {i} (p :: i -> i -> Type).
((Neg p :.: Neg p) !~> Neg p) -> p !~> NegComp p p
asCocat (Neg p :.: Neg p) !~> Neg p
comp p a b
p = (forall (b :: i). Par (p a b) (p b b)) -> NegComp p p a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (q :: i +-> j) (c :: i).
(forall (b :: j). Par (p a b) (q b c)) -> NegComp p q a c
NegComp (Not (Not (p a b), Not (p b b)) -> Par (p a b) (p b b)
forall a b. Not (Not a, Not b) -> Par a b
Par \(Not (p a b)
np1, Not (p b b)
np2) -> Neg p b a %1 -> Not (p a b)
forall {k} {k} (p :: k -> k -> Type) (a :: k) (b :: k).
Neg p a b %1 -> Not (p b a)
getNeg ((:.:) (Neg p) (Neg p) b a %1 -> Neg p b a
(Neg p :.: Neg p) !~> Neg p
comp (Not (p b b) -> Neg p b b
forall {k} {k} (p :: k -> k -> Type) (a :: k) (b :: k).
Not (p b a) -> Neg p a b
Neg Not (p b b)
np2 Neg p b b -> Neg p b a -> (:.:) (Neg p) (Neg p) b a
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: Not (p a b) -> Neg p b a
forall {k} {k} (p :: k -> k -> Type) (a :: k) (b :: k).
Not (p b a) -> Neg p a b
Neg Not (p a b)
np1)) p a b
p)