{-# LANGUAGE AllowAmbiguousTypes #-}

-- | Thin categories, where any two parallel arrows are equal: a 'ThinProfunctor' has at most one
-- element between any two objects, mere existence being captured by the constraint
-- @'HasArrow' p a b@. Also defines the codiscrete (always exactly one arrow) and discrete (only
-- identity arrows) special cases; 'DecidableProfunctor's, whose arrows are computed at the type
-- level as a 'BOOL' (the category thin profunctors are enriched in); and 'Indexed', 'Finite' and
-- 'Enumerable' kinds and categories, whose inhabitants are numbered, listed, and reflected to the
-- value level.
module Proarrow.Category.Enriched.Thin where

import Data.Kind (Constraint, Type)
import Data.Type.Equality (type (:~:) (..))
import Data.Type.Nat (Nat (..), SNat (..), SNatI, snat)
import Prelude (Maybe (..), type (~))

import Proarrow.Category.Instance.Bool (BOOL (..), BoolLeq, Booleans (..), NonTrivialHolds, NonTrivialProfunctor (..))
import Proarrow.Category.Instance.Zero (Bottom (..), VOID, Zero)
import Proarrow.Core (CAT, CategoryOf (..), Hom, Profunctor (..), VacuusOb, obj, type (+->))

-- | The defaults take everything from a 'DecidableProfunctor' instance: the arrow exists when
-- @'Holds' p a b@ computes to 'TRU'.
type ThinProfunctor :: forall {j} {k}. j +-> k -> Constraint
class (Profunctor p) => ThinProfunctor (p :: j +-> k) where
  type HasArrow (p :: j +-> k) (a :: k) (b :: j) :: Constraint
  type HasArrow p a b = Holds p a b ~ TRU
  arr :: (Ob a, Ob b, HasArrow p a b) => p a b
  default arr :: (Ob a, Ob b, DecidableProfunctor p, Holds p a b ~ TRU) => p a b
  arr = p a b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(DecidableProfunctor p, Ob a, Ob b, Holds p a b ~ 'TRU) =>
p a b
fromHolds
  withArr :: p a b -> ((HasArrow p a b, Ob a, Ob b) => r) -> r
  default withArr
    :: (DecidableProfunctor p, HasArrow p a b ~ (Holds p a b ~ TRU)) => p a b -> ((HasArrow p a b, Ob a, Ob b) => r) -> r
  withArr = p a b -> ((Holds p a b ~ 'TRU, Ob a, Ob b) => r) -> r
p a b -> ((HasArrow p a b, Ob a, Ob b) => r) -> r
forall (a :: k) (b :: j) r.
p a b -> ((Holds p a b ~ 'TRU, Ob a, Ob b) => r) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
DecidableProfunctor p =>
p a b -> ((Holds p a b ~ 'TRU, Ob a, Ob b) => r) -> r
toHolds

instance ThinProfunctor Zero
instance ThinProfunctor Booleans
instance (Ob ff, Ob tt) => ThinProfunctor (NonTrivialProfunctor '(ff, tt))

instance (VacuusOb k, Hom k ~ (:~:)) => ThinProfunctor ((:~:) :: CAT k) where
  type HasArrow ((:~:) :: CAT k) a b = a ~ b
  arr :: forall (a :: k) (b :: k).
(Ob a, Ob b, HasArrow (:~:) a b) =>
a :~: b
arr = a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
  withArr :: forall (a :: k) (b :: k) r.
(a :~: b) -> ((HasArrow (:~:) a b, Ob a, Ob b) => r) -> r
withArr a :~: b
Refl (HasArrow (:~:) a b, Ob a, Ob b) => r
r = r
(HasArrow (:~:) a b, Ob a, Ob b) => r
r

-- * Decidable thin profunctors

-- | The value-level shadow of a type-level 'BOOL' @h@ answering whether @p a b@ has an arrow: the
-- arrow itself when @h@ is 'TRU', nothing when it is 'FLS'.
type Decision :: forall {j} {k}. (j +-> k) -> k -> j -> BOOL -> Type
data Decision p a b h where
  Yes :: p a b -> Decision p a b TRU
  No :: Decision p a b FLS

mapDecision :: (p a b -> q c d) -> Decision p a b h -> Decision q c d h
mapDecision :: forall {k} {j} {k} {j} (p :: k -> j -> Type) (a :: k) (b :: j)
       (q :: k -> j -> Type) (c :: k) (d :: j) (h :: BOOL).
(p a b -> q c d) -> Decision p a b h -> Decision q c d h
mapDecision p a b -> q c d
f (Yes p a b
x) = q c d -> Decision q c d 'TRU
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Decision p a b 'TRU
Yes (p a b -> q c d
f p a b
x)
mapDecision p a b -> q c d
_ Decision p a b h
No = Decision q c d h
Decision q c d 'FLS
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Decision p a b 'FLS
No

-- | A thin profunctor whose arrows are decidable at the type level: @'Holds' p a b@ is the
-- 'BOOL'-valued profunctor a thin profunctor really is, computed by a type family, so it reduces to
-- 'TRU' or 'FLS' for concrete objects. It agrees with 'HasArrow' ('fromHolds' and 'toHolds' are the
-- two directions of that agreement, and the 'ThinProfunctor' defaults make it definitional), and
-- 'decide' computes the answer at the value level, arrow included. This is what lets a composite of
-- thin profunctors search for its middle object ("Proarrow.Category.Enriched.Thin.Composition").
type DecidableProfunctor :: forall {j} {k}. j +-> k -> Constraint
class (ThinProfunctor p) => DecidableProfunctor (p :: j +-> k) where
  type Holds (p :: j +-> k) (a :: k) (b :: j) :: BOOL
  decide :: (Ob a, Ob b) => Decision p a b (Holds p a b)
  toHolds :: p a b -> ((Holds p a b ~ TRU, Ob a, Ob b) => r) -> r

fromHolds :: forall {j} {k} (p :: j +-> k) a b. (DecidableProfunctor p, Ob a, Ob b, Holds p a b ~ TRU) => p a b
fromHolds :: forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(DecidableProfunctor p, Ob a, Ob b, Holds p a b ~ 'TRU) =>
p a b
fromHolds = case forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(DecidableProfunctor p, Ob a, Ob b) =>
Decision p a b (Holds p a b)
forall (p :: j +-> k) (a :: k) (b :: j).
(DecidableProfunctor p, Ob a, Ob b) =>
Decision p a b (Holds p a b)
decide @p @a @b of Yes p a b
x -> p a b
x

-- | A profunctor that decides against an arrow has none, so a caller holding one may return anything.
noArrow :: forall {j} {k} (p :: j +-> k) a b r. (DecidableProfunctor p, Holds p a b ~ FLS) => p a b -> r
noArrow :: forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
(DecidableProfunctor p, Holds p a b ~ 'FLS) =>
p a b -> r
noArrow p a b
x = case Holds p a b :~: 'TRU
eq of {}
  where
    eq :: Holds p a b :~: TRU
    eq :: Holds p a b :~: 'TRU
eq = p a b
-> ((Holds p a b ~ 'TRU, Ob a, Ob b) => 'FLS :~: 'TRU)
-> 'FLS :~: 'TRU
forall (a :: k) (b :: j) r.
p a b -> ((Holds p a b ~ 'TRU, Ob a, Ob b) => r) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
DecidableProfunctor p =>
p a b -> ((Holds p a b ~ 'TRU, Ob a, Ob b) => r) -> r
toHolds p a b
x 'FLS :~: 'FLS
'FLS :~: 'TRU
(Holds p a b ~ 'TRU, Ob a, Ob b) => 'FLS :~: 'TRU
forall {k} (a :: k). a :~: a
Refl

-- | A thin category whose order is decidable at the type level.
class (DecidableProfunctor (Hom k), CategoryOf k) => Decidable k

instance (DecidableProfunctor (Hom k), CategoryOf k) => Decidable k

instance DecidableProfunctor Zero where
  type Holds Zero a b = FLS
  decide :: forall (a :: VOID) (b :: VOID).
(Ob a, Ob b) =>
Decision Zero a b (Holds Zero a b)
decide = Decision Zero a b 'FLS
Decision Zero a b (Holds Zero a b)
forall a. Bottom => a
forall a. a
no
  toHolds :: forall (a :: VOID) (b :: VOID) r.
Zero a b -> ((Holds Zero a b ~ 'TRU, Ob a, Ob b) => r) -> r
toHolds = \case {}

instance DecidableProfunctor Booleans where
  type Holds Booleans a b = BoolLeq a b
  decide :: forall (a :: BOOL) (b :: BOOL).
(Ob a, Ob b) =>
Decision Booleans a b (Holds Booleans a b)
decide @a @b = case (forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: BOOL). (CategoryOf BOOL, Ob a) => Obj a
obj @a, forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: BOOL). (CategoryOf BOOL, Ob a) => Obj a
obj @b) of
    (Booleans a a
Fls, Booleans b b
Fls) -> Booleans a b -> Decision Booleans a b 'TRU
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Decision p a b 'TRU
Yes Booleans a b
Booleans 'FLS 'FLS
Fls
    (Booleans a a
Fls, Booleans b b
Tru) -> Booleans a b -> Decision Booleans a b 'TRU
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Decision p a b 'TRU
Yes Booleans a b
Booleans 'FLS 'TRU
F2T
    (Booleans a a
Tru, Booleans b b
Tru) -> Booleans a b -> Decision Booleans a b 'TRU
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Decision p a b 'TRU
Yes Booleans a b
Booleans 'TRU 'TRU
Tru
    (Booleans a a
Tru, Booleans b b
Fls) -> Decision Booleans a b 'FLS
Decision Booleans a b (Holds Booleans a b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Decision p a b 'FLS
No
  toHolds :: forall (a :: BOOL) (b :: BOOL) r.
Booleans a b -> ((Holds Booleans a b ~ 'TRU, Ob a, Ob b) => r) -> r
toHolds Booleans a b
Fls (Holds Booleans a b ~ 'TRU, Ob a, Ob b) => r
r = r
(Holds Booleans a b ~ 'TRU, Ob a, Ob b) => r
r
  toHolds Booleans a b
F2T (Holds Booleans a b ~ 'TRU, Ob a, Ob b) => r
r = r
(Holds Booleans a b ~ 'TRU, Ob a, Ob b) => r
r
  toHolds Booleans a b
Tru (Holds Booleans a b ~ 'TRU, Ob a, Ob b) => r
r = r
(Holds Booleans a b ~ 'TRU, Ob a, Ob b) => r
r

instance (Ob ff, Ob tt) => DecidableProfunctor (NonTrivialProfunctor '(ff, tt)) where
  type Holds (NonTrivialProfunctor '(ff, tt)) a b = NonTrivialHolds ff tt a b
  decide :: forall (a :: BOOL) (b :: BOOL).
(Ob a, Ob b) =>
Decision
  (NonTrivialProfunctor '(ff, tt))
  a
  b
  (Holds (NonTrivialProfunctor '(ff, tt)) a b)
decide @a @b = case (forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: BOOL). (CategoryOf BOOL, Ob a) => Obj a
obj @a, forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: BOOL). (CategoryOf BOOL, Ob a) => Obj a
obj @b) of
    (Booleans a a
Fls, Booleans b b
Fls) -> case forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: BOOL). (CategoryOf BOOL, Ob a) => Obj a
obj @ff of
      Obj ff
Booleans ff ff
Fls -> Decision (NonTrivialProfunctor '(ff, tt)) a b 'FLS
Decision
  (NonTrivialProfunctor '(ff, tt))
  a
  b
  (Holds (NonTrivialProfunctor '(ff, tt)) a b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Decision p a b 'FLS
No
      Obj ff
Booleans ff ff
Tru -> NonTrivialProfunctor '(ff, tt) a b
-> Decision (NonTrivialProfunctor '(ff, tt)) a b 'TRU
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Decision p a b 'TRU
Yes NonTrivialProfunctor '(ff, tt) a b
NonTrivialProfunctor '( 'TRU, tt) 'FLS 'FLS
forall (tt :: BOOL). NonTrivialProfunctor '( 'TRU, tt) 'FLS 'FLS
FF
    (Booleans a a
Fls, Booleans b b
Tru) -> NonTrivialProfunctor '(ff, tt) a b
-> Decision (NonTrivialProfunctor '(ff, tt)) a b 'TRU
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Decision p a b 'TRU
Yes NonTrivialProfunctor '(ff, tt) a b
NonTrivialProfunctor '(ff, tt) 'FLS 'TRU
forall (ft :: (BOOL, BOOL)). NonTrivialProfunctor ft 'FLS 'TRU
FT
    (Booleans a a
Tru, Booleans b b
Tru) -> case forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: BOOL). (CategoryOf BOOL, Ob a) => Obj a
obj @tt of
      Obj tt
Booleans tt tt
Fls -> Decision (NonTrivialProfunctor '(ff, tt)) a b 'FLS
Decision
  (NonTrivialProfunctor '(ff, tt))
  a
  b
  (Holds (NonTrivialProfunctor '(ff, tt)) a b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Decision p a b 'FLS
No
      Obj tt
Booleans tt tt
Tru -> NonTrivialProfunctor '(ff, tt) a b
-> Decision (NonTrivialProfunctor '(ff, tt)) a b 'TRU
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Decision p a b 'TRU
Yes NonTrivialProfunctor '(ff, tt) a b
NonTrivialProfunctor '(ff, 'TRU) 'TRU 'TRU
forall (ff :: BOOL). NonTrivialProfunctor '(ff, 'TRU) 'TRU 'TRU
TT
    (Booleans a a
Tru, Booleans b b
Fls) -> Decision (NonTrivialProfunctor '(ff, tt)) a b 'FLS
Decision
  (NonTrivialProfunctor '(ff, tt))
  a
  b
  (Holds (NonTrivialProfunctor '(ff, tt)) a b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Decision p a b 'FLS
No
  toHolds :: forall (a :: BOOL) (b :: BOOL) r.
NonTrivialProfunctor '(ff, tt) a b
-> ((Holds (NonTrivialProfunctor '(ff, tt)) a b ~ 'TRU, Ob a,
     Ob b) =>
    r)
-> r
toHolds NonTrivialProfunctor '(ff, tt) a b
FF (Holds (NonTrivialProfunctor '(ff, tt)) a b ~ 'TRU, Ob a, Ob b) =>
r
r = r
(Holds (NonTrivialProfunctor '(ff, tt)) a b ~ 'TRU, Ob a, Ob b) =>
r
r
  toHolds NonTrivialProfunctor '(ff, tt) a b
FT (Holds (NonTrivialProfunctor '(ff, tt)) a b ~ 'TRU, Ob a, Ob b) =>
r
r = r
(Holds (NonTrivialProfunctor '(ff, tt)) a b ~ 'TRU, Ob a, Ob b) =>
r
r
  toHolds NonTrivialProfunctor '(ff, tt) a b
TT (Holds (NonTrivialProfunctor '(ff, tt)) a b ~ 'TRU, Ob a, Ob b) =>
r
r = r
(Holds (NonTrivialProfunctor '(ff, tt)) a b ~ 'TRU, Ob a, Ob b) =>
r
r

class (ThinProfunctor (Hom k), CategoryOf k) => Thin k
instance (ThinProfunctor (Hom k), CategoryOf k) => Thin k

class (ThinProfunctor p, Ob a, Ob b, HasArrow p a b) => HasArrow' p a b where arr' :: p a b
instance (ThinProfunctor p, Ob a, Ob b, HasArrow p a b) => HasArrow' p a b where arr' :: p a b
arr' = p a b
forall (a :: k) (b :: j). (Ob a, Ob b, HasArrow p a b) => p a b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(ThinProfunctor p, Ob a, Ob b, HasArrow p a b) =>
p a b
arr

type CodiscreteProfunctor :: forall {j} {k}. j +-> k -> Constraint
class
  (ThinProfunctor p, forall c d. (Ob c, Ob d) => HasArrow' p c d, Codiscrete j, Codiscrete k) =>
  CodiscreteProfunctor (p :: j +-> k)
  where
  anyArr :: (Ob a, Ob b) => p a b
instance
  (ThinProfunctor p, forall c d. (Ob c, Ob d) => HasArrow' p c d, Codiscrete j, Codiscrete k)
  => CodiscreteProfunctor (p :: j +-> k)
  where
  anyArr :: forall (a :: k) (b :: j). (Ob a, Ob b) => p a b
anyArr = p a b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
HasArrow' p a b =>
p a b
arr'

type Codiscrete k = CodiscreteProfunctor (Hom k)

class ((c) => d, (d) => c) => c <=> d
instance ((c) => d, (d) => c) => c <=> d

class ((HasArrow p a b) => Bottom) => HasNoArrow p a b where
  arrowIsBottomProof :: (HasArrow p a b) => r
instance ((HasArrow p a b) => Bottom) => HasNoArrow p a b where
  arrowIsBottomProof :: forall r. HasArrow p a b => r
arrowIsBottomProof = r
forall a. Bottom => a
forall a. a
no

type DiscreteProfunctor :: forall {j} {k}. j +-> k -> Constraint
class (ThinProfunctor p, forall a b. (Ob a, Ob b) => HasNoArrow p a b) => DiscreteProfunctor (p :: j +-> k) where
  exfalso :: p a b -> r
instance (ThinProfunctor p, forall a b. (Ob a, Ob b) => HasNoArrow p a b) => DiscreteProfunctor (p :: j +-> k) where
  exfalso :: forall (a :: k) (b :: j) r. p a b -> r
exfalso @a @b p a b
p = p a b -> ((HasArrow p a b, Ob a, Ob b) => r) -> r
forall (a :: k) (b :: j) r.
p a b -> ((HasArrow p a b, Ob a, Ob b) => r) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
ThinProfunctor p =>
p a b -> ((HasArrow p a b, Ob a, Ob b) => r) -> r
withArr p a b
p (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
(HasNoArrow p a b, HasArrow p a b) =>
r
forall (p :: j +-> k) (a :: k) (b :: j) r.
(HasNoArrow p a b, HasArrow p a b) =>
r
arrowIsBottomProof @p @a @b)

class ((HasArrow (Hom k) c d) <=> (c ~ d)) => ArrowIsId k c d where
  arrowIsIdProof :: (HasArrow (Hom k) c d) => ((c ~ d) => r) -> r
instance ((HasArrow (Hom k) c d) <=> (c ~ d)) => ArrowIsId k c d where
  arrowIsIdProof :: forall r. HasArrow (Hom k) c d => ((c ~ d) => r) -> r
arrowIsIdProof (c ~ d) => r
r = r
(c ~ d) => r
r

-- | Note: @Discrete k@ is not the same as @DiscreteProfunctor (Hom k)@!
class (Thin k, forall c d. (Ob c, Ob d) => ArrowIsId k c d) => Discrete k where
  withEq :: (a :: k) ~> b -> ((a ~ b) => r) -> r

instance (Thin k, forall c d. (Ob c, Ob d) => ArrowIsId k c d) => Discrete k where
  withEq :: forall (a :: k) (b :: k) r. (a ~> b) -> ((a ~ b) => r) -> r
withEq @a @b a ~> b
f (a ~ b) => r
r = (a ~> b) -> ((HasArrow (Hom k) a b, Ob a, Ob b) => r) -> r
forall (a :: k) (b :: k) r.
(a ~> b) -> ((HasArrow (Hom k) a b, Ob a, Ob b) => r) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
ThinProfunctor p =>
p a b -> ((HasArrow p a b, Ob a, Ob b) => r) -> r
withArr a ~> b
f (forall k (c :: k) (d :: k) r.
(ArrowIsId k c d, HasArrow (Hom k) c d) =>
((c ~ d) => r) -> r
arrowIsIdProof @k @a @b r
(a ~ b) => r
r)

-- * Indexed, finite and enumerable kinds

-- | A kind whose inhabitants are numbered: 'Index' gives each its position and 'At' reads it back,
-- so that two inhabitants are equal exactly when their indices are ('decideEq'). 'At' is partial, so
-- that finitely many inhabitants can be numbered by an initial segment of the naturals.
class Indexed k where
  type Index (a :: k) :: Nat

  -- | A 'Finite' kind is numbered by its own object list: this default and the one for 'At' are
  -- inverse walks of 'Objects', so an instance that lists its inhabitants need say nothing here.
  type Index (a :: k) = IndexOf a (Objects k)

  type At k (i :: Nat) :: Maybe k
  type At k i = Lookup (Objects k) i

-- | The evidence that @a@ is numbered: its index, reflected, and 'At' reading it back.
class (SNatI (Index a), At k (Index a) ~ 'Just a) => KnownIndex (a :: k)

instance (SNatI (Index a), At k (Index a) ~ 'Just a) => KnownIndex (a :: k)

instance Indexed Nat where
  type Index n = n
  type At Nat i = 'Just i

-- | Equality of naturals, with evidence either way.
type NatEq :: Nat -> Nat -> BOOL
type family NatEq n m where
  NatEq 'Z 'Z = TRU
  NatEq ('S n) ('S m) = NatEq n m
  NatEq n m = FLS

natEq :: SNat n -> SNat m -> Decision (:~:) n m (NatEq n m)
natEq :: forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> Decision (:~:) n m (NatEq n m)
natEq SNat n
SZ SNat m
SZ = (n :~: m) -> Decision (:~:) n m 'TRU
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Decision p a b 'TRU
Yes n :~: m
m :~: m
forall {k} (a :: k). a :~: a
Refl
natEq (SS @n) (SS @m) = ((n1 :~: n1) -> n :~: m)
-> Decision (:~:) n1 n1 (NatEq n1 n1)
-> Decision (:~:) n m (NatEq n1 n1)
forall {k} {j} {k} {j} (p :: k -> j -> Type) (a :: k) (b :: j)
       (q :: k -> j -> Type) (c :: k) (d :: j) (h :: BOOL).
(p a b -> q c d) -> Decision p a b h -> Decision q c d h
mapDecision (\n1 :~: n1
Refl -> n :~: m
m :~: m
forall {k} (a :: k). a :~: a
Refl) (SNat n1 -> SNat n1 -> Decision (:~:) n1 n1 (NatEq n1 n1)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> Decision (:~:) n m (NatEq n m)
natEq (forall (n :: Nat). SNatI n => SNat n
snat @n) (forall (n :: Nat). SNatI n => SNat n
snat @m))
natEq SNat n
SZ SNat m
SS = Decision (:~:) n m 'FLS
Decision (:~:) n m (NatEq n m)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Decision p a b 'FLS
No
natEq SNat n
SS SNat m
SZ = Decision (:~:) n m 'FLS
Decision (:~:) n m (NatEq n m)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Decision p a b 'FLS
No

withNatEqRefl :: forall n r. SNat n -> ((NatEq n n ~ TRU) => r) -> r
withNatEqRefl :: forall (n :: Nat) r. SNat n -> ((NatEq n n ~ 'TRU) => r) -> r
withNatEqRefl SNat n
SZ (NatEq n n ~ 'TRU) => r
r = r
(NatEq n n ~ 'TRU) => r
r
withNatEqRefl (SS @n') (NatEq n n ~ 'TRU) => r
r = SNat n1 -> ((NatEq n1 n1 ~ 'TRU) => r) -> r
forall (n :: Nat) r. SNat n -> ((NatEq n n ~ 'TRU) => r) -> r
withNatEqRefl (forall (n :: Nat). SNatI n => SNat n
snat @n') r
(NatEq n n ~ 'TRU) => r
(NatEq n1 n1 ~ 'TRU) => r
r

-- | Two numbered inhabitants are equal exactly when their indices are.
type Equal (a :: k) (b :: k) = NatEq (Index a) (Index b)

decideEq :: forall {k} (a :: k) b. (KnownIndex a, KnownIndex b) => Decision (:~:) a b (Equal a b)
decideEq :: forall {k} (a :: k) (b :: k).
(KnownIndex a, KnownIndex b) =>
Decision (:~:) a b (Equal a b)
decideEq = case SNat (Index a)
-> SNat (Index b) -> Decision (:~:) (Index a) (Index b) (Equal a b)
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> Decision (:~:) n m (NatEq n m)
natEq (forall (n :: Nat). SNatI n => SNat n
snat @(Index a)) (forall (n :: Nat). SNatI n => SNat n
snat @(Index b)) of
  Yes Index a :~: Index b
Refl -> (a :~: b) -> Decision (:~:) a b 'TRU
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Decision p a b 'TRU
Yes a :~: b
b :~: b
forall {k} (a :: k). a :~: a
Refl
  Decision (:~:) (Index a) (Index b) (Equal a b)
No -> Decision (:~:) a b 'FLS
Decision (:~:) a b (Equal a b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Decision p a b 'FLS
No

type Length :: [k] -> Nat
type family Length xs where
  Length '[] = 'Z
  Length (x ': xs) = 'S (Length xs)

type Lookup :: [k] -> Nat -> Maybe k
type family Lookup xs i where
  Lookup '[] i = 'Nothing
  Lookup (x ': xs) 'Z = 'Just x
  Lookup (x ': xs) ('S i) = Lookup xs i

-- | The inhabitant at an index in a type-level list known to be long enough: 'Lookup' without the
-- 'Maybe', for tables indexed by 'Index'. Out of range it is stuck rather than 'Nothing'.
type Entry :: [k] -> Nat -> k
type family Entry xs i where
  Entry (x ': xs) 'Z = x
  Entry (x ': xs) ('S i) = Entry xs i

-- | Every entry of @xs@ satisfies @c@. The list is shaped like @shape@, a list of objects, so that
-- an index into @shape@ selects an entry of @xs@. The equality argument ties the index to @shape@,
-- so that walking off the end is refutable rather than an error.
type KnownList :: forall {x} {y}. (x -> Constraint) -> [y] -> [x] -> Constraint
class KnownList c shape xs where
  withEntry :: forall s i r. SNat i -> Lookup shape i :~: 'Just s -> ((c (Entry xs i)) => r) -> r

instance KnownList c '[] '[] where
  withEntry :: forall (s :: y) (i :: Nat) r.
SNat i -> (Lookup '[] i :~: 'Just s) -> (c (Entry '[] i) => r) -> r
withEntry SNat i
_ Lookup '[] i :~: 'Just s
eq c (Entry '[] i) => r
_ = case Lookup '[] i :~: 'Just s
eq of {}

instance (c x, KnownList c shape xs) => KnownList c (s ': shape) (x ': xs) where
  withEntry :: forall (s :: y) (i :: Nat) r.
SNat i
-> (Lookup (s : shape) i :~: 'Just s)
-> (c (Entry (x : xs) i) => r)
-> r
withEntry SNat i
SZ Lookup (s : shape) i :~: 'Just s
Refl c (Entry (x : xs) i) => r
r = r
c (Entry (x : xs) i) => r
r
  withEntry (SS @i') Lookup (s : shape) i :~: 'Just s
eq c (Entry (x : xs) i) => r
r = forall {x} {y} (c :: x -> Constraint) (shape :: [y]) (xs :: [x])
       (s :: y) (i :: Nat) r.
KnownList c shape xs =>
SNat i
-> (Lookup shape i :~: 'Just s) -> (c (Entry xs i) => r) -> r
forall (c :: a -> Constraint) (shape :: [y]) (xs :: [a]) (s :: y)
       (i :: Nat) r.
KnownList c shape xs =>
SNat i
-> (Lookup shape i :~: 'Just s) -> (c (Entry xs i) => r) -> r
withEntry @c @shape @xs (forall (n :: Nat). SNatI n => SNat n
snat @i') Lookup shape n1 :~: 'Just s
Lookup (s : shape) i :~: 'Just s
eq r
c (Entry xs n1) => r
c (Entry (x : xs) i) => r
r

-- | Where an inhabitant sits in a type-level list, the inverse of 'Lookup'. An inhabitant that does
-- not occur has no index, so the family is stuck rather than total.
type IndexOf :: forall k. k -> [k] -> Nat
type family IndexOf a xs where
  IndexOf a (a ': xs) = 'Z
  IndexOf a (b ': xs) = 'S (IndexOf a xs)

-- | A type-level list of inhabitants, reflected to the value level with their indices.
type IndexedList :: forall k. [k] -> Type
data IndexedList as where
  FNil :: IndexedList '[]
  FCons :: forall a as. (KnownIndex a) => IndexedList as -> IndexedList (a ': as)

-- | Every element of the list is numbered, so the list can be reflected to an 'IndexedList'. This
-- is what lets a kind that simply writes its objects out give 'finite' for free.
class HasFiniteDefault (xs :: [k]) where
  finiteDefault :: IndexedList xs

instance HasFiniteDefault '[] where
  finiteDefault :: IndexedList '[]
finiteDefault = IndexedList '[]
forall k. IndexedList '[]
FNil
instance (KnownIndex a, HasFiniteDefault as) => HasFiniteDefault (a ': as) where
  finiteDefault :: IndexedList (a : as)
finiteDefault = IndexedList as -> IndexedList (a : as)
forall {k} (a :: k) (as :: [k]).
KnownIndex a =>
IndexedList as -> IndexedList (a : as)
FCons IndexedList as
forall k (xs :: [k]). HasFiniteDefault xs => IndexedList xs
finiteDefault

-- | An 'Indexed' kind with finitely many inhabitants, listed in 'Objects' in the order of their
-- indices: 'withAtLookup' says that the list tabulates 'At'.
class (Indexed k) => Finite k where
  type Objects k :: [k]
  finite :: IndexedList (Objects k)
  default finite :: (HasFiniteDefault (Objects k)) => IndexedList (Objects k)
  finite = IndexedList (Objects k)
forall k (xs :: [k]). HasFiniteDefault xs => IndexedList xs
finiteDefault
  withAtLookup :: forall (i :: Nat) r. SNat i -> ((Lookup (Objects k) i ~ At k i) => r) -> r
  default withAtLookup
    :: forall (i :: Nat) r. (At k i ~ Lookup (Objects k) i) => SNat i -> ((Lookup (Objects k) i ~ At k i) => r) -> r
  withAtLookup SNat i
_ (Lookup (Objects k) i ~ At k i) => r
r = r
(Lookup (Objects k) i ~ At k i) => r
r

-- | A proof that @a@ occurs in the type-level list @as@.
type Member :: forall k. k -> [k] -> Type
data Member a as where
  Here :: Member a (a ': as)
  There :: Member a as -> Member a (b ': as)

-- | Every numbered inhabitant of a finite kind occurs in its list: walk to its index.
memberIndex :: forall {k} (a :: k). (Finite k, KnownIndex a) => Member a (Objects k)
memberIndex :: forall {k} (a :: k).
(Finite k, KnownIndex a) =>
Member a (Objects k)
memberIndex = forall k (i :: Nat) r.
Finite k =>
SNat i -> ((Lookup (Objects k) i ~ At k i) => r) -> r
withAtLookup @k (forall (n :: Nat). SNatI n => SNat n
snat @(Index a)) (SNat (Index a) -> IndexedList (Objects k) -> Member a (Objects k)
forall (i :: Nat) (xs :: [k]).
(Lookup xs i ~ 'Just a) =>
SNat i -> IndexedList xs -> Member a xs
go (forall (n :: Nat). SNatI n => SNat n
snat @(Index a)) (forall k. Finite k => IndexedList (Objects k)
finite @k))
  where
    go :: forall i xs. (Lookup xs i ~ 'Just a) => SNat i -> IndexedList xs -> Member a xs
    go :: forall (i :: Nat) (xs :: [k]).
(Lookup xs i ~ 'Just a) =>
SNat i -> IndexedList xs -> Member a xs
go SNat i
SZ (FCons IndexedList as
_) = Member a xs
Member a (a : as)
forall {a} (a :: a) (a :: [a]). Member a (a : a)
Here
    go (SS @i') (FCons IndexedList as
xs) = Member a as -> Member a (a : as)
forall {k} (a :: k) (a :: [k]) (as :: k).
Member a a -> Member a (as : a)
There (SNat n1 -> IndexedList as -> Member a as
forall (i :: Nat) (xs :: [k]).
(Lookup xs i ~ 'Just a) =>
SNat i -> IndexedList xs -> Member a xs
go (forall (n :: Nat). SNatI n => SNat n
snat @i') IndexedList as
xs)

-- | A category on a 'Finite' kind whose objects are exactly its numbered inhabitants: 'withIndex'
-- and 'withOb' convert between the two notions, and 'atOb' looks an object up by its index.
type Enumerable :: Type -> Constraint
class (CategoryOf k, Finite k) => Enumerable k where
  withIndex :: forall (a :: k) r. (Ob a) => ((KnownIndex a) => r) -> r
  withOb :: forall (a :: k) r. (KnownIndex a) => ((Ob a) => r) -> r
  withOb @x Ob a => r
r = case forall k (i :: Nat). Enumerable k => SNat i -> AtOb k (At k i)
atOb @k (forall (n :: Nat). SNatI n => SNat n
snat @(Index x)) of AtOb k (At k (Index a))
AtJust -> r
Ob a => r
r

  -- | The object at an index, if there is one. The default walks the object list, which is all a
  -- kind in general can do. A kind that can answer from the index alone should say so, and a wrapper
  -- kind whose base is itself 'Enumerable' should defer to it -- which the discrete kinds cannot,
  -- since they ask only that the kind they wrap be 'Finite'.
  atOb :: forall (i :: Nat). SNat i -> AtOb k (At k i)
  atOb SNat i
i = forall k (i :: Nat) r.
Finite k =>
SNat i -> ((Lookup (Objects k) i ~ At k i) => r) -> r
withAtLookup @k SNat i
i (forall k (j :: Nat) (xs :: [k]).
Enumerable k =>
SNat j -> IndexedList xs -> AtOb k (Lookup xs j)
lookupOb @k SNat i
i (forall k. Finite k => IndexedList (Objects k)
finite @k))

  {-# MINIMAL withIndex, (atOb | withOb) #-}

-- | Locate an object in the object list.
member :: forall {k} (a :: k). (Enumerable k, Ob a) => Member a (Objects k)
member :: forall {k} (a :: k). (Enumerable k, Ob a) => Member a (Objects k)
member = forall k (a :: k) r.
(Enumerable k, Ob a) =>
(KnownIndex a => r) -> r
withIndex @k @a (forall (a :: k). (Finite k, KnownIndex a) => Member a (Objects k)
forall {k} (a :: k).
(Finite k, KnownIndex a) =>
Member a (Objects k)
memberIndex @a)

-- | Whether the inhabitant at an index exists, and if so that it is an object. Indexed by the lookup
-- itself, so that a caller holding @'At' k i ~ ''Just' a@ learns @'Ob' a@ -- which is what a wrapper
-- kind needs to recover the objects of the kind it wraps.
type AtOb :: forall k -> Maybe k -> Type
data AtOb k x where
  AtNothing :: AtOb k 'Nothing
  AtJust :: (Ob a, KnownIndex a) => AtOb k ('Just a)

-- | A numbered inhabitant is found at its own index, so evidence that nothing is there refutes
-- itself: under @'KnownIndex' a@ the argument's type is @''Just' a ':~:' ''Nothing'@, and a caller
-- holding one may return anything.
noIndex :: forall {k} (a :: k) r. (KnownIndex a) => At k (Index a) :~: 'Nothing -> r
noIndex :: forall {k} (a :: k) r.
KnownIndex a =>
(At k (Index a) :~: 'Nothing) -> r
noIndex At k (Index a) :~: 'Nothing
eq = case At k (Index a) :~: 'Nothing
eq of {}

-- | A kind that wraps another, one inhabitant for one, keeps its numbering: map the wrapper over the
-- lookup ('FmapWrap') and over the object list ('MapWrap'), and the two agree ('withLookupMapWrap').
type FmapWrap :: forall {j} {k}. (j -> k) -> Maybe j -> Maybe k
type family FmapWrap w x where
  FmapWrap w 'Nothing = 'Nothing
  FmapWrap w ('Just a) = 'Just (w a)

type MapWrap :: forall {j} {k}. (j -> k) -> [j] -> [k]
type family MapWrap w xs where
  MapWrap w '[] = '[]
  MapWrap w (x ': xs) = w x ': MapWrap w xs

mapWrap
  :: forall {j} {k} (w :: j -> k) xs
   . (forall (a :: j). (KnownIndex a) => KnownIndex (w a))
  => IndexedList xs -> IndexedList (MapWrap w xs)
mapWrap :: forall {j} {k} (w :: j -> k) (xs :: [j]).
(forall (a :: j). KnownIndex a => KnownIndex (w a)) =>
IndexedList xs -> IndexedList (MapWrap w xs)
mapWrap IndexedList xs
FNil = IndexedList '[]
IndexedList (MapWrap w xs)
forall k. IndexedList '[]
FNil
mapWrap (FCons @a IndexedList as
xs) = forall (a :: k) (as :: [k]).
KnownIndex a =>
IndexedList as -> IndexedList (a : as)
forall {k} (a :: k) (as :: [k]).
KnownIndex a =>
IndexedList as -> IndexedList (a : as)
FCons @(w a) (forall {j} {k} (w :: j -> k) (xs :: [j]).
(forall (a :: j). KnownIndex a => KnownIndex (w a)) =>
IndexedList xs -> IndexedList (MapWrap w xs)
forall (w :: j -> k) (xs :: [j]).
(forall (a :: j). KnownIndex a => KnownIndex (w a)) =>
IndexedList xs -> IndexedList (MapWrap w xs)
mapWrap @w IndexedList as
xs)

withLookupMapWrap
  :: forall {j} {k} (w :: j -> k) xs i r
   . SNat i -> IndexedList xs -> ((Lookup (MapWrap w xs) i ~ FmapWrap w (Lookup xs i)) => r) -> r
withLookupMapWrap :: forall {j} {k} (w :: j -> k) (xs :: [j]) (i :: Nat) r.
SNat i
-> IndexedList xs
-> ((Lookup (MapWrap w xs) i ~ FmapWrap w (Lookup xs i)) => r)
-> r
withLookupMapWrap SNat i
_ IndexedList xs
FNil (Lookup (MapWrap w xs) i ~ FmapWrap w (Lookup xs i)) => r
r = r
(Lookup (MapWrap w xs) i ~ FmapWrap w (Lookup xs i)) => r
r
withLookupMapWrap SNat i
SZ (FCons IndexedList as
_) (Lookup (MapWrap w xs) i ~ FmapWrap w (Lookup xs i)) => r
r = r
(Lookup (MapWrap w xs) i ~ FmapWrap w (Lookup xs i)) => r
r
withLookupMapWrap (SS @i') (FCons IndexedList as
xs) (Lookup (MapWrap w xs) i ~ FmapWrap w (Lookup xs i)) => r
r = forall {j} {k} (w :: j -> k) (xs :: [j]) (i :: Nat) r.
SNat i
-> IndexedList xs
-> ((Lookup (MapWrap w xs) i ~ FmapWrap w (Lookup xs i)) => r)
-> r
forall (w :: j -> k) (xs :: [j]) (i :: Nat) r.
SNat i
-> IndexedList xs
-> ((Lookup (MapWrap w xs) i ~ FmapWrap w (Lookup xs i)) => r)
-> r
withLookupMapWrap @w (forall (n :: Nat). SNatI n => SNat n
snat @i') IndexedList as
xs r
(Lookup (MapWrap w xs) i ~ FmapWrap w (Lookup xs i)) => r
(Lookup (MapWrap w as) n1 ~ FmapWrap w (Lookup as n1)) => r
r

-- | The two 'Finite' methods of a wrapper kind, which are the same for every wrapper.
wrapFinite
  :: forall {j} {k} (w :: j -> k)
   . (Finite j, forall (a :: j). (KnownIndex a) => KnownIndex (w a))
  => IndexedList (MapWrap w (Objects j))
wrapFinite :: forall {j} {k} (w :: j -> k).
(Finite j, forall (a :: j). KnownIndex a => KnownIndex (w a)) =>
IndexedList (MapWrap w (Objects j))
wrapFinite = forall {j} {k} (w :: j -> k) (xs :: [j]).
(forall (a :: j). KnownIndex a => KnownIndex (w a)) =>
IndexedList xs -> IndexedList (MapWrap w xs)
forall (w :: j -> k) (xs :: [j]).
(forall (a :: j). KnownIndex a => KnownIndex (w a)) =>
IndexedList xs -> IndexedList (MapWrap w xs)
mapWrap @w (forall k. Finite k => IndexedList (Objects k)
finite @j)

withWrapAtLookup
  :: forall {j} {k} (w :: j -> k) i r
   . (Finite j)
  => SNat i -> ((Lookup (MapWrap w (Objects j)) i ~ FmapWrap w (At j i)) => r) -> r
withWrapAtLookup :: forall {j} {k} (w :: j -> k) (i :: Nat) r.
Finite j =>
SNat i
-> ((Lookup (MapWrap w (Objects j)) i ~ FmapWrap w (At j i)) => r)
-> r
withWrapAtLookup SNat i
i (Lookup (MapWrap w (Objects j)) i ~ FmapWrap w (At j i)) => r
r = forall k (i :: Nat) r.
Finite k =>
SNat i -> ((Lookup (Objects k) i ~ At k i) => r) -> r
withAtLookup @j SNat i
i (forall {j} {k} (w :: j -> k) (xs :: [j]) (i :: Nat) r.
SNat i
-> IndexedList xs
-> ((Lookup (MapWrap w xs) i ~ FmapWrap w (Lookup xs i)) => r)
-> r
forall (w :: j -> k) (xs :: [j]) (i :: Nat) r.
SNat i
-> IndexedList xs
-> ((Lookup (MapWrap w xs) i ~ FmapWrap w (Lookup xs i)) => r)
-> r
withLookupMapWrap @w SNat i
i (forall k. Finite k => IndexedList (Objects k)
finite @j) r
(Lookup (MapWrap w (Objects j)) i ~ FmapWrap w (At j i)) => r
(Lookup (MapWrap w (Objects j)) i
 ~ FmapWrap w (Lookup (Objects j) i)) =>
r
r)

-- | The default 'atOb': walk the object list to the index.
lookupOb :: forall k (j :: Nat) xs. (Enumerable k) => SNat j -> IndexedList (xs :: [k]) -> AtOb k (Lookup xs j)
lookupOb :: forall k (j :: Nat) (xs :: [k]).
Enumerable k =>
SNat j -> IndexedList xs -> AtOb k (Lookup xs j)
lookupOb SNat j
_ IndexedList xs
FNil = AtOb k 'Nothing
AtOb k (Lookup xs j)
forall k. AtOb k 'Nothing
AtNothing
lookupOb SNat j
SZ (FCons @a IndexedList as
_) = forall k (a :: k) r.
(Enumerable k, KnownIndex a) =>
(Ob a => r) -> r
withOb @k @a AtOb k ('Just a)
Ob a => AtOb k ('Just a)
forall k (a :: k). (Ob a, KnownIndex a) => AtOb k ('Just a)
AtJust
lookupOb (SS @j') (FCons IndexedList as
xs) = forall k (j :: Nat) (xs :: [k]).
Enumerable k =>
SNat j -> IndexedList xs -> AtOb k (Lookup xs j)
lookupOb @k (forall (n :: Nat). SNatI n => SNat n
snat @j') IndexedList as
xs

instance Indexed BOOL

instance Finite BOOL where type Objects BOOL = '[FLS, TRU]

instance Enumerable BOOL where
  withIndex :: forall (a :: BOOL) r. Ob a => (KnownIndex a => r) -> r
withIndex @a KnownIndex a => r
r = case forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: BOOL). (CategoryOf BOOL, Ob a) => Obj a
obj @a of
    Obj a
Booleans a a
Fls -> r
KnownIndex a => r
r
    Obj a
Booleans a a
Tru -> r
KnownIndex a => r
r
  withOb :: forall (a :: BOOL) r. KnownIndex a => (Ob a => r) -> r
withOb @a Ob a => r
r = case forall (n :: Nat). SNatI n => SNat n
snat @(Index a) of
    SNat (Index a)
SZ -> r
Ob a => r
r
    SS @i -> case forall (n :: Nat). SNatI n => SNat n
snat @i of SNat n1
SZ -> r
Ob a => r
r

-- | The empty kind has no inhabitants to number.
instance Indexed VOID where
  type Index (a :: VOID) = 'Z
  type At VOID i = 'Nothing

instance Finite VOID where type Objects VOID = '[]

instance Enumerable VOID where
  withIndex :: forall (a :: VOID) r. Ob a => (KnownIndex a => r) -> r
withIndex KnownIndex a => r
_ = r
forall a. Bottom => a
forall a. a
no
  withOb :: forall (a :: VOID) r. KnownIndex a => (Ob a => r) -> r
withOb @a Ob a => r
_ = forall {k} (a :: k) r.
KnownIndex a =>
(At k (Index a) :~: 'Nothing) -> r
forall (a :: VOID) r.
KnownIndex a =>
(At VOID (Index a) :~: 'Nothing) -> r
noIndex @a 'Nothing :~: 'Nothing
At VOID (Index a) :~: 'Nothing
forall {k} (a :: k). a :~: a
Refl