module Proarrow.Object.NaturalNumbers where

import Data.Kind (Type)
import Data.Nat qualified as N

import Proarrow.Category.Instance.Product ((:**:) (..))
import Proarrow.Category.Instance.Unit qualified as U
import Proarrow.Category.Monoidal (Monoidal (..), SymMonoidal (..))
import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..))
import Proarrow.Object.BinaryProduct ()

class (SymMonoidal k, Ob (NNO :: k)) => HasParamNNO k where
  type NNO :: k
  zero :: Unit ~> (NNO :: k)
  succ :: NNO ~> (NNO :: k)
  nnoUniv :: forall (a :: k) x. a ~> x -> x ~> x -> a ** NNO ~> x

add :: forall {k}. (HasParamNNO k) => NNO ** NNO ~> (NNO :: k)
add :: forall {k}. HasParamNNO k => (NNO ** NNO) ~> NNO
add = (NNO ~> NNO) -> (NNO ~> NNO) -> (NNO ** NNO) ~> NNO
forall (a :: k) (x :: k). (a ~> x) -> (x ~> x) -> (a ** NNO) ~> x
forall k (a :: k) (x :: k).
HasParamNNO k =>
(a ~> x) -> (x ~> x) -> (a ** NNO) ~> x
nnoUniv NNO ~> NNO
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id NNO ~> NNO
forall k. HasParamNNO k => NNO ~> NNO
succ

instance HasParamNNO () where
  type NNO = '()
  zero :: Unit ~> NNO
zero = Unit ~> NNO
Unit '() '()
U.Unit
  succ :: NNO ~> NNO
succ = NNO ~> NNO
Unit '() '()
U.Unit
  nnoUniv :: forall (a :: ()) (x :: ()). (a ~> x) -> (x ~> x) -> (a ** NNO) ~> x
nnoUniv a ~> x
z x ~> x
_ = Unit '() '()
Unit (a ** '()) x
(Ob a, Ob x) => Unit (a ** '()) x
U.Unit ((Ob a, Ob x) => Unit (a ** '()) x)
-> Unit a x -> Unit (a ** '()) x
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: ()) (b :: ()) r. ((Ob a, Ob b) => r) -> Unit a b -> r
\\ a ~> x
Unit a x
z

instance (HasParamNNO j, HasParamNNO k) => HasParamNNO (j, k) where
  type NNO = '(NNO, NNO)
  zero :: Unit ~> NNO
zero = Unit ~> NNO
forall k. HasParamNNO k => Unit ~> NNO
zero (Unit ~> NNO)
-> (Unit ~> NNO) -> (:**:) (~>) (~>) '(Unit, Unit) '(NNO, NNO)
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: Unit ~> NNO
forall k. HasParamNNO k => Unit ~> NNO
zero
  succ :: NNO ~> NNO
succ = NNO ~> NNO
forall k. HasParamNNO k => NNO ~> NNO
succ (NNO ~> NNO)
-> (NNO ~> NNO) -> (:**:) (~>) (~>) '(NNO, NNO) '(NNO, NNO)
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: NNO ~> NNO
forall k. HasParamNNO k => NNO ~> NNO
succ
  nnoUniv :: forall (a :: (j, k)) (x :: (j, k)).
(a ~> x) -> (x ~> x) -> (a ** NNO) ~> x
nnoUniv (a1 ~> b1
z1 :**: a2 ~> b2
z2) (a1 ~> b1
s1 :**: a2 ~> b2
s2) = (a1 ~> b1) -> (b1 ~> b1) -> (a1 ** NNO) ~> b1
forall (a :: j) (x :: j). (a ~> x) -> (x ~> x) -> (a ** NNO) ~> x
forall k (a :: k) (x :: k).
HasParamNNO k =>
(a ~> x) -> (x ~> x) -> (a ** NNO) ~> x
nnoUniv a1 ~> b1
z1 b1 ~> b1
a1 ~> b1
s1 ((a1 ** NNO) ~> b1)
-> ((a2 ** NNO) ~> b2)
-> (:**:) (~>) (~>) '(a1 ** NNO, a2 ** NNO) '(b1, b2)
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: (a2 ~> b2) -> (b2 ~> b2) -> (a2 ** NNO) ~> b2
forall (a :: k) (x :: k). (a ~> x) -> (x ~> x) -> (a ** NNO) ~> x
forall k (a :: k) (x :: k).
HasParamNNO k =>
(a ~> x) -> (x ~> x) -> (a ** NNO) ~> x
nnoUniv a2 ~> b2
z2 b2 ~> b2
a2 ~> b2
s2

instance HasParamNNO Type where
  type NNO = N.Nat
  zero :: Unit ~> NNO
zero () = Nat
N.Z
  succ :: NNO ~> NNO
succ = NNO ~> NNO
Nat -> Nat
N.S
  nnoUniv :: forall a x. (a ~> x) -> (x ~> x) -> (a ** NNO) ~> x
nnoUniv a ~> x
z x ~> x
s (a
a, Nat
n) = x -> (x -> x) -> Nat -> x
forall a. a -> (a -> a) -> Nat -> a
N.cata (a ~> x
a -> x
z a
a) x ~> x
x -> x
s Nat
n