{-# LANGUAGE LinearTypes #-}

module Proarrow.Category.Instance.Linear where

import Data.IORef (newIORef, readIORef, writeIORef)
import Data.Kind (Type)
import Data.Void (Void)
import Prelude (Bool (..), Either (..), Eq (..), Show (..), showParen, showString, undefined, (&&), (>))

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 (..), FunctorForRep (..))
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.Corepresentable (Corep (..), Corepresentable (..))
import Proarrow.Profunctor.Identity (Id (..))
import Proarrow.Profunctor.Representable (Rep (..))
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))

data family Forget :: LINEAR +-> Type
instance FunctorForRep Forget where
  type Forget @ a = UN L a
  fmap :: forall (a :: LINEAR) (b :: LINEAR).
(a ~> b) -> (Forget @ a) ~> (Forget @ b)
fmap (Linear a %1 -> b
f) UN 'L a
x = a %1 -> b
f a
UN 'L a
x

-- | By creating the left adjoint to the forgetful functor,
-- we obtain the free-forgetful adjunction between Hask and LINEAR
instance Corepresentable (Rep Forget :: LINEAR +-> Type) where
  type Rep Forget %% a = L (Ur a)
  coindex :: forall a (b :: LINEAR). Rep Forget a b -> (Rep Forget %% a) ~> b
coindex (Rep a ~> (Forget @ b)
f) = (Ur a %1 -> UN 'L b) -> Linear ('L (Ur a)) ('L (UN 'L b))
forall a b. (a %1 -> b) -> Linear ('L a) ('L b)
Linear \(Ur a
a) -> a ~> (Forget @ b)
a -> UN 'L b
f a
a
  cotabulate :: forall a (b :: LINEAR).
Ob a =>
((Rep Forget %% a) ~> b) -> Rep Forget a b
cotabulate (Linear a %1 -> b
f) = (a ~> (Forget @ b)) -> Rep Forget a b
forall {j} {k} (f :: j +-> k) (a :: k) (b :: j).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep \a
a -> a %1 -> b
f (a -> Ur a
forall a. a -> Ur a
Ur a
a)
  corepMap :: forall a b. (a ~> b) -> (Rep Forget %% a) ~> (Rep Forget %% b)
corepMap 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)

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

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

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
instance Show Top where
  showsPrec :: Int -> Top -> ShowS
showsPrec Int
_ Top
_ = String -> ShowS
showString String
"⊤"
instance Eq Top where
  Top
_ == :: Top -> Top -> Bool
== Top
_ = Bool
True

data With a b where
  With :: x %1 -> (x %1 -> a) -> (x %1 -> b) -> With a b
instance (Show a, Show b) => Show (With a b) where
  showsPrec :: Int -> With a b -> ShowS
showsPrec Int
d (With x
x x %1 -> a
f x %1 -> b
g) = Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
9) (String -> ShowS
showString String
"mkWith " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Int -> a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
10 (x %1 -> a
f x
x) ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. String -> ShowS
showString String
" " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Int -> b -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
10 (x %1 -> b
g x
x))
instance (Eq a, Eq b) => Eq (With a b) where
  With x
x x %1 -> a
fa x %1 -> b
fb == :: With a b -> With a b -> Bool
== With x
y x %1 -> a
ga x %1 -> b
gb = (x %1 -> a
fa x
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== x %1 -> a
ga x
y) Bool -> Bool -> Bool
&& (x %1 -> b
fb x
x b -> b -> Bool
forall a. Eq a => a -> a -> Bool
== x %1 -> b
gb x
y)

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 Type LINEAR where
  type L a ^ n = L (n -> a)
  withObPower :: forall (a :: LINEAR) n r. (Ob a, Ob n) => (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 ~> HomObj Type a b) -> a ~> (b ^ n)
power n ~> HomObj Type 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 ~> HomObj Type a b
n -> Linear ('L (UN 'L a)) ('L (UN 'L b))
f n
n) UN 'L a
x
  unpower :: forall (b :: LINEAR) n (a :: LINEAR).
(Ob b, Ob n) =>
(a ~> (b ^ n)) -> n ~> HomObj Type 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 Type LINEAR where
  type n *. L a = L (Ur n, a)
  withObCopower :: forall (a :: LINEAR) n r. (Ob a, Ob n) => (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 ~> HomObj Type a b) -> (n *. a) ~> b
copower n ~> HomObj Type 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 ~> HomObj Type a b
n -> Linear ('L (UN 'L a)) ('L (UN 'L b))
f n
n) UN 'L a
a
  uncopower :: forall (a :: LINEAR) n (b :: LINEAR).
(Ob a, Ob n) =>
((n *. a) ~> b) -> n ~> HomObj Type 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 -> ()) -> Not a
forall a b. (a -> b) -> 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) -> (a %1 -> b)
unsafeLinear :: forall a b. (a -> b) -> a %1 -> b
unsafeLinear = (a -> b) -> a %1 -> b
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)