{-# LANGUAGE AllowAmbiguousTypes #-}
{-# OPTIONS_GHC -Wno-orphans #-}

{- HLINT ignore "Use const" -}

-- | The category of __finite Haskell types__: objects are types with 'Universe'\/'Finite'
-- instances (wrapped in 'FH'), and a morphism is a function stored extensionally as a finite
-- lookup table ('Data.Map.Map'), so morphisms can be enumerated, shown and compared. A finite,
-- fully inspectable stand-in for "Proarrow.Category.Instance.Hask".
module Proarrow.Category.Instance.FinHask where

import Data.Coerce qualified as P
import Data.Containers.ListUtils (nubOrd)
import Data.Data (Proxy (..))
import Data.Kind (Type)
import Data.List (genericLength)
import Data.List qualified as P
import Data.Map.Strict (Map)
import Data.Map.Strict qualified as M
import Data.Universe.Class (Finite (..), Universe (..))
import Data.Universe.Helpers (Tagged (..), retag)
import Data.Void (Void)
import GHC.TypeNats (KnownNat, Nat, natVal, withKnownNat, withSomeSNat)
import Numeric.Natural (Natural)
import Prelude (Bool (..), ($))
import Prelude qualified as P

import Proarrow.Category.Enriched.Finitary (Finitary (..), finiteSize)
import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal (..))
import Proarrow.Category.Monoidal.Cartesian (distLProd, distRProd)
import Proarrow.Category.Monoidal.Closed (Closed (..), uncurry)
import Proarrow.Category.Monoidal.CopyDiscard (CopyDiscard)
import Proarrow.Category.Monoidal.Distributive (Distributive (..))
import Proarrow.Category.Topos (ElementaryTopos, HasEpiMonoFactorization (..), HasSubobjectClassifier (..))
import Proarrow.Colimit.BinaryCoproduct (HasBinaryCoproducts (..))
import Proarrow.Colimit.Coequalizer (HasCoequalizers (..))
import Proarrow.Colimit.Initial (HasInitialObject (..))
import Proarrow.Colimit.Pushout (HasPushouts (..))
import Proarrow.Core (CAT, CategoryOf (..), Is, Profunctor (..), Promonad (..), UN, dimapDefault)
import Proarrow.Limit.BinaryProduct
  ( HasBinaryProducts (..)
  , associatorProd
  , associatorProdInv
  , diag
  , leftUnitorProd
  , leftUnitorProdInv
  , rightUnitorProd
  , rightUnitorProdInv
  , swapProd
  )
import Proarrow.Limit.Equalizer (HasEqualizers (..))
import Proarrow.Limit.Pullback (HasPullbacks (..))
import Proarrow.Limit.Terminal (HasTerminalObject (..))
import Proarrow.Monoid (CocommutativeComonoid, Comonoid (..), Monoid (..))
import Proarrow.Profunctor.Instance.Composition ((:.:) (..))

newtype Fin (n :: Nat) = Fin {forall (n :: Nat). Fin n -> Int
unFin :: P.Int}
  deriving newtype (Fin n -> Fin n -> Bool
(Fin n -> Fin n -> Bool) -> (Fin n -> Fin n -> Bool) -> Eq (Fin n)
forall (n :: Nat). Fin n -> Fin n -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall (n :: Nat). Fin n -> Fin n -> Bool
== :: Fin n -> Fin n -> Bool
$c/= :: forall (n :: Nat). Fin n -> Fin n -> Bool
/= :: Fin n -> Fin n -> Bool
P.Eq, Eq (Fin n)
Eq (Fin n) =>
(Fin n -> Fin n -> Ordering)
-> (Fin n -> Fin n -> Bool)
-> (Fin n -> Fin n -> Bool)
-> (Fin n -> Fin n -> Bool)
-> (Fin n -> Fin n -> Bool)
-> (Fin n -> Fin n -> Fin n)
-> (Fin n -> Fin n -> Fin n)
-> Ord (Fin n)
Fin n -> Fin n -> Bool
Fin n -> Fin n -> Ordering
Fin n -> Fin n -> Fin n
forall (n :: Nat). Eq (Fin n)
forall (n :: Nat). Fin n -> Fin n -> Bool
forall (n :: Nat). Fin n -> Fin n -> Ordering
forall (n :: Nat). Fin n -> Fin n -> Fin n
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: forall (n :: Nat). Fin n -> Fin n -> Ordering
compare :: Fin n -> Fin n -> Ordering
$c< :: forall (n :: Nat). Fin n -> Fin n -> Bool
< :: Fin n -> Fin n -> Bool
$c<= :: forall (n :: Nat). Fin n -> Fin n -> Bool
<= :: Fin n -> Fin n -> Bool
$c> :: forall (n :: Nat). Fin n -> Fin n -> Bool
> :: Fin n -> Fin n -> Bool
$c>= :: forall (n :: Nat). Fin n -> Fin n -> Bool
>= :: Fin n -> Fin n -> Bool
$cmax :: forall (n :: Nat). Fin n -> Fin n -> Fin n
max :: Fin n -> Fin n -> Fin n
$cmin :: forall (n :: Nat). Fin n -> Fin n -> Fin n
min :: Fin n -> Fin n -> Fin n
P.Ord, Int -> Fin n -> ShowS
[Fin n] -> ShowS
Fin n -> String
(Int -> Fin n -> ShowS)
-> (Fin n -> String) -> ([Fin n] -> ShowS) -> Show (Fin n)
forall (n :: Nat). Int -> Fin n -> ShowS
forall (n :: Nat). [Fin n] -> ShowS
forall (n :: Nat). Fin n -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall (n :: Nat). Int -> Fin n -> ShowS
showsPrec :: Int -> Fin n -> ShowS
$cshow :: forall (n :: Nat). Fin n -> String
show :: Fin n -> String
$cshowList :: forall (n :: Nat). [Fin n] -> ShowS
showList :: [Fin n] -> ShowS
P.Show, Integer -> Fin n
Fin n -> Fin n
Fin n -> Fin n -> Fin n
(Fin n -> Fin n -> Fin n)
-> (Fin n -> Fin n -> Fin n)
-> (Fin n -> Fin n -> Fin n)
-> (Fin n -> Fin n)
-> (Fin n -> Fin n)
-> (Fin n -> Fin n)
-> (Integer -> Fin n)
-> Num (Fin n)
forall (n :: Nat). Integer -> Fin n
forall (n :: Nat). Fin n -> Fin n
forall (n :: Nat). Fin n -> Fin n -> Fin n
forall a.
(a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (Integer -> a)
-> Num a
$c+ :: forall (n :: Nat). Fin n -> Fin n -> Fin n
+ :: Fin n -> Fin n -> Fin n
$c- :: forall (n :: Nat). Fin n -> Fin n -> Fin n
- :: Fin n -> Fin n -> Fin n
$c* :: forall (n :: Nat). Fin n -> Fin n -> Fin n
* :: Fin n -> Fin n -> Fin n
$cnegate :: forall (n :: Nat). Fin n -> Fin n
negate :: Fin n -> Fin n
$cabs :: forall (n :: Nat). Fin n -> Fin n
abs :: Fin n -> Fin n
$csignum :: forall (n :: Nat). Fin n -> Fin n
signum :: Fin n -> Fin n
$cfromInteger :: forall (n :: Nat). Integer -> Fin n
fromInteger :: Integer -> Fin n
P.Num)

instance (KnownNat n) => Universe (Fin n) where
  universe :: [Fin n]
universe = forall a b. Coercible a b => a -> b
forall a b. Coercible a b => a -> b
P.coerce @[P.Int] [Int
0 .. (Nat -> Int
forall a b. (Integral a, Num b) => a -> b
P.fromIntegral (Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Nat
natVal (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n)) Int -> Int -> Int
forall a. Num a => a -> a -> a
P.- Int
1)]

instance (KnownNat n) => Finite (Fin n) where
  cardinality :: Tagged (Fin n) Nat
cardinality = Nat -> Tagged (Fin n) Nat
forall {k} (s :: k) b. b -> Tagged s b
Tagged (Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Nat
natVal (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n))

type data FINHASK = FH Type

type FinHask :: CAT FINHASK
data FinHask a b where
  FinHask :: (Ob (FH a), Ob (FH b)) => {forall a b. FinHask (FH a) (FH b) -> Map a b
unFinHask :: Map a b} -> FinHask (FH a) (FH b)

instance P.Show (FinHask a b) where
  show :: FinHask a b -> String
show (FinHask Map a b
m) = Map a b -> String
forall a. Show a => a -> String
P.show Map a b
m
deriving instance P.Eq (FinHask a b)
deriving instance P.Ord (FinHask a b)
instance (Ob a, Ob b) => Universe (FinHask a b) where
  universe :: [FinHask a b]
universe = [(UN FH a, UN FH b)] -> FinHask a b
[(UN FH a, UN FH b)] -> FinHask (FH (UN FH a)) (FH (UN FH b))
forall a b.
(Ob (FH a), Ob (FH b)) =>
[(a, b)] -> FinHask (FH a) (FH b)
fromList ([(UN FH a, UN FH b)] -> FinHask a b)
-> [[(UN FH a, UN FH b)]] -> [FinHask a b]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
P.<$> (UN FH a -> [(UN FH a, UN FH b)])
-> [UN FH a] -> [[(UN FH a, UN FH b)]]
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
P.traverse (\UN FH a
a -> (UN FH a
a,) (UN FH b -> (UN FH a, UN FH b))
-> [UN FH b] -> [(UN FH a, UN FH b)]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
P.<$> [UN FH b]
forall a. Universe a => [a]
universe) [UN FH a]
forall a. Universe a => [a]
universe
instance (Ob a, Ob b) => Finite (FinHask a b) where
  cardinality :: Tagged (FinHask a b) Nat
cardinality =
    (Nat -> Nat -> Nat)
-> Tagged (FinHask a b) Nat
-> Tagged (FinHask a b) Nat
-> Tagged (FinHask a b) Nat
forall a b c.
(a -> b -> c)
-> Tagged (FinHask a b) a
-> Tagged (FinHask a b) b
-> Tagged (FinHask a b) c
forall (f :: Type -> Type) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
P.liftA2
      Nat -> Nat -> Nat
forall a b. (Num a, Integral b) => a -> b -> a
(P.^)
      (forall {k1} {k2} (s :: k1) b (t :: k2). Tagged s b -> Tagged t b
forall s b t. Tagged s b -> Tagged t b
retag @_ @_ @(FinHask a b) (forall a. Finite a => Tagged a Nat
cardinality @(UN FH b)))
      (forall {k1} {k2} (s :: k1) b (t :: k2). Tagged s b -> Tagged t b
forall s b t. Tagged s b -> Tagged t b
retag @_ @_ @(FinHask a b) (forall a. Finite a => Tagged a Nat
cardinality @(UN FH a)))

(!) :: (P.Ord (UN FH a)) => FinHask a b -> UN FH a -> UN FH b
FinHask Map a b
m ! :: forall (a :: FINHASK) (b :: FINHASK).
Ord (UN FH a) =>
FinHask a b -> UN FH a -> UN FH b
! UN FH a
a = case a -> Map a b -> Maybe b
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup a
UN FH a
a Map a b
m of
  P.Just b
x -> b
UN FH b
x
  Maybe b
P.Nothing -> String -> UN FH b
forall a. HasCallStack => String -> a
P.error (String -> UN FH b) -> String -> UN FH b
forall a b. (a -> b) -> a -> b
$ String
"Index " String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ a -> String
forall a. Show a => a -> String
P.show a
UN FH a
a String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ String
" out of bounds for " String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ Map a b -> String
forall a. Show a => a -> String
P.show Map a b
m

arr :: (Ob (FH a), Ob (FH b)) => (a -> b) -> FinHask (FH a) (FH b)
arr :: forall a b.
(Ob (FH a), Ob (FH b)) =>
(a -> b) -> FinHask (FH a) (FH b)
arr a -> b
f = [(a, b)] -> FinHask (FH a) (FH b)
forall a b.
(Ob (FH a), Ob (FH b)) =>
[(a, b)] -> FinHask (FH a) (FH b)
fromList [(a
x, a -> b
f a
x) | a
x <- [a]
forall a. Finite a => [a]
universeF]

reifyList :: [a] -> (forall l. (Ob (FH l)) => Map l a -> r) -> r
reifyList :: forall a r. [a] -> (forall l. Ob (FH l) => Map l a -> r) -> r
reifyList [a]
xs forall l. Ob (FH l) => Map l a -> r
k =
  Nat -> (forall (n :: Nat). SNat n -> r) -> r
forall r. Nat -> (forall (n :: Nat). SNat n -> r) -> r
withSomeSNat ([a] -> Nat
forall i a. Num i => [a] -> i
genericLength [a]
xs) \ @n SNat n
snat ->
    SNat n -> (KnownNat n => r) -> r
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat SNat n
snat (forall l. Ob (FH l) => Map l a -> r
k @(Fin n) ([(Fin n, a)] -> Map (Fin n) a
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([Fin n] -> [a] -> [(Fin n, a)]
forall a b. [a] -> [b] -> [(a, b)]
P.zip [Fin n]
forall a. Finite a => [a]
universeF [a]
xs)))

fromList :: (Ob (FH a), Ob (FH b)) => [(a, b)] -> FinHask (FH a) (FH b)
fromList :: forall a b.
(Ob (FH a), Ob (FH b)) =>
[(a, b)] -> FinHask (FH a) (FH b)
fromList = Map a b -> FinHask (FH a) (FH b)
forall a b.
(Ob (FH a), Ob (FH b)) =>
Map a b -> FinHask (FH a) (FH b)
FinHask (Map a b -> FinHask (FH a) (FH b))
-> ([(a, b)] -> Map a b) -> [(a, b)] -> FinHask (FH a) (FH b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. [(a, b)] -> Map a b
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList

toList :: (Ob (FH a), Ob (FH b)) => FinHask (FH a) (FH b) -> [(a, b)]
toList :: forall a b.
(Ob (FH a), Ob (FH b)) =>
FinHask (FH a) (FH b) -> [(a, b)]
toList (FinHask Map a b
m) = Map a b -> [(a, b)]
forall k a. Map k a -> [(k, a)]
M.toList Map a b
Map a b
m

instance Profunctor FinHask where
  dimap :: forall (c :: FINHASK) (a :: FINHASK) (b :: FINHASK) (d :: FINHASK).
(c ~> a) -> (b ~> d) -> FinHask a b -> FinHask c d
dimap = (c ~> a) -> (b ~> d) -> FinHask a b -> FinHask c d
FinHask c a -> FinHask b d -> FinHask a b -> FinHask c d
forall {k} (p :: CAT 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 :: FINHASK) (b :: FINHASK) r.
((Ob a, Ob b) => r) -> FinHask a b -> r
\\ FinHask{} = r
(Ob a, Ob b) => r
r
instance Promonad FinHask where
  id :: forall (a :: FINHASK). Ob a => FinHask a a
id = (UN FH a -> UN FH a) -> FinHask (FH (UN FH a)) (FH (UN FH a))
forall a b.
(Ob (FH a), Ob (FH b)) =>
(a -> b) -> FinHask (FH a) (FH b)
arr UN FH a -> UN FH a
forall a. Ob a => a -> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id
  FinHask Map a b
l . :: forall (b :: FINHASK) (c :: FINHASK) (a :: FINHASK).
FinHask b c -> FinHask a b -> FinHask a c
. FinHask Map a b
r = Map a b -> FinHask (FH a) (FH b)
forall a b.
(Ob (FH a), Ob (FH b)) =>
Map a b -> FinHask (FH a) (FH b)
FinHask ((a -> b) -> Map a a -> Map a b
forall a b. (a -> b) -> Map a a -> Map a b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
P.fmap (Map a b
l Map a b -> a -> b
forall k a. Ord k => Map k a -> k -> a
M.!) Map a a
Map a b
r)

-- | The category of finite Haskell types, with morphisms stored extensionally as finite lookup
-- tables.
instance CategoryOf FINHASK where
  type (~>) = FinHask
  type Ob a = (Is FH a, Finite (UN FH a), P.Ord (UN FH a), P.Show (UN FH a))

instance HasInitialObject FINHASK where
  type InitialObject = FH Void
  initiate :: forall (a :: FINHASK). Ob a => InitialObject ~> a
initiate = Map Void (UN FH a) -> FinHask (FH Void) (FH (UN FH a))
forall a b.
(Ob (FH a), Ob (FH b)) =>
Map a b -> FinHask (FH a) (FH b)
FinHask Map Void (UN FH a)
forall k a. Map k a
M.empty
instance HasBinaryCoproducts FINHASK where
  type FH a || FH b = FH (P.Either a b)
  withObCoprod :: forall (a :: FINHASK) (b :: FINHASK) 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 :: FINHASK) (b :: FINHASK). (Ob a, Ob b) => a ~> (a || b)
lft = (UN FH a -> Either (UN FH a) (UN FH b))
-> FinHask (FH (UN FH a)) (FH (Either (UN FH a) (UN FH b)))
forall a b.
(Ob (FH a), Ob (FH b)) =>
(a -> b) -> FinHask (FH a) (FH b)
arr UN FH a -> Either (UN FH a) (UN FH b)
forall a b. a -> Either a b
P.Left
  rgt :: forall (a :: FINHASK) (b :: FINHASK). (Ob a, Ob b) => b ~> (a || b)
rgt = (UN FH b -> Either (UN FH a) (UN FH b))
-> FinHask (FH (UN FH b)) (FH (Either (UN FH a) (UN FH b)))
forall a b.
(Ob (FH a), Ob (FH b)) =>
(a -> b) -> FinHask (FH a) (FH b)
arr UN FH b -> Either (UN FH a) (UN FH b)
forall a b. b -> Either a b
P.Right
  FinHask Map a b
l ||| :: forall (x :: FINHASK) (a :: FINHASK) (y :: FINHASK).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| FinHask Map a b
r = Map (Either a a) b -> FinHask (FH (Either a a)) (FH b)
forall a b.
(Ob (FH a), Ob (FH b)) =>
Map a b -> FinHask (FH a) (FH b)
FinHask ((a -> Either a a) -> Map a b -> Map (Either a a) b
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
M.mapKeys a -> Either a a
forall a b. a -> Either a b
P.Left Map a b
l Map (Either a a) b -> Map (Either a a) b -> Map (Either a a) b
forall a. Semigroup a => a -> a -> a
P.<> (a -> Either a a) -> Map a b -> Map (Either a a) b
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
M.mapKeys a -> Either a a
forall a b. b -> Either a b
P.Right Map a b
Map a b
r)

instance HasTerminalObject FINHASK where
  type TerminalObject = FH ()
  terminate :: forall (a :: FINHASK). Ob a => a ~> TerminalObject
terminate = (UN FH a -> ()) -> FinHask (FH (UN FH a)) (FH ())
forall a b.
(Ob (FH a), Ob (FH b)) =>
(a -> b) -> FinHask (FH a) (FH b)
arr \UN FH a
_ -> ()
instance HasBinaryProducts FINHASK where
  type FH a && FH b = FH (a, b)
  withObProd :: forall (a :: FINHASK) (b :: FINHASK) 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 :: FINHASK) (b :: FINHASK). (Ob a, Ob b) => (a && b) ~> a
fst = ((UN FH a, UN FH b) -> UN FH a)
-> FinHask (FH (UN FH a, UN FH b)) (FH (UN FH a))
forall a b.
(Ob (FH a), Ob (FH b)) =>
(a -> b) -> FinHask (FH a) (FH b)
arr (UN FH a, UN FH b) -> UN FH a
forall a b. (a, b) -> a
P.fst
  snd :: forall (a :: FINHASK) (b :: FINHASK). (Ob a, Ob b) => (a && b) ~> b
snd = ((UN FH a, UN FH b) -> UN FH b)
-> FinHask (FH (UN FH a, UN FH b)) (FH (UN FH b))
forall a b.
(Ob (FH a), Ob (FH b)) =>
(a -> b) -> FinHask (FH a) (FH b)
arr (UN FH a, UN FH b) -> UN FH b
forall a b. (a, b) -> b
P.snd
  FinHask Map a b
l &&& :: forall (a :: FINHASK) (x :: FINHASK) (y :: FINHASK).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& FinHask Map a b
r =
    Map a (b, b) -> FinHask (FH a) (FH (b, b))
forall a b.
(Ob (FH a), Ob (FH b)) =>
Map a b -> FinHask (FH a) (FH b)
FinHask
      ( (a -> b -> b -> Maybe (b, b))
-> (Map a b -> Map a (b, b))
-> (Map a b -> Map a (b, b))
-> Map a b
-> Map a b
-> Map a (b, b)
forall k a b c.
Ord k =>
(k -> a -> b -> Maybe c)
-> (Map k a -> Map k c)
-> (Map k b -> Map k c)
-> Map k a
-> Map k b
-> Map k c
M.mergeWithKey
          (\a
_ b
a b
b -> (b, b) -> Maybe (b, b)
forall a. a -> Maybe a
P.Just (b
a, b
b))
          (\Map a b
_ -> Map a (b, b)
forall k a. Map k a
M.empty)
          (\Map a b
_ -> Map a (b, b)
forall k a. Map k a
M.empty)
          Map a b
l
          Map a b
Map a b
r
      )

instance MonoidalProfunctor FinHask where
  one :: FinHask Unit Unit
one = FinHask Unit Unit
FinHask (FH ()) (FH ())
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: FINHASK). Ob a => FinHask a a
id
  ** :: forall (x1 :: FINHASK) (x2 :: FINHASK) (y1 :: FINHASK)
       (y2 :: FINHASK).
FinHask x1 x2 -> FinHask y1 y2 -> FinHask (x1 ** y1) (x2 ** y2)
(**) = (x1 ~> x2) -> (y1 ~> y2) -> (x1 && y1) ~> (x2 && y2)
FinHask x1 x2 -> FinHask y1 y2 -> FinHask (x1 ** y1) (x2 ** y2)
forall k (a :: k) (b :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (b ~> y) -> (a && b) ~> (x && y)
forall (a :: FINHASK) (b :: FINHASK) (x :: FINHASK) (y :: FINHASK).
(a ~> x) -> (b ~> y) -> (a && b) ~> (x && y)
(***)

instance Monoidal FINHASK where
  type a ** b = a && b
  type Unit = TerminalObject
  withOb2 :: forall (a :: FINHASK) (b :: FINHASK) r.
(Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @a @b = forall k (a :: k) (b :: k) r.
(HasBinaryProducts k, Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @_ @a @b
  leftUnitor :: forall (a :: FINHASK). Ob a => (Unit ** a) ~> a
leftUnitor = (Unit ** a) ~> a
(TerminalObject && FH (UN FH a)) ~> FH (UN FH a)
forall {k} (a :: k).
(HasProducts k, Ob a) =>
(TerminalObject && a) ~> a
leftUnitorProd
  leftUnitorInv :: forall (a :: FINHASK). Ob a => a ~> (Unit ** a)
leftUnitorInv = a ~> (Unit ** a)
FH (UN FH a) ~> (TerminalObject && FH (UN FH a))
forall {k} (a :: k).
(HasProducts k, Ob a) =>
a ~> (TerminalObject && a)
leftUnitorProdInv
  rightUnitor :: forall (a :: FINHASK). Ob a => (a ** Unit) ~> a
rightUnitor = (a ** Unit) ~> a
(FH (UN FH a) && TerminalObject) ~> FH (UN FH a)
forall {k} (a :: k).
(HasProducts k, Ob a) =>
(a && TerminalObject) ~> a
rightUnitorProd
  rightUnitorInv :: forall (a :: FINHASK). Ob a => a ~> (a ** Unit)
rightUnitorInv = a ~> (a ** Unit)
FH (UN FH a) ~> (FH (UN FH a) && TerminalObject)
forall {k} (a :: k).
(HasProducts k, Ob a) =>
a ~> (a && TerminalObject)
rightUnitorProdInv
  associator :: forall (a :: FINHASK) (b :: FINHASK) (c :: FINHASK).
(Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @a @b @c = forall {k} (a :: k) (b :: k) (c :: k).
(HasBinaryProducts k, Ob a, Ob b, Ob c) =>
((a && b) && c) ~> (a && (b && c))
forall (a :: FINHASK) (b :: FINHASK) (c :: FINHASK).
(HasBinaryProducts FINHASK, Ob a, Ob b, Ob c) =>
((a && b) && c) ~> (a && (b && c))
associatorProd @a @b @c
  associatorInv :: forall (a :: FINHASK) (b :: FINHASK) (c :: FINHASK).
(Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @a @b @c = forall {k} (a :: k) (b :: k) (c :: k).
(HasBinaryProducts k, Ob a, Ob b, Ob c) =>
(a && (b && c)) ~> ((a && b) && c)
forall (a :: FINHASK) (b :: FINHASK) (c :: FINHASK).
(HasBinaryProducts FINHASK, Ob a, Ob b, Ob c) =>
(a && (b && c)) ~> ((a && b) && c)
associatorProdInv @a @b @c

instance SymMonoidal FINHASK where
  swap :: forall (a :: FINHASK) (b :: FINHASK).
(Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @a @b = forall {k} (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> (b && a)
forall (a :: FINHASK) (b :: FINHASK).
(HasBinaryProducts FINHASK, Ob a, Ob b) =>
(a && b) ~> (b && a)
swapProd @a @b

instance Closed FINHASK where
  type a ~~> b = FH (FinHask a b)
  withObExp :: forall (a :: FINHASK) (b :: FINHASK) 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 :: FINHASK) (b :: FINHASK) (c :: FINHASK).
(Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
curry f :: (a ** b) ~> c
f@FinHask{} = (UN FH a -> FinHask (FH (UN FH b)) (FH b))
-> FinHask (FH (UN FH a)) (FH (FinHask (FH (UN FH b)) (FH b)))
forall a b.
(Ob (FH a), Ob (FH b)) =>
(a -> b) -> FinHask (FH a) (FH b)
arr \UN FH a
a -> (UN FH b -> b) -> FinHask (FH (UN FH b)) (FH b)
forall a b.
(Ob (FH a), Ob (FH b)) =>
(a -> b) -> FinHask (FH a) (FH b)
arr \UN FH b
b -> (a ** b) ~> c
FinHask (FH (UN FH a, UN FH b)) (FH b)
f FinHask (FH (UN FH a, UN FH b)) (FH b)
-> UN FH (FH (UN FH a, UN FH b)) -> UN FH (FH b)
forall (a :: FINHASK) (b :: FINHASK).
Ord (UN FH a) =>
FinHask a b -> UN FH a -> UN FH b
! (UN FH a
a, UN FH b
b)
  apply :: forall (a :: FINHASK) (b :: FINHASK).
(Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
apply = ((FinHask (FH (UN FH a)) (FH (UN FH b)), UN FH a) -> UN FH b)
-> FinHask
     (FH (FinHask (FH (UN FH a)) (FH (UN FH b)), UN FH a))
     (FH (UN FH b))
forall a b.
(Ob (FH a), Ob (FH b)) =>
(a -> b) -> FinHask (FH a) (FH b)
arr ((FinHask (FH (UN FH a)) (FH (UN FH b)) ~> (UN FH a ~~> UN FH b))
-> (FinHask (FH (UN FH a)) (FH (UN FH b)) ** UN FH a) ~> UN FH b
forall {k} (b :: k) (c :: k) (a :: k).
(Closed k, Ob b, Ob c) =>
(a ~> (b ~~> c)) -> (a ** b) ~> c
uncurry FinHask (FH (UN FH a)) (FH (UN FH b)) ~> (UN FH a ~~> UN FH b)
FinHask (FH (UN FH a)) (FH (UN FH b))
-> UN FH (FH (UN FH a)) -> UN FH (FH (UN FH b))
forall (a :: FINHASK) (b :: FINHASK).
Ord (UN FH a) =>
FinHask a b -> UN FH a -> UN FH b
(!))

-- | Where a value sits in its own type's 'universe'.
position :: forall x. (Finite x, P.Eq x) => x -> Natural
position :: forall x. (Finite x, Eq x) => x -> Nat
position x
x = case x -> [x] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
P.elemIndex x
x [x]
forall a. Finite a => [a]
universeF of
  P.Just Int
i -> Int -> Nat
forall a b. (Integral a, Num b) => a -> b
P.fromIntegral Int
i
  Maybe Int
P.Nothing -> String -> Nat
forall a. HasCallStack => String -> a
P.error String
"position: not in the universe of its type"

-- | The hom-sets of 'FINHASK' are finite, so its hom-profunctor is finitary. It is numbered in the
-- order of the 'universe' the 'Finite' instance above enumerates, but arithmetically instead of by
-- searching it. A morphism is a table of values indexed by @'universeF' \@a@. Reading that table
-- as a numeral in base @|b|@, most significant digit first, gives @universe@\'s own order, since
-- @universe@ is @'P.traverse' (\a -> (a,) '<$>' universe) universe@ and for lists @'<*>'@ varies
-- its right operand fastest. So it is the /last/ element of @a@ that varies fastest.
instance Finitary FinHask where
  size :: forall (a :: FINHASK) (b :: FINHASK). (Ob a, Ob b) => Nat
size @a @b = forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Finite (p a b) =>
Nat
forall (p :: FINHASK +-> FINHASK) (a :: FINHASK) (b :: FINHASK).
Finite (p a b) =>
Nat
finiteSize @FinHask @a @b
  toIndex :: forall (a :: FINHASK) (b :: FINHASK).
(Ob a, Ob b) =>
FinHask a b -> Nat
toIndex @(FH a) @(FH b) FinHask a b
f = (Nat -> UN FH a -> Nat) -> Nat -> [UN FH a] -> Nat
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: Type -> Type) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
P.foldl (\Nat
acc UN FH a
x -> Nat
acc Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
P.* forall x. Finite x => Nat
card @b Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
P.+ UN FH b -> Nat
forall x. (Finite x, Eq x) => x -> Nat
position (FinHask a b
f FinHask a b -> UN FH a -> UN FH b
forall (a :: FINHASK) (b :: FINHASK).
Ord (UN FH a) =>
FinHask a b -> UN FH a -> UN FH b
! UN FH a
x)) Nat
0 (forall a. Finite a => [a]
universeF @a)
  fromIndex :: forall (a :: FINHASK) (b :: FINHASK).
(Ob a, Ob b) =>
Nat -> FinHask a b
fromIndex @(FH a) @(FH b) Nat
i = [(UN FH a, UN FH b)] -> FinHask (FH (UN FH a)) (FH (UN FH b))
forall a b.
(Ob (FH a), Ob (FH b)) =>
[(a, b)] -> FinHask (FH a) (FH b)
fromList ([UN FH a] -> [UN FH b] -> [(UN FH a, UN FH b)]
forall a b. [a] -> [b] -> [(a, b)]
P.zip [UN FH a]
xs (Int -> Nat -> [UN FH b]
digits ([UN FH a] -> Int
forall a. [a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
P.length [UN FH a]
xs) Nat
i))
    where
      xs :: [UN FH a]
xs = forall a. Finite a => [a]
universeF @a
      digits :: P.Int -> Natural -> [b]
      digits :: Int -> Nat -> [UN FH b]
digits Int
0 Nat
_ = []
      digits Int
n Nat
m = case forall x. Finite x => Nat
card @b of
        Nat
0 -> String -> [UN FH b]
forall a. HasCallStack => String -> a
P.error String
"fromIndex: the source is inhabited and the target is empty, so there are no morphisms"
        Nat
c -> let (Nat
q, Nat
r) = Nat
m Nat -> Nat -> (Nat, Nat)
forall a. Integral a => a -> a -> (a, a)
`P.divMod` Nat
c in Int -> Nat -> [UN FH b]
digits (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
P.- Int
1) Nat
q [UN FH b] -> [UN FH b] -> [UN FH b]
forall a. [a] -> [a] -> [a]
P.++ [forall a. Finite a => [a]
universeF @b [UN FH b] -> Nat -> UN FH b
forall i a. Integral i => [a] -> i -> a
`P.genericIndex` Nat
r]

-- | How many inhabitants a type has.
card :: forall x. (Finite x) => Natural
card :: forall x. Finite x => Nat
card = Tagged x Nat -> Nat
forall {k} (s :: k) b. Tagged s b -> b
unTagged (forall a. Finite a => Tagged a Nat
cardinality @x)

instance Distributive FINHASK where
  distL :: forall (a :: FINHASK) (b :: FINHASK) (c :: FINHASK).
(Ob a, Ob b, Ob c) =>
(a ** (b || c)) ~> ((a ** b) || (a ** c))
distL @a @b @c = forall {k} (a :: k) (b :: k) (c :: k).
(BiCCC k, Ob a, Ob b, Ob c) =>
(a && (b || c)) ~> ((a && b) || (a && c))
forall (a :: FINHASK) (b :: FINHASK) (c :: FINHASK).
(BiCCC FINHASK, Ob a, Ob b, Ob c) =>
(a && (b || c)) ~> ((a && b) || (a && c))
distLProd @a @b @c
  distR :: forall (a :: FINHASK) (b :: FINHASK) (c :: FINHASK).
(Ob a, Ob b, Ob c) =>
((a || b) ** c) ~> ((a ** c) || (b ** c))
distR @a @b @c = forall {k} (a :: k) (b :: k) (c :: k).
(BiCCC k, Ob a, Ob b, Ob c) =>
((a || b) && c) ~> ((a && c) || (b && c))
forall (a :: FINHASK) (b :: FINHASK) (c :: FINHASK).
(BiCCC FINHASK, Ob a, Ob b, Ob c) =>
((a || b) && c) ~> ((a && c) || (b && c))
distRProd @a @b @c
  absorbL :: forall (a :: FINHASK).
Ob a =>
(a ** InitialObject) ~> InitialObject
absorbL = Map (UN FH a, Void) Void -> FinHask (FH (UN FH a, Void)) (FH Void)
forall a b.
(Ob (FH a), Ob (FH b)) =>
Map a b -> FinHask (FH a) (FH b)
FinHask Map (UN FH a, Void) Void
forall k a. Map k a
M.empty
  absorbR :: forall (a :: FINHASK).
Ob a =>
(InitialObject ** a) ~> InitialObject
absorbR = Map (Void, UN FH a) Void -> FinHask (FH (Void, UN FH a)) (FH Void)
forall a b.
(Ob (FH a), Ob (FH b)) =>
Map a b -> FinHask (FH a) (FH b)
FinHask Map (Void, UN FH a) Void
forall k a. Map k a
M.empty

instance (Ob (FH a)) => Comonoid (FH a) where
  counit :: FH a ~> Unit
counit = FH a ~> Unit
FH a ~> TerminalObject
forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
forall (a :: FINHASK). Ob a => a ~> TerminalObject
terminate
  comult :: FH a ~> (FH a ** FH a)
comult = FH a ~> (FH a ** FH a)
FH a ~> (FH a && FH a)
forall {k} (a :: k). (HasBinaryProducts k, Ob a) => a ~> (a && a)
diag
instance (Ob (FH a)) => CocommutativeComonoid (FH a)

instance CopyDiscard FINHASK

instance Monoid (FH ()) where
  mempty :: Unit ~> FH ()
mempty = Unit ~> FH ()
FH () ~> TerminalObject
forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
forall (a :: FINHASK). Ob a => a ~> TerminalObject
terminate
  mappend :: (FH () ** FH ()) ~> FH ()
mappend = (FH () ** FH ()) ~> FH ()
FH ((), ()) ~> TerminalObject
forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
forall (a :: FINHASK). Ob a => a ~> TerminalObject
terminate

-- | >>> let f :: FinHask (FH (Fin 4)) (FH (Fin 3)) = fromList [(0,0), (1,1), (2,1), (3,0)]
-- >>> let g :: FinHask (FH (Fin 4)) (FH (Fin 3)) = fromList [(0,2), (1,0), (2,1), (3,0)]
-- >>> let h :: FinHask (FH (Fin 3)) (FH (Fin 4)) = fromList [(0,3), (1,2), (2,3)]
-- >>> (equalize f g \incl -> let p = factorEqualizer incl h in P.show (incl, p, incl . p)) :: P.String
-- "(fromList [(0,2),(1,3)],fromList [(0,1),(1,0),(2,1)],fromList [(0,3),(1,2),(2,3)])"
instance HasEqualizers FINHASK where
  equalize :: forall (a :: FINHASK) (b :: FINHASK) r.
(a ~> b) -> (a ~> b) -> (forall (e :: FINHASK). (e ~> a) -> r) -> r
equalize f :: a ~> b
f@FinHask{} a ~> b
g forall (e :: FINHASK). (e ~> a) -> r
k =
    let groups :: [a]
groups = [a
x | a
x <- [a]
forall a. Finite a => [a]
universeF, a ~> b
FinHask (FH a) (FH b)
f FinHask (FH a) (FH b) -> UN FH (FH a) -> UN FH (FH b)
forall (a :: FINHASK) (b :: FINHASK).
Ord (UN FH a) =>
FinHask a b -> UN FH a -> UN FH b
! a
UN FH (FH a)
x UN FH (FH b) -> UN FH (FH b) -> Bool
forall a. Eq a => a -> a -> Bool
P.== a ~> b
FinHask (FH a) (FH b)
g FinHask (FH a) (FH b) -> UN FH (FH a) -> UN FH (FH b)
forall (a :: FINHASK) (b :: FINHASK).
Ord (UN FH a) =>
FinHask a b -> UN FH a -> UN FH b
! a
UN FH (FH a)
x]
    in [a] -> (forall l. Ob (FH l) => Map l a -> r) -> r
forall a r. [a] -> (forall l. Ob (FH l) => Map l a -> r) -> r
reifyList [a]
groups \Map l a
e -> (FH l ~> a) -> r
forall (e :: FINHASK). (e ~> a) -> r
k (Map l a -> FinHask (FH l) (FH a)
forall a b.
(Ob (FH a), Ob (FH b)) =>
Map a b -> FinHask (FH a) (FH b)
FinHask Map l a
e)
  factorEqualizer :: forall (e :: FINHASK) (x :: FINHASK) (e' :: FINHASK).
(e ~> x) -> (e' ~> x) -> e' ~> e
factorEqualizer (FinHask Map a b
incl) (FinHask Map a b
h) =
    let invIncl :: Map b a
invIncl = [(b, a)] -> Map b a
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(b
v, a
ky) | (a
ky, b
v) <- Map a b -> [(a, b)]
forall k a. Map k a -> [(k, a)]
M.toList Map a b
incl]
    in Map a a -> FinHask (FH a) (FH a)
forall a b.
(Ob (FH a), Ob (FH b)) =>
Map a b -> FinHask (FH a) (FH b)
FinHask ((Map b a
invIncl Map b a -> b -> a
forall k a. Ord k => Map k a -> k -> a
M.!) (b -> a) -> Map a b -> Map a a
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
P.<$> Map a b
Map a b
h)

-- | Example 3.84 of Seven Sketches (A: 0=red, 1=blue, 2=black)
-- >>> data Color = Red | Blue | Black deriving (P.Eq, P.Ord, P.Show, P.Enum, P.Bounded, Universe, Finite)
-- >>> let f :: FinHask (FH (Fin 6)) (FH Color) = fromList [(0,Red), (1,Blue), (2,Red), (3,Red), (4,Black), (5,Blue)]
-- >>> let g :: FinHask (FH (Fin 4)) (FH Color) = fromList [(0,Black), (1,Red), (2,Blue), (3,Red)]
-- >>> (pullback f g \(FinHask l) (FinHask r) -> P.show (P.zip (M.elems l) (M.elems r))) :: P.String
-- "[(0,1),(0,3),(1,2),(2,1),(2,3),(3,1),(3,3),(4,0),(5,2)]"
instance HasPullbacks FINHASK where
  pullback :: forall (o :: FINHASK) (a :: FINHASK) (b :: FINHASK) r.
(a ~> o)
-> (b ~> o)
-> (forall (p :: FINHASK). (p ~> a) -> (p ~> b) -> r)
-> r
pullback (FinHask Map a b
f) (FinHask Map a b
g) forall (p :: FINHASK). (p ~> a) -> (p ~> b) -> r
k =
    let
      gByValue :: Map b [a]
gByValue = ([a] -> [a] -> [a]) -> [(b, [a])] -> Map b [a]
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
M.fromListWith (([a] -> [a] -> [a]) -> [a] -> [a] -> [a]
forall a b c. (a -> b -> c) -> b -> a -> c
P.flip [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
(P.++)) [(b
v, [a
y]) | (a
y, b
v) <- Map a b -> [(a, b)]
forall k a. Map k a -> [(k, a)]
M.toList Map a b
g]
      groups :: [(a, a)]
groups = [(a
x, a
y) | (a
x, b
v) <- Map a b -> [(a, b)]
forall k a. Map k a -> [(k, a)]
M.toList Map a b
f, a
y <- [a] -> b -> Map b [a] -> [a]
forall k a. Ord k => a -> k -> Map k a -> a
M.findWithDefault [] b
v Map b [a]
Map b [a]
gByValue]
    in
      [(a, a)] -> (forall l. Ob (FH l) => Map l (a, a) -> r) -> r
forall a r. [a] -> (forall l. Ob (FH l) => Map l a -> r) -> r
reifyList [(a, a)]
groups \Map l (a, a)
e -> (FH l ~> a) -> (FH l ~> b) -> r
forall (p :: FINHASK). (p ~> a) -> (p ~> b) -> r
k (Map l a -> FinHask (FH l) (FH a)
forall a b.
(Ob (FH a), Ob (FH b)) =>
Map a b -> FinHask (FH a) (FH b)
FinHask ((a, a) -> a
forall a b. (a, b) -> a
P.fst ((a, a) -> a) -> Map l (a, a) -> Map l a
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
P.<$> Map l (a, a)
e)) (Map l a -> FinHask (FH l) (FH a)
forall a b.
(Ob (FH a), Ob (FH b)) =>
Map a b -> FinHask (FH a) (FH b)
FinHask ((a, a) -> a
forall a b. (a, b) -> b
P.snd ((a, a) -> a) -> Map l (a, a) -> Map l a
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
P.<$> Map l (a, a)
e))

-- | The representative of each element after joining the given pairs: union-find, on a map of
-- parent pointers.
unionFind :: (P.Ord a) => [(a, a)] -> a -> a
unionFind :: forall a. Ord a => [(a, a)] -> a -> a
unionFind [(a, a)]
pairs = Map a a -> a -> a
forall {a}. Ord a => Map a a -> a -> a
find ((Map a a -> (a, a) -> Map a a) -> Map a a -> [(a, a)] -> Map a a
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: Type -> Type) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
P.foldl Map a a -> (a, a) -> Map a a
forall {a}. Ord a => Map a a -> (a, a) -> Map a a
union Map a a
forall k a. Map k a
M.empty [(a, a)]
pairs)
  where
    find :: Map a a -> a -> a
find Map a a
m a
i = a -> (a -> a) -> Maybe a -> a
forall b a. b -> (a -> b) -> Maybe a -> b
P.maybe a
i (Map a a -> a -> a
find Map a a
m) (a -> Map a a -> Maybe a
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup a
i Map a a
m)
    union :: Map a a -> (a, a) -> Map a a
union Map a a
m (a
i, a
j) = let ri :: a
ri = Map a a -> a -> a
forall {a}. Ord a => Map a a -> a -> a
find Map a a
m a
i; rj :: a
rj = Map a a -> a -> a
forall {a}. Ord a => Map a a -> a -> a
find Map a a
m a
j in if a
ri a -> a -> Bool
forall a. Eq a => a -> a -> Bool
P.== a
rj then Map a a
m else a -> a -> Map a a -> Map a a
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert a
ri a
rj Map a a
m

instance HasCoequalizers FINHASK where
  coequalize :: forall (a :: FINHASK) (b :: FINHASK) r.
(a ~> b) -> (a ~> b) -> (forall (c :: FINHASK). (b ~> c) -> r) -> r
coequalize (FinHask @_ @b Map a b
f) (FinHask Map a b
g) forall (c :: FINHASK). (b ~> c) -> r
k =
    let
      rep :: b -> b
rep = [(b, b)] -> b -> b
forall a. Ord a => [(a, a)] -> a -> a
unionFind ([b] -> [b] -> [(b, b)]
forall a b. [a] -> [b] -> [(a, b)]
P.zip (Map a b -> [b]
forall k a. Map k a -> [a]
M.elems Map a b
f) (Map a b -> [b]
forall k a. Map k a -> [a]
M.elems Map a b
Map a b
g))
      step :: Map b [b] -> b -> Map b [b]
step Map b [b]
m b
x = ([b] -> [b] -> [b]) -> b -> [b] -> Map b [b] -> Map b [b]
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
M.insertWith [b] -> [b] -> [b]
forall a. [a] -> [a] -> [a]
(P.++) (b -> b
rep b
x) [b
x] Map b [b]
m
      groups :: [[b]]
groups = Map b [b] -> [[b]]
forall k a. Map k a -> [a]
M.elems (Map b [b] -> [[b]]) -> Map b [b] -> [[b]]
forall a b. (a -> b) -> a -> b
$ (Map b [b] -> b -> Map b [b]) -> Map b [b] -> [b] -> Map b [b]
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: Type -> Type) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
P.foldl Map b [b] -> b -> Map b [b]
step Map b [b]
forall k a. Map k a
M.empty (forall a. Finite a => [a]
universeF @b)
    in
      [[b]] -> (forall l. Ob (FH l) => Map l [b] -> r) -> r
forall a r. [a] -> (forall l. Ob (FH l) => Map l a -> r) -> r
reifyList [[b]]
groups \Map l [b]
ce ->
        let invMap :: Map b l
invMap = [(b, l)] -> Map b l
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(b, l)] -> Map b l) -> [(b, l)] -> Map b l
forall a b. (a -> b) -> a -> b
$ ((l, [b]) -> [(b, l)]) -> [(l, [b])] -> [(b, l)]
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> [b]) -> t a -> [b]
P.concatMap (\(l
l, [b]
bs) -> (b -> (b, l)) -> [b] -> [(b, l)]
forall a b. (a -> b) -> [a] -> [b]
P.map (,l
l) [b]
bs) ([(l, [b])] -> [(b, l)]) -> [(l, [b])] -> [(b, l)]
forall a b. (a -> b) -> a -> b
$ Map l [b] -> [(l, [b])]
forall k a. Map k a -> [(k, a)]
M.toList Map l [b]
ce
        in (b ~> FH l) -> r
forall (c :: FINHASK). (b ~> c) -> r
k (Map b l -> FinHask (FH b) (FH l)
forall a b.
(Ob (FH a), Ob (FH b)) =>
Map a b -> FinHask (FH a) (FH b)
FinHask Map b l
invMap)
  factorCoequalizer :: forall (c :: FINHASK) (x :: FINHASK) (c' :: FINHASK).
(x ~> c) -> (x ~> c') -> c ~> c'
factorCoequalizer (FinHask Map a b
q) (FinHask Map a b
h) =
    let reps :: Map b a
reps = (a -> a -> a) -> [(b, a)] -> Map b a
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
M.fromListWith (\a
_ a
old -> a
old) [(b
v, a
ky) | (a
ky, b
v) <- Map a b -> [(a, b)]
forall k a. Map k a -> [(k, a)]
M.toList Map a b
q]
    in Map b b -> FinHask (FH b) (FH b)
forall a b.
(Ob (FH a), Ob (FH b)) =>
Map a b -> FinHask (FH a) (FH b)
FinHask ((Map a b
h Map a b -> a -> b
forall k a. Ord k => Map k a -> k -> a
M.!) (a -> b) -> Map b a -> Map b b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
P.<$> Map b a
Map b a
reps)

-- | Exercise 6.22 of Seven Sketches
-- >>> let l :: FinHask (FH (Fin 4)) (FH (Fin 3)) = fromList [(0,0), (1,0), (2,1), (3,2)]
-- >>> let r :: FinHask (FH (Fin 4)) (FH (Fin 5)) = fromList [(0,0), (1,2), (2,4), (3,4)]
-- >>> (pushout l r \l' r' -> P.show (l', r')) :: P.String
-- "(fromList [(0,1),(1,3),(2,3)],fromList [(0,1),(1,0),(2,1),(3,2),(4,3)])"
instance HasPushouts FINHASK

-- | >>> import Proarrow.Colimit.Pushout (isEpi)
-- >>> let f :: FinHask (FH (Fin 3)) (FH (Fin 3)) = fromList [(0,2), (1,0), (2,1)]
-- >>> (pushout f f \(FinHask g1) (FinHask g2) -> P.show (g1, g2)) :: P.String
-- "(fromList [(0,0),(1,1),(2,2)],fromList [(0,0),(1,1),(2,2)])"
-- >>> isEpi (f :: FinHask (FH (Fin 3)) (FH (Fin 3)))
-- True
-- >>> import Proarrow.Limit.Pullback (isMono)
-- >>> (pullback f f \(FinHask l) (FinHask r) -> P.show (l, r)) :: P.String
-- "(fromList [(0,0),(1,1),(2,2)],fromList [(0,0),(1,1),(2,2)])"
-- >>> isMono f
-- True
-- >>> import Proarrow.Category.Topos (classifyImage, classifyKernelPair, and, or, implies, false)
-- >>> (case factorize f of p :.: q -> P.show (p, q) \\ p \\ q) :: P.String
-- "(fromList [(0,0),(1,1),(2,2)],fromList [(0,2),(1,0),(2,1)])"
-- >>> (classifyImage f, classifyKernelPair f)
-- (fromList [(0,True),(1,True),(2,True)],fromList [((0,0),True),((0,1),False),((0,2),False),((1,0),False),((1,1),True),((1,2),False),((2,0),False),((2,1),False),((2,2),True)])
-- >>> [and, or, implies] :: [FinHask (FH (Bool, Bool)) (FH Bool)]
-- [fromList [((False,False),False),((False,True),False),((True,False),False),((True,True),True)],fromList [((False,False),False),((False,True),True),((True,False),True),((True,True),True)],fromList [((False,False),True),((False,True),True),((True,False),False),((True,True),True)]]
-- >>> false :: FinHask (FH ()) (FH Bool)
-- fromList [((),False)]
instance HasSubobjectClassifier FINHASK where
  type Omega = FH Bool
  true :: TerminalObject ~> Omega
true = (() -> Bool) -> FinHask (FH ()) (FH Bool)
forall a b.
(Ob (FH a), Ob (FH b)) =>
(a -> b) -> FinHask (FH a) (FH b)
arr \()
_ -> Bool
True
  classifyGraph :: forall (a :: FINHASK) (b :: FINHASK). (a ~> b) -> (a && b) ~> Omega
classifyGraph f :: a ~> b
f@FinHask{} = ((a, b) -> Bool) -> FinHask (FH (a, b)) (FH Bool)
forall a b.
(Ob (FH a), Ob (FH b)) =>
(a -> b) -> FinHask (FH a) (FH b)
arr \(a
a, b
b) -> a ~> b
FinHask (FH a) (FH b)
f FinHask (FH a) (FH b) -> UN FH (FH a) -> UN FH (FH b)
forall (a :: FINHASK) (b :: FINHASK).
Ord (UN FH a) =>
FinHask a b -> UN FH a -> UN FH b
! a
UN FH (FH a)
a b -> b -> Bool
forall a. Eq a => a -> a -> Bool
P.== b
b

instance HasEpiMonoFactorization FINHASK where
  factorize :: forall (a :: FINHASK) (b :: FINHASK).
(a ~> b) -> (:.:) (~>) (~>) a b
factorize (FinHask Map a b
f) = [b]
-> (forall l.
    Ob (FH l) =>
    Map l b -> (:.:) FinHask FinHask (FH a) (FH b))
-> (:.:) FinHask FinHask (FH a) (FH b)
forall a r. [a] -> (forall l. Ob (FH l) => Map l a -> r) -> r
reifyList ([b] -> [b]
forall a. Ord a => [a] -> [a]
nubOrd (Map a b -> [b]
forall k a. Map k a -> [a]
M.elems Map a b
f)) \Map l b
lb ->
    let invMap :: Map b l
invMap = [(b, l)] -> Map b l
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(Map l b
lb Map l b -> l -> b
forall k a. Ord k => Map k a -> k -> a
M.! l
l, l
l) | l
l <- [l]
forall a. Finite a => [a]
universeF]
    in Map a l -> FinHask (FH a) (FH l)
forall a b.
(Ob (FH a), Ob (FH b)) =>
Map a b -> FinHask (FH a) (FH b)
FinHask ((b -> l) -> Map a b -> Map a l
forall a b. (a -> b) -> Map a a -> Map a b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
P.fmap (Map b l
invMap Map b l -> b -> l
forall k a. Ord k => Map k a -> k -> a
M.!) Map a b
f) FinHask (FH a) (FH l)
-> FinHask (FH l) (FH b) -> (:.:) FinHask FinHask (FH a) (FH b)
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: Map l b -> FinHask (FH l) (FH b)
forall a b.
(Ob (FH a), Ob (FH b)) =>
Map a b -> FinHask (FH a) (FH b)
FinHask Map l b
lb

instance ElementaryTopos FINHASK