proarrow
Safe HaskellNone
LanguageGHC2024

Proarrow.Category.Enriched.Thin

Description

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; DecidableProfunctors, 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.

Synopsis

Documentation

class Profunctor p => ThinProfunctor (p :: j +-> k) where Source Github #

The defaults take everything from a DecidableProfunctor instance: the arrow exists when Holds p a b computes to TRU.

Minimal complete definition

Nothing

Associated Types

type HasArrow (p :: j +-> k) (a :: k) (b :: j) Source Github #

type HasArrow (p :: j +-> k) (a :: k) (b :: j) = Holds p a b ~ 'TRU

Methods

arr :: forall (a :: k) (b :: j). (Ob a, Ob b, HasArrow p a b) => p a b Source Github #

default arr :: forall (a :: k) (b :: j). (Ob a, Ob b, DecidableProfunctor p, Holds p a b ~ 'TRU) => p a b Source Github #

withArr :: forall (a :: k) (b :: j) r. p a b -> ((HasArrow p a b, Ob a, Ob b) => r) -> r Source Github #

default withArr :: forall (a :: k) (b :: j) r. (DecidableProfunctor p, HasArrow p a b ~ (Holds p a b ~ 'TRU)) => p a b -> ((HasArrow p a b, Ob a, Ob b) => r) -> r Source Github #

Instances

Instances details
ThinProfunctor Booleans Source Github # 
Instance details

Defined in Proarrow.Category.Enriched.Thin

Associated Types

type HasArrow Booleans (a :: BOOL) (b :: BOOL) 
Instance details

Defined in Proarrow.Category.Enriched.Thin

type HasArrow Booleans (a :: BOOL) (b :: BOOL) = Holds Booleans a b ~ 'TRU

Methods

arr :: forall (a :: BOOL) (b :: BOOL). (Ob a, Ob b, HasArrow Booleans a b) => Booleans a b Source Github #

withArr :: forall (a :: BOOL) (b :: BOOL) r. Booleans a b -> ((HasArrow Booleans a b, Ob a, Ob b) => r) -> r Source Github #

ThinProfunctor (:-) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Constraint

Associated Types

type HasArrow (:-) (a :: CONSTRAINT) (b :: CONSTRAINT) 
Instance details

Defined in Proarrow.Category.Instance.Constraint

type HasArrow (:-) (a :: CONSTRAINT) (b :: CONSTRAINT) = UN 'CNSTRNT a :=> UN 'CNSTRNT b

Methods

arr :: forall (a :: CONSTRAINT) (b :: CONSTRAINT). (Ob a, Ob b, HasArrow (:-) a b) => a :- b Source Github #

withArr :: forall (a :: CONSTRAINT) (b :: CONSTRAINT) r. (a :- b) -> ((HasArrow (:-) a b, Ob a, Ob b) => r) -> r Source Github #

ThinProfunctor GTE Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Cost

Associated Types

type HasArrow GTE (a :: COST) (b :: COST) 
Instance details

Defined in Proarrow.Category.Instance.Cost

type HasArrow GTE (a :: COST) (b :: COST) = Holds GTE a b ~ 'TRU

Methods

arr :: forall (a :: COST) (b :: COST). (Ob a, Ob b, HasArrow GTE a b) => GTE a b Source Github #

withArr :: forall (a :: COST) (b :: COST) r. GTE a b -> ((HasArrow GTE a b, Ob a, Ob b) => r) -> r Source Github #

ThinProfunctor Zero Source Github # 
Instance details

Defined in Proarrow.Category.Enriched.Thin

Associated Types

type HasArrow Zero (a :: VOID) (b :: VOID) 
Instance details

Defined in Proarrow.Category.Enriched.Thin

type HasArrow Zero (a :: VOID) (b :: VOID) = Holds Zero a b ~ 'TRU

Methods

arr :: forall (a :: VOID) (b :: VOID). (Ob a, Ob b, HasArrow Zero a b) => Zero a b Source Github #

withArr :: forall (a :: VOID) (b :: VOID) r. Zero a b -> ((HasArrow Zero a b, Ob a, Ob b) => r) -> r Source Github #

ThinProfunctor Unit Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Unit

Associated Types

type HasArrow Unit (a :: ()) (b :: ()) 
Instance details

Defined in Proarrow.Category.Instance.Unit

type HasArrow Unit (a :: ()) (b :: ()) = a ~ b

Methods

arr :: forall (a :: ()) (b :: ()). (Ob a, Ob b, HasArrow Unit a b) => Unit a b Source Github #

withArr :: forall (a :: ()) (b :: ()) r. Unit a b -> ((HasArrow Unit a b, Ob a, Ob b) => r) -> r Source Github #

(Ob ff, Ob tt) => ThinProfunctor (NonTrivialProfunctor '(ff, tt) :: BOOL -> BOOL -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Enriched.Thin

Methods

arr :: forall (a :: BOOL) (b :: BOOL). (Ob a, Ob b, HasArrow (NonTrivialProfunctor '(ff, tt)) a b) => NonTrivialProfunctor '(ff, tt) a b Source Github #

withArr :: forall (a :: BOOL) (b :: BOOL) r. NonTrivialProfunctor '(ff, tt) a b -> ((HasArrow (NonTrivialProfunctor '(ff, tt)) a b, Ob a, Ob b) => r) -> r Source Github #

(VacuousOb k, Hom k ~ ((:~:) :: k -> k -> Type)) => ThinProfunctor ((:~:) :: k -> k -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Enriched.Thin

Methods

arr :: forall (a :: k) (b :: k). (Ob a, Ob b, HasArrow ((:~:) :: k -> k -> Type) a b) => a :~: b Source Github #

withArr :: forall (a :: k) (b :: k) r. (a :~: b) -> ((HasArrow ((:~:) :: k -> k -> Type) a b, Ob a, Ob b) => r) -> r Source Github #

Thin k => ThinProfunctor (Id :: k -> k -> Type) Source Github # 
Instance details

Defined in Proarrow.Profunctor.Instance.Identity

Methods

arr :: forall (a :: k) (b :: k). (Ob a, Ob b, HasArrow (Id :: k -> k -> Type) a b) => Id a b Source Github #

withArr :: forall (a :: k) (b :: k) r. Id a b -> ((HasArrow (Id :: k -> k -> Type) a b, Ob a, Ob b) => r) -> r Source Github #

(Thin j, Thin k) => ThinProfunctor (InitialProfunctor :: k -> j -> Type) Source Github # 
Instance details

Defined in Proarrow.Profunctor.Instance.Initial

Methods

arr :: forall (a :: k) (b :: j). (Ob a, Ob b, HasArrow (InitialProfunctor :: k -> j -> Type) a b) => InitialProfunctor a b Source Github #

withArr :: forall (a :: k) (b :: j) r. InitialProfunctor a b -> ((HasArrow (InitialProfunctor :: k -> j -> Type) a b, Ob a, Ob b) => r) -> r Source Github #

(CategoryOf j, CategoryOf k) => ThinProfunctor (TerminalProfunctor :: k -> j -> Type) Source Github # 
Instance details

Defined in Proarrow.Profunctor.Instance.Terminal

Methods

arr :: forall (a :: k) (b :: j). (Ob a, Ob b, HasArrow (TerminalProfunctor :: k -> j -> Type) a b) => TerminalProfunctor a b Source Github #

withArr :: forall (a :: k) (b :: j) r. TerminalProfunctor a b -> ((HasArrow (TerminalProfunctor :: k -> j -> Type) a b, Ob a, Ob b) => r) -> r Source Github #

(Thin j, Thin k, ThinProfunctor p) => ThinProfunctor (UnOp p :: k -> j -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Opposite

Methods

arr :: forall (a :: k) (b :: j). (Ob a, Ob b, HasArrow (UnOp p) a b) => UnOp p a b Source Github #

withArr :: forall (a :: k) (b :: j) r. UnOp p a b -> ((HasArrow (UnOp p) a b, Ob a, Ob b) => r) -> r Source Github #

Relation p => ThinProfunctor (Converse p :: k -> j -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Rel

Methods

arr :: forall (a :: k) (b :: j). (Ob a, Ob b, HasArrow (Converse p) a b) => Converse p a b Source Github #

withArr :: forall (a :: k) (b :: j) r. Converse p a b -> ((HasArrow (Converse p) a b, Ob a, Ob b) => r) -> r Source Github #

(FunctorForRep f, Thin j) => ThinProfunctor (Corep f :: k -> j -> Type) Source Github #

Corep f a b holds in a thin category exactly when f a ≤ b.

Instance details

Defined in Proarrow.Profunctor.Corepresentable

Methods

arr :: forall (a :: k) (b :: j). (Ob a, Ob b, HasArrow (Corep f) a b) => Corep f a b Source Github #

withArr :: forall (a :: k) (b :: j) r. Corep f a b -> ((HasArrow (Corep f) a b, Ob a, Ob b) => r) -> r Source Github #

(Functor f, Thin j) => ThinProfunctor (Costar f :: k -> j -> Type) Source Github # 
Instance details

Defined in Proarrow.Profunctor.Instance.Costar

Methods

arr :: forall (a :: k) (b :: j). (Ob a, Ob b, HasArrow (Costar f) a b) => Costar f a b Source Github #

withArr :: forall (a :: k) (b :: j) r. Costar f a b -> ((HasArrow (Costar f) a b, Ob a, Ob b) => r) -> r Source Github #

(Functor f, Thin k) => ThinProfunctor (Star f :: k -> j -> Type) Source Github # 
Instance details

Defined in Proarrow.Profunctor.Instance.Star

Methods

arr :: forall (a :: k) (b :: j). (Ob a, Ob b, HasArrow (Star f) a b) => Star f a b Source Github #

withArr :: forall (a :: k) (b :: j) r. Star f a b -> ((HasArrow (Star f) a b, Ob a, Ob b) => r) -> r Source Github #

(Corepresentable p, Thin k) => ThinProfunctor (CorepStar p :: k -> j -> Type) Source Github #

CorepStar p a b holds in a thin category exactly when a ≤ p %% b.

Instance details

Defined in Proarrow.Profunctor.Representable

Methods

arr :: forall (a :: k) (b :: j). (Ob a, Ob b, HasArrow (CorepStar p) a b) => CorepStar p a b Source Github #

withArr :: forall (a :: k) (b :: j) r. CorepStar p a b -> ((HasArrow (CorepStar p) a b, Ob a, Ob b) => r) -> r Source Github #

(FunctorForRep f, Thin k) => ThinProfunctor (Rep f :: k -> j -> Type) Source Github # 
Instance details

Defined in Proarrow.Profunctor.Representable

Methods

arr :: forall (a :: k) (b :: j). (Ob a, Ob b, HasArrow (Rep f) a b) => Rep f a b Source Github #

withArr :: forall (a :: k) (b :: j) r. Rep f a b -> ((HasArrow (Rep f) a b, Ob a, Ob b) => r) -> r Source Github #

(Representable p, Thin j) => ThinProfunctor (RepCostar p :: k -> j -> Type) Source Github # 
Instance details

Defined in Proarrow.Profunctor.Representable

Methods

arr :: forall (a :: k) (b :: j). (Ob a, Ob b, HasArrow (RepCostar p) a b) => RepCostar p a b Source Github #

withArr :: forall (a :: k) (b :: j) r. RepCostar p a b -> ((HasArrow (RepCostar p) a b, Ob a, Ob b) => r) -> r Source Github #

(SNatI n, DecidableProfunctor p, Decidable k, Enumerable k) => ThinProfunctor (Walk n p :: k -> k -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Enriched.Thin.Composition

Methods

arr :: forall (a :: k) (b :: k). (Ob a, Ob b, HasArrow (Walk n p) a b) => Walk n p a b Source Github #

withArr :: forall (a :: k) (b :: k) r. Walk n p a b -> ((HasArrow (Walk n p) a b, Ob a, Ob b) => r) -> r Source Github #

(ThinProfunctor p, ThinProfunctor q, Discrete j, Discrete k) => ThinProfunctor (p :~>: q :: k -> j -> Type) Source Github # 
Instance details

Defined in Proarrow.Profunctor.Instance.Exponential

Methods

arr :: forall (a :: k) (b :: j). (Ob a, Ob b, HasArrow (p :~>: q) a b) => (p :~>: q) a b Source Github #

withArr :: forall (a :: k) (b :: j) r. (p :~>: q) a b -> ((HasArrow (p :~>: q) a b, Ob a, Ob b) => r) -> r Source Github #

(ThinProfunctor p, ThinProfunctor q) => ThinProfunctor (p :*: q :: k -> j -> Type) Source Github # 
Instance details

Defined in Proarrow.Profunctor.Instance.Product

Methods

arr :: forall (a :: k) (b :: j). (Ob a, Ob b, HasArrow (p :*: q) a b) => (p :*: q) a b Source Github #

withArr :: forall (a :: k) (b :: j) r. (p :*: q) a b -> ((HasArrow (p :*: q) a b, Ob a, Ob b) => r) -> r Source Github #

(Thin k, FunctorForRep f, FunctorForRep g) => ThinProfunctor (Direp f g :: j -> i -> Type) Source Github # 
Instance details

Defined in Proarrow.Profunctor.Instance.Direp

Methods

arr :: forall (a :: j) (b :: i). (Ob a, Ob b, HasArrow (Direp f g) a b) => Direp f g a b Source Github #

withArr :: forall (a :: j) (b :: i) r. Direp f g a b -> ((HasArrow (Direp f g) a b, Ob a, Ob b) => r) -> r Source Github #

ComposeThin (ThinCompStrategy p q) p q => ThinProfunctor (p :.: q :: k -> j2 -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Enriched.Thin.Composition

Methods

arr :: forall (a :: k) (b :: j2). (Ob a, Ob b, HasArrow (p :.: q) a b) => (p :.: q) a b Source Github #

withArr :: forall (a :: k) (b :: j2) r. (p :.: q) a b -> ((HasArrow (p :.: q) a b, Ob a, Ob b) => r) -> r Source Github #

Indexed k => ThinProfunctor (Codiscrete :: CODISCRETE k -> CODISCRETE k -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Discrete

Methods

arr :: forall (a :: CODISCRETE k) (b :: CODISCRETE k). (Ob a, Ob b, HasArrow (Codiscrete :: CODISCRETE k -> CODISCRETE k -> Type) a b) => Codiscrete a b Source Github #

withArr :: forall (a :: CODISCRETE k) (b :: CODISCRETE k) r. Codiscrete a b -> ((HasArrow (Codiscrete :: CODISCRETE k -> CODISCRETE k -> Type) a b, Ob a, Ob b) => r) -> r Source Github #

Indexed k => ThinProfunctor (Discrete :: DISCRETE k -> DISCRETE k -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Discrete

Methods

arr :: forall (a :: DISCRETE k) (b :: DISCRETE k). (Ob a, Ob b, HasArrow (Discrete :: DISCRETE k -> DISCRETE k -> Type) a b) => Discrete a b Source Github #

withArr :: forall (a :: DISCRETE k) (b :: DISCRETE k) r. Discrete a b -> ((HasArrow (Discrete :: DISCRETE k -> DISCRETE k -> Type) a b, Ob a, Ob b) => r) -> r Source Github #

ThinProfunctor (LTE :: ORDINAL n -> ORDINAL n -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Ordinal

Methods

arr :: forall (a :: ORDINAL n) (b :: ORDINAL n). (Ob a, Ob b, HasArrow (LTE :: ORDINAL n -> ORDINAL n -> Type) a b) => LTE a b Source Github #

withArr :: forall (a :: ORDINAL n) (b :: ORDINAL n) r. LTE a b -> ((HasArrow (LTE :: ORDINAL n -> ORDINAL n -> Type) a b, Ob a, Ob b) => r) -> r Source Github #

(Indexed k, KnownEdges es) => ThinProfunctor (Edges es :: DISCRETE k -> DISCRETE k -> Type) Source Github #

A graph with BOOL weights is a relation on the points: decided by walking the edge list.

Instance details

Defined in Proarrow.Profunctor.Instance.Edges

Methods

arr :: forall (a :: DISCRETE k) (b :: DISCRETE k). (Ob a, Ob b, HasArrow (Edges es) a b) => Edges es a b Source Github #

withArr :: forall (a :: DISCRETE k) (b :: DISCRETE k) r. Edges es a b -> ((HasArrow (Edges es) a b, Ob a, Ob b) => r) -> r Source Github #

ThinProfunctor p => ThinProfunctor (Op p :: OPPOSITE j -> OPPOSITE k -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Opposite

Methods

arr :: forall (a :: OPPOSITE j) (b :: OPPOSITE k). (Ob a, Ob b, HasArrow (Op p) a b) => Op p a b Source Github #

withArr :: forall (a :: OPPOSITE j) (b :: OPPOSITE k) r. Op p a b -> ((HasArrow (Op p) a b, Ob a, Ob b) => r) -> r Source Github #

(ThinProfunctor p, Promonad p) => ThinProfunctor (Kleisli :: KLEISLI p -> KLEISLI p -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Kleisli

Methods

arr :: forall (a :: KLEISLI p) (b :: KLEISLI p). (Ob a, Ob b, HasArrow (Kleisli :: KLEISLI p -> KLEISLI p -> Type) a b) => Kleisli a b Source Github #

withArr :: forall (a :: KLEISLI p) (b :: KLEISLI p) r. Kleisli a b -> ((HasArrow (Kleisli :: KLEISLI p -> KLEISLI p -> Type) a b, Ob a, Ob b) => r) -> r Source Github #

(ThinProfunctor p, ThinProfunctor q) => ThinProfunctor (p :**: q :: (k1, k2) -> (j1, j2) -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Product

Methods

arr :: forall (a :: (k1, k2)) (b :: (j1, j2)). (Ob a, Ob b, HasArrow (p :**: q) a b) => (p :**: q) a b Source Github #

withArr :: forall (a :: (k1, k2)) (b :: (j1, j2)) r. (p :**: q) a b -> ((HasArrow (p :**: q) a b, Ob a, Ob b) => r) -> r Source Github #

(Thin j, Thin k, ThinProfunctor p) => ThinProfunctor (Collage :: COLLAGE p -> COLLAGE p -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Collage

Methods

arr :: forall (a :: COLLAGE p) (b :: COLLAGE p). (Ob a, Ob b, HasArrow (Collage :: COLLAGE p -> COLLAGE p -> Type) a b) => Collage a b Source Github #

withArr :: forall (a :: COLLAGE p) (b :: COLLAGE p) r. Collage a b -> ((HasArrow (Collage :: COLLAGE p -> COLLAGE p -> Type) a b, Ob a, Ob b) => r) -> r Source Github #

Decidable thin profunctors

data Decision (p :: j +-> k) (a :: k) (b :: j) (h :: BOOL) where Source Github #

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.

Constructors

Yes :: forall {j} {k} (p :: j +-> k) (a :: k) (b :: j). p a b -> Decision p a b 'TRU 
No :: forall {j} {k} (p :: j +-> k) (a :: k) (b :: j). Decision p a b 'FLS 

mapDecision :: forall {k1} {j1} {k2} {j2} p (a :: k1) (b :: j1) q (c :: k2) (d :: j2) (h :: BOOL). (p a b -> q c d) -> Decision p a b h -> Decision q c d h Source Github #

class ThinProfunctor p => DecidableProfunctor (p :: j +-> k) where Source Github #

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. With it a composite of thin profunctors can search for its middle object (Proarrow.Category.Enriched.Thin.Composition).

Associated Types

type Holds (p :: j +-> k) (a :: k) (b :: j) :: BOOL Source Github #

Methods

decide :: forall (a :: k) (b :: j). (Ob a, Ob b) => Decision p a b (Holds p a b) Source Github #

toHolds :: forall (a :: k) (b :: j) r. p a b -> ((Holds p a b ~ 'TRU, Ob a, Ob b) => r) -> r Source Github #

Instances

Instances details
DecidableProfunctor Booleans Source Github # 
Instance details

Defined in Proarrow.Category.Enriched.Thin

Associated Types

type Holds Booleans (a :: BOOL) (b :: BOOL) 
Instance details

Defined in Proarrow.Category.Enriched.Thin

type Holds Booleans (a :: BOOL) (b :: BOOL) = BoolLeq a b

Methods

decide :: forall (a :: BOOL) (b :: BOOL). (Ob a, Ob b) => Decision Booleans a b (Holds Booleans a b) Source Github #

toHolds :: forall (a :: BOOL) (b :: BOOL) r. Booleans a b -> ((Holds Booleans a b ~ 'TRU, Ob a, Ob b) => r) -> r Source Github #

DecidableProfunctor GTE Source Github #

Decided by comparing the naturals; INF is below everything.

Instance details

Defined in Proarrow.Category.Instance.Cost

Associated Types

type Holds GTE ('C a :: COST) ('C b :: COST) 
Instance details

Defined in Proarrow.Category.Instance.Cost

type Holds GTE ('C a :: COST) ('C b :: COST) = FromBool (b <=? a)
type Holds GTE ('C a :: COST) 'INF 
Instance details

Defined in Proarrow.Category.Instance.Cost

type Holds GTE ('C a :: COST) 'INF = 'FLS
type Holds GTE 'INF (b :: COST) 
Instance details

Defined in Proarrow.Category.Instance.Cost

type Holds GTE 'INF (b :: COST) = 'TRU

Methods

decide :: forall (a :: COST) (b :: COST). (Ob a, Ob b) => Decision GTE a b (Holds GTE a b) Source Github #

toHolds :: forall (a :: COST) (b :: COST) r. GTE a b -> ((Holds GTE a b ~ 'TRU, Ob a, Ob b) => r) -> r Source Github #

DecidableProfunctor Zero Source Github # 
Instance details

Defined in Proarrow.Category.Enriched.Thin

Associated Types

type Holds Zero (a :: VOID) (b :: VOID) 
Instance details

Defined in Proarrow.Category.Enriched.Thin

type Holds Zero (a :: VOID) (b :: VOID) = 'FLS

Methods

decide :: forall (a :: VOID) (b :: VOID). (Ob a, Ob b) => Decision Zero a b (Holds Zero a b) Source Github #

toHolds :: forall (a :: VOID) (b :: VOID) r. Zero a b -> ((Holds Zero a b ~ 'TRU, Ob a, Ob b) => r) -> r Source Github #

DecidableProfunctor Unit Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Unit

Associated Types

type Holds Unit (a :: ()) (b :: ()) 
Instance details

Defined in Proarrow.Category.Instance.Unit

type Holds Unit (a :: ()) (b :: ()) = 'TRU

Methods

decide :: forall (a :: ()) (b :: ()). (Ob a, Ob b) => Decision Unit a b (Holds Unit a b) Source Github #

toHolds :: forall (a :: ()) (b :: ()) r. Unit a b -> ((Holds Unit a b ~ 'TRU, Ob a, Ob b) => r) -> r Source Github #

(Ob ff, Ob tt) => DecidableProfunctor (NonTrivialProfunctor '(ff, tt) :: BOOL -> BOOL -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Enriched.Thin

Methods

decide :: forall (a :: BOOL) (b :: BOOL). (Ob a, Ob b) => Decision (NonTrivialProfunctor '(ff, tt)) a b (Holds (NonTrivialProfunctor '(ff, tt)) a b) Source Github #

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 Source Github #

DecidableProfunctor (Hom k) => DecidableProfunctor (Id :: k -> k -> Type) Source Github # 
Instance details

Defined in Proarrow.Profunctor.Instance.Identity

Methods

decide :: forall (a :: k) (b :: k). (Ob a, Ob b) => Decision (Id :: k -> k -> Type) a b (Holds (Id :: k -> k -> Type) a b) Source Github #

toHolds :: forall (a :: k) (b :: k) r. Id a b -> ((Holds (Id :: k -> k -> Type) a b ~ 'TRU, Ob a, Ob b) => r) -> r Source Github #

(Thin j, Thin k) => DecidableProfunctor (InitialProfunctor :: k -> j -> Type) Source Github # 
Instance details

Defined in Proarrow.Profunctor.Instance.Initial

Methods

decide :: forall (a :: k) (b :: j). (Ob a, Ob b) => Decision (InitialProfunctor :: k -> j -> Type) a b (Holds (InitialProfunctor :: k -> j -> Type) a b) Source Github #

toHolds :: forall (a :: k) (b :: j) r. InitialProfunctor a b -> ((Holds (InitialProfunctor :: k -> j -> Type) a b ~ 'TRU, Ob a, Ob b) => r) -> r Source Github #

(CategoryOf j, CategoryOf k) => DecidableProfunctor (TerminalProfunctor :: k -> j -> Type) Source Github # 
Instance details

Defined in Proarrow.Profunctor.Instance.Terminal

Methods

decide :: forall (a :: k) (b :: j). (Ob a, Ob b) => Decision (TerminalProfunctor :: k -> j -> Type) a b (Holds (TerminalProfunctor :: k -> j -> Type) a b) Source Github #

toHolds :: forall (a :: k) (b :: j) r. TerminalProfunctor a b -> ((Holds (TerminalProfunctor :: k -> j -> Type) a b ~ 'TRU, Ob a, Ob b) => r) -> r Source Github #

(Thin j, Thin k, DecidableProfunctor p) => DecidableProfunctor (UnOp p :: k -> j -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Opposite

Methods

decide :: forall (a :: k) (b :: j). (Ob a, Ob b) => Decision (UnOp p) a b (Holds (UnOp p) a b) Source Github #

toHolds :: forall (a :: k) (b :: j) r. UnOp p a b -> ((Holds (UnOp p) a b ~ 'TRU, Ob a, Ob b) => r) -> r Source Github #

(Relation p, DecidableProfunctor p) => DecidableProfunctor (Converse p :: k -> j -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Rel

Methods

decide :: forall (a :: k) (b :: j). (Ob a, Ob b) => Decision (Converse p) a b (Holds (Converse p) a b) Source Github #

toHolds :: forall (a :: k) (b :: j) r. Converse p a b -> ((Holds (Converse p) a b ~ 'TRU, Ob a, Ob b) => r) -> r Source Github #

(FunctorForRep f, DecidableProfunctor (Hom j)) => DecidableProfunctor (Corep f :: k -> j -> Type) Source Github # 
Instance details

Defined in Proarrow.Profunctor.Corepresentable

Methods

decide :: forall (a :: k) (b :: j). (Ob a, Ob b) => Decision (Corep f) a b (Holds (Corep f) a b) Source Github #

toHolds :: forall (a :: k) (b :: j) r. Corep f a b -> ((Holds (Corep f) a b ~ 'TRU, Ob a, Ob b) => r) -> r Source Github #

(Functor f, DecidableProfunctor (Hom j)) => DecidableProfunctor (Costar f :: k -> j -> Type) Source Github # 
Instance details

Defined in Proarrow.Profunctor.Instance.Costar

Methods

decide :: forall (a :: k) (b :: j). (Ob a, Ob b) => Decision (Costar f) a b (Holds (Costar f) a b) Source Github #

toHolds :: forall (a :: k) (b :: j) r. Costar f a b -> ((Holds (Costar f) a b ~ 'TRU, Ob a, Ob b) => r) -> r Source Github #

(Functor f, DecidableProfunctor (Hom k)) => DecidableProfunctor (Star f :: k -> j -> Type) Source Github # 
Instance details

Defined in Proarrow.Profunctor.Instance.Star

Methods

decide :: forall (a :: k) (b :: j). (Ob a, Ob b) => Decision (Star f) a b (Holds (Star f) a b) Source Github #

toHolds :: forall (a :: k) (b :: j) r. Star f a b -> ((Holds (Star f) a b ~ 'TRU, Ob a, Ob b) => r) -> r Source Github #

(Corepresentable p, DecidableProfunctor (Hom k)) => DecidableProfunctor (CorepStar p :: k -> j -> Type) Source Github # 
Instance details

Defined in Proarrow.Profunctor.Representable

Methods

decide :: forall (a :: k) (b :: j). (Ob a, Ob b) => Decision (CorepStar p) a b (Holds (CorepStar p) a b) Source Github #

toHolds :: forall (a :: k) (b :: j) r. CorepStar p a b -> ((Holds (CorepStar p) a b ~ 'TRU, Ob a, Ob b) => r) -> r Source Github #

(FunctorForRep f, DecidableProfunctor (Hom k)) => DecidableProfunctor (Rep f :: k -> j -> Type) Source Github # 
Instance details

Defined in Proarrow.Profunctor.Representable

Methods

decide :: forall (a :: k) (b :: j). (Ob a, Ob b) => Decision (Rep f) a b (Holds (Rep f) a b) Source Github #

toHolds :: forall (a :: k) (b :: j) r. Rep f a b -> ((Holds (Rep f) a b ~ 'TRU, Ob a, Ob b) => r) -> r Source Github #

(Representable p, DecidableProfunctor (Hom j)) => DecidableProfunctor (RepCostar p :: k -> j -> Type) Source Github # 
Instance details

Defined in Proarrow.Profunctor.Representable

Methods

decide :: forall (a :: k) (b :: j). (Ob a, Ob b) => Decision (RepCostar p) a b (Holds (RepCostar p) a b) Source Github #

toHolds :: forall (a :: k) (b :: j) r. RepCostar p a b -> ((Holds (RepCostar p) a b ~ 'TRU, Ob a, Ob b) => r) -> r Source Github #

(SNatI n, DecidableProfunctor p, Decidable k, Enumerable k) => DecidableProfunctor (Walk n p :: k -> k -> Type) Source Github #

Reachability: the truth of a walk is its hom-object in BOOL, and shortest at grade TRU is the path.

Instance details

Defined in Proarrow.Category.Enriched.Thin.Composition

Methods

decide :: forall (a :: k) (b :: k). (Ob a, Ob b) => Decision (Walk n p) a b (Holds (Walk n p) a b) Source Github #

toHolds :: forall (a :: k) (b :: k) r. Walk n p a b -> ((Holds (Walk n p) a b ~ 'TRU, Ob a, Ob b) => r) -> r Source Github #

(DecidableProfunctor p, DecidableProfunctor q, Discrete j, Discrete k) => DecidableProfunctor (p :~>: q :: k -> j -> Type) Source Github #

Implication, decided: the exponential holds unless p holds and q does not. Against p an arrow of p is refuted by noArrow.

Instance details

Defined in Proarrow.Profunctor.Instance.Exponential

Methods

decide :: forall (a :: k) (b :: j). (Ob a, Ob b) => Decision (p :~>: q) a b (Holds (p :~>: q) a b) Source Github #

toHolds :: forall (a :: k) (b :: j) r. (p :~>: q) a b -> ((Holds (p :~>: q) a b ~ 'TRU, Ob a, Ob b) => r) -> r Source Github #

(DecidableProfunctor p, DecidableProfunctor q) => DecidableProfunctor (p :*: q :: k -> j -> Type) Source Github # 
Instance details

Defined in Proarrow.Limit.BinaryProduct

Methods

decide :: forall (a :: k) (b :: j). (Ob a, Ob b) => Decision (p :*: q) a b (Holds (p :*: q) a b) Source Github #

toHolds :: forall (a :: k) (b :: j) r. (p :*: q) a b -> ((Holds (p :*: q) a b ~ 'TRU, Ob a, Ob b) => r) -> r Source Github #

(DecidableProfunctor (Hom k), FunctorForRep f, FunctorForRep g) => DecidableProfunctor (Direp f g :: j -> i -> Type) Source Github # 
Instance details

Defined in Proarrow.Profunctor.Instance.Direp

Methods

decide :: forall (a :: j) (b :: i). (Ob a, Ob b) => Decision (Direp f g) a b (Holds (Direp f g) a b) Source Github #

toHolds :: forall (a :: j) (b :: i) r. Direp f g a b -> ((Holds (Direp f g) a b ~ 'TRU, Ob a, Ob b) => r) -> r Source Github #

DecideComp (ThinCompStrategy p q) p q => DecidableProfunctor (p :.: q :: k -> j2 -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Enriched.Thin.Composition

Methods

decide :: forall (a :: k) (b :: j2). (Ob a, Ob b) => Decision (p :.: q) a b (Holds (p :.: q) a b) Source Github #

toHolds :: forall (a :: k) (b :: j2) r. (p :.: q) a b -> ((Holds (p :.: q) a b ~ 'TRU, Ob a, Ob b) => r) -> r Source Github #

Indexed k => DecidableProfunctor (Codiscrete :: CODISCRETE k -> CODISCRETE k -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Discrete

Methods

decide :: forall (a :: CODISCRETE k) (b :: CODISCRETE k). (Ob a, Ob b) => Decision (Codiscrete :: CODISCRETE k -> CODISCRETE k -> Type) a b (Holds (Codiscrete :: CODISCRETE k -> CODISCRETE k -> Type) a b) Source Github #

toHolds :: forall (a :: CODISCRETE k) (b :: CODISCRETE k) r. Codiscrete a b -> ((Holds (Codiscrete :: CODISCRETE k -> CODISCRETE k -> Type) a b ~ 'TRU, Ob a, Ob b) => r) -> r Source Github #

Indexed k => DecidableProfunctor (Discrete :: DISCRETE k -> DISCRETE k -> Type) Source Github #

Two points are equal exactly when their indices are.

Instance details

Defined in Proarrow.Category.Instance.Discrete

Methods

decide :: forall (a :: DISCRETE k) (b :: DISCRETE k). (Ob a, Ob b) => Decision (Discrete :: DISCRETE k -> DISCRETE k -> Type) a b (Holds (Discrete :: DISCRETE k -> DISCRETE k -> Type) a b) Source Github #

toHolds :: forall (a :: DISCRETE k) (b :: DISCRETE k) r. Discrete a b -> ((Holds (Discrete :: DISCRETE k -> DISCRETE k -> Type) a b ~ 'TRU, Ob a, Ob b) => r) -> r Source Github #

DecidableProfunctor (LTE :: ORDINAL n -> ORDINAL n -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Ordinal

Methods

decide :: forall (a :: ORDINAL n) (b :: ORDINAL n). (Ob a, Ob b) => Decision (LTE :: ORDINAL n -> ORDINAL n -> Type) a b (Holds (LTE :: ORDINAL n -> ORDINAL n -> Type) a b) Source Github #

toHolds :: forall (a :: ORDINAL n) (b :: ORDINAL n) r. LTE a b -> ((Holds (LTE :: ORDINAL n -> ORDINAL n -> Type) a b ~ 'TRU, Ob a, Ob b) => r) -> r Source Github #

(Indexed k, KnownEdges es) => DecidableProfunctor (Edges es :: DISCRETE k -> DISCRETE k -> Type) Source Github # 
Instance details

Defined in Proarrow.Profunctor.Instance.Edges

Methods

decide :: forall (a :: DISCRETE k) (b :: DISCRETE k). (Ob a, Ob b) => Decision (Edges es) a b (Holds (Edges es) a b) Source Github #

toHolds :: forall (a :: DISCRETE k) (b :: DISCRETE k) r. Edges es a b -> ((Holds (Edges es) a b ~ 'TRU, Ob a, Ob b) => r) -> r Source Github #

DecidableProfunctor p => DecidableProfunctor (Op p :: OPPOSITE j -> OPPOSITE k -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Opposite

Methods

decide :: forall (a :: OPPOSITE j) (b :: OPPOSITE k). (Ob a, Ob b) => Decision (Op p) a b (Holds (Op p) a b) Source Github #

toHolds :: forall (a :: OPPOSITE j) (b :: OPPOSITE k) r. Op p a b -> ((Holds (Op p) a b ~ 'TRU, Ob a, Ob b) => r) -> r Source Github #

(DecidableProfunctor p, Promonad p) => DecidableProfunctor (Kleisli :: KLEISLI p -> KLEISLI p -> Type) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Kleisli

Methods

decide :: forall (a :: KLEISLI p) (b :: KLEISLI p). (Ob a, Ob b) => Decision (Kleisli :: KLEISLI p -> KLEISLI p -> Type) a b (Holds (Kleisli :: KLEISLI p -> KLEISLI p -> Type) a b) Source Github #

toHolds :: forall (a :: KLEISLI p) (b :: KLEISLI p) r. Kleisli a b -> ((Holds (Kleisli :: KLEISLI p -> KLEISLI p -> Type) a b ~ 'TRU, Ob a, Ob b) => r) -> r Source Github #

(DecidableProfunctor p, DecidableProfunctor q) => DecidableProfunctor (p :**: q :: (k1, k2) -> (j1, j2) -> Type) Source Github #

A product holds when both components do: the type-level && is BOOL's categorical product.

Instance details

Defined in Proarrow.Limit.BinaryProduct

Methods

decide :: forall (a :: (k1, k2)) (b :: (j1, j2)). (Ob a, Ob b) => Decision (p :**: q) a b (Holds (p :**: q) a b) Source Github #

toHolds :: forall (a :: (k1, k2)) (b :: (j1, j2)) r. (p :**: q) a b -> ((Holds (p :**: q) a b ~ 'TRU, Ob a, Ob b) => r) -> r Source Github #

(Decidable j, Decidable k, DecidableProfunctor p) => DecidableProfunctor (Collage :: COLLAGE p -> COLLAGE p -> Type) Source Github #

Decided piecewise: within either side by that side's order, across by p, and never backwards.

Instance details

Defined in Proarrow.Category.Instance.Collage

Methods

decide :: forall (a :: COLLAGE p) (b :: COLLAGE p). (Ob a, Ob b) => Decision (Collage :: COLLAGE p -> COLLAGE p -> Type) a b (Holds (Collage :: COLLAGE p -> COLLAGE p -> Type) a b) Source Github #

toHolds :: forall (a :: COLLAGE p) (b :: COLLAGE p) r. Collage a b -> ((Holds (Collage :: COLLAGE p -> COLLAGE p -> Type) a b ~ 'TRU, Ob a, Ob b) => r) -> r Source Github #

fromHolds :: forall {j} {k} p (a :: k) (b :: j). (DecidableProfunctor p, Ob a, Ob b, Holds p a b ~ 'TRU) => p a b Source Github #

noArrow :: forall {j} {k} p (a :: k) (b :: j) r. (DecidableProfunctor p, Holds p a b ~ 'FLS) => p a b -> r Source Github #

A profunctor that decides against an arrow has none, so a caller holding one may return anything.

class (DecidableProfunctor (Hom k), CategoryOf k) => Decidable k Source Github #

A thin category whose order is decidable at the type level.

Instances

Instances details
(DecidableProfunctor (Hom k), CategoryOf k) => Decidable k Source Github # 
Instance details

Defined in Proarrow.Category.Enriched.Thin

class (ThinProfunctor (Hom k), CategoryOf k) => Thin k Source Github #

Instances

Instances details
(ThinProfunctor (Hom k), CategoryOf k) => Thin k Source Github # 
Instance details

Defined in Proarrow.Category.Enriched.Thin

class (ThinProfunctor p, Ob a, Ob b, HasArrow p a b) => HasArrow' (p :: j +-> k) (a :: k) (b :: j) where Source Github #

Methods

arr' :: p a b Source Github #

Instances

Instances details
(ThinProfunctor p, Ob a, Ob b, HasArrow p a b) => HasArrow' (p :: j +-> k) (a :: k) (b :: j) Source Github # 
Instance details

Defined in Proarrow.Category.Enriched.Thin

Methods

arr' :: p a b Source Github #

class (ThinProfunctor p, forall (c :: k) (d :: j). (Ob c, Ob d) => HasArrow' p c d, Codiscrete j, Codiscrete k) => CodiscreteProfunctor (p :: j +-> k) where Source Github #

Methods

anyArr :: forall (a :: k) (b :: j). (Ob a, Ob b) => p a b Source Github #

Instances

Instances details
(ThinProfunctor p, forall (c :: k) (d :: j). (Ob c, Ob d) => HasArrow' p c d, Codiscrete j, Codiscrete k) => CodiscreteProfunctor (p :: j +-> k) Source Github # 
Instance details

Defined in Proarrow.Category.Enriched.Thin

Methods

anyArr :: forall (a :: k) (b :: j). (Ob a, Ob b) => p a b Source Github #

type Codiscrete k = CodiscreteProfunctor (Hom k) Source Github #

class (c => d, d => c) => c <=> d Source Github #

Instances

Instances details
(c => d, d => c) => c <=> d Source Github # 
Instance details

Defined in Proarrow.Category.Enriched.Thin

class (HasArrow p a b => Bottom) => HasNoArrow (p :: j +-> k) (a :: k) (b :: j) where Source Github #

Methods

arrowIsBottomProof :: HasArrow p a b => r Source Github #

Instances

Instances details
(HasArrow p a b => Bottom) => HasNoArrow (p :: j +-> k) (a :: k) (b :: j) Source Github # 
Instance details

Defined in Proarrow.Category.Enriched.Thin

Methods

arrowIsBottomProof :: HasArrow p a b => r Source Github #

class (ThinProfunctor p, forall (a :: k) (b :: j). (Ob a, Ob b) => HasNoArrow p a b) => DiscreteProfunctor (p :: j +-> k) where Source Github #

Methods

exfalso :: forall (a :: k) (b :: j) r. p a b -> r Source Github #

Instances

Instances details
(ThinProfunctor p, forall (a :: k) (b :: j). (Ob a, Ob b) => HasNoArrow p a b) => DiscreteProfunctor (p :: j +-> k) Source Github # 
Instance details

Defined in Proarrow.Category.Enriched.Thin

Methods

exfalso :: forall (a :: k) (b :: j) r. p a b -> r Source Github #

class HasArrow (Hom k) c d <=> (c ~ d) => ArrowIsId k (c :: k) (d :: k) where Source Github #

Methods

arrowIsIdProof :: HasArrow (Hom k) c d => (c ~ d => r) -> r Source Github #

Instances

Instances details
HasArrow (Hom k) c d <=> (c ~ d) => ArrowIsId k (c :: k) (d :: k) Source Github # 
Instance details

Defined in Proarrow.Category.Enriched.Thin

Methods

arrowIsIdProof :: HasArrow (Hom k) c d => (c ~ d => r) -> r Source Github #

class (Thin k, forall (c :: k) (d :: k). (Ob c, Ob d) => ArrowIsId k c d) => Discrete k where Source Github #

Discrete k is not the same as DiscreteProfunctor (Hom k)!

Methods

withEq :: forall (a :: k) (b :: k) r. (a ~> b) -> (a ~ b => r) -> r Source Github #

Instances

Instances details
(Thin k, forall (c :: k) (d :: k). (Ob c, Ob d) => ArrowIsId k c d) => Discrete k Source Github # 
Instance details

Defined in Proarrow.Category.Enriched.Thin

Methods

withEq :: forall (a :: k) (b :: k) r. (a ~> b) -> (a ~ b => r) -> r Source Github #

Indexed, finite and enumerable kinds

class Indexed k Source Github #

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.

Associated Types

type Index (a :: k) :: Nat Source Github #

type Index (a :: k) = IndexOf a (Objects k)

type At k (i :: Nat) :: Maybe k Source Github #

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 At k (i :: Nat) = Lookup (Objects k) i

Instances

Instances details
Indexed Nat Source Github # 
Instance details

Defined in Proarrow.Category.Enriched.Thin

Associated Types

type Index (n :: Nat) 
Instance details

Defined in Proarrow.Category.Enriched.Thin

type Index (n :: Nat) = n
type At Nat i 
Instance details

Defined in Proarrow.Category.Enriched.Thin

type At Nat i = 'Just i
Indexed BOOL Source Github # 
Instance details

Defined in Proarrow.Category.Enriched.Thin

Associated Types

type Index (a :: BOOL) 
Instance details

Defined in Proarrow.Category.Enriched.Thin

type Index (a :: BOOL) = IndexOf a (Objects BOOL)
type At BOOL i 
Instance details

Defined in Proarrow.Category.Enriched.Thin

type At BOOL i = Lookup (Objects BOOL) i
Indexed VOID Source Github #

The empty kind has no inhabitants to number.

Instance details

Defined in Proarrow.Category.Enriched.Thin

Associated Types

type Index (a :: VOID) 
Instance details

Defined in Proarrow.Category.Enriched.Thin

type Index (a :: VOID) = 'Z
type At VOID i 
Instance details

Defined in Proarrow.Category.Enriched.Thin

type At VOID i = 'Nothing :: Maybe VOID
Indexed () Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Unit

Associated Types

type Index (a :: ()) 
Instance details

Defined in Proarrow.Category.Instance.Unit

type Index (a :: ()) = IndexOf a (Objects ())
type At () i 
Instance details

Defined in Proarrow.Category.Instance.Unit

type At () i = Lookup (Objects ()) i
Indexed k => Indexed (CODISCRETE k) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Discrete

Indexed k => Indexed (DISCRETE k) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Discrete

Indexed k => Indexed (OPPOSITE k) Source Github #

The opposite category has the same objects, numbered the same way.

Instance details

Defined in Proarrow.Category.Instance.Opposite

Indexed (ORDINAL n) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Ordinal

Indexed k => Indexed (KLEISLI p) Source Github #

The Kleisli category has the objects of k, numbered the same way, so a Kleisli category of a decidable promonad on an enumerable category is itself enumerable, and so can be searched, or closed (Proarrow.Category.Enriched.Thin.Composition).

Instance details

Defined in Proarrow.Category.Instance.Kleisli

Indexed (MONOID m) Source Github #

A monoid is a one-object category, so its kind has one inhabitant, at index zero. This is stated directly instead of left to the Objects default, so that it reduces for a not-yet-known inhabitant. That way withOb learns there is only M.

Instance details

Defined in Proarrow.Category.Instance.Monoid

Indexed k => Indexed (PATHS p) Source Github #

Objects are vertices, so a free category has as many of them as its quiver has, however many arrows the paths add (usually unboundedly many). So a free category is Finite without being anywhere near thin or decidable. This buys enumeration of the objects alone. That is enough for Proarrow.Testing.genSomeFinite to derive a schema's object palette, and not enough for anything that wants to enumerate arrows.

Instance details

Defined in Proarrow.Category.Instance.Paths

InternalIn ik FINSET => Indexed (INTERNAL ik) Source Github # 
Instance details

Defined in Proarrow.Category.Internal

Indexed (BOOL, BOOL) Source Github #

The product of two enumerable kinds is enumerable, but numbering one in general needs type-level division to invert the pairing, which fin does not provide, so this instance for (BOOL, BOOL) is numbered by hand. The order matches the value-level pairIndex convention: first component slowest.

(Proarrow.Category.Sheaf uses this kind as the opens of a discrete two-point space: a pair of booleans is a subset of {x, y}.)

Instance details

Defined in Proarrow.Category.Instance.Product

Associated Types

type Index (a :: (BOOL, BOOL)) 
Instance details

Defined in Proarrow.Category.Instance.Product

type Index (a :: (BOOL, BOOL)) = IndexOf a (Objects (BOOL, BOOL))
type At (BOOL, BOOL) i 
Instance details

Defined in Proarrow.Category.Instance.Product

type At (BOOL, BOOL) i = Lookup (Objects (BOOL, BOOL)) i
(Finite j, Finite k) => Indexed (COLLAGE p) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Collage

class (SNatI (Index a), At k (Index a) ~ 'Just a) => KnownIndex (a :: k) Source Github #

The evidence that a is numbered: its index, reflected, and At reading it back.

Instances

Instances details
(SNatI (Index a), At k (Index a) ~ 'Just a) => KnownIndex (a :: k) Source Github # 
Instance details

Defined in Proarrow.Category.Enriched.Thin

type family NatEq (n :: Nat) (m :: Nat) :: BOOL where ... Source Github #

Equality of naturals, with evidence either way.

Equations

NatEq 'Z 'Z = 'TRU 
NatEq ('S n) ('S m) = NatEq n m 
NatEq n m = 'FLS 

natEq :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> Decision ((:~:) :: Nat -> Nat -> Type) n m (NatEq n m) Source Github #

withNatEqRefl :: forall (n :: Nat) r. SNat n -> (NatEq n n ~ 'TRU => r) -> r Source Github #

type Equal (a :: k) (b :: k) = NatEq (Index a) (Index b) Source Github #

Two numbered inhabitants are equal exactly when their indices are.

decideEq :: forall {k} (a :: k) (b :: k). (KnownIndex a, KnownIndex b) => Decision ((:~:) :: k -> k -> Type) a b (Equal a b) Source Github #

type family Length (xs :: [k]) :: Nat where ... Source Github #

Equations

Length ('[] :: [k]) = 'Z 
Length (x ': xs :: [k]) = 'S (Length xs) 

type family Lookup (xs :: [k]) (i :: Nat) :: Maybe k where ... Source Github #

Equations

Lookup ('[] :: [k]) i = 'Nothing :: Maybe k 
Lookup (x ': xs :: [a]) 'Z = 'Just x 
Lookup (x ': xs :: [k]) ('S i) = Lookup xs i 

type family Entry (xs :: [k]) (i :: Nat) :: k where ... Source Github #

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.

Equations

Entry (x ': xs :: [k]) 'Z = x 
Entry (x ': xs :: [k]) ('S i) = Entry xs i 

class KnownList (c :: x -> Constraint) (shape :: [y]) (xs :: [x]) where Source Github #

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.

Methods

withEntry :: forall (s :: y) (i :: Nat) r. SNat i -> (Lookup shape i :~: 'Just s) -> (c (Entry xs i) => r) -> r Source Github #

Instances

Instances details
KnownList (c :: x -> Constraint) ('[] :: [y]) ('[] :: [x]) Source Github # 
Instance details

Defined in Proarrow.Category.Enriched.Thin

Methods

withEntry :: forall (s :: y) (i :: Nat) r. SNat i -> (Lookup ('[] :: [y]) i :~: 'Just s) -> (c (Entry ('[] :: [x]) i) => r) -> r Source Github #

(c x, KnownList c shape xs) => KnownList (c :: a -> Constraint) (s ': shape :: [y]) (x ': xs :: [a]) Source Github # 
Instance details

Defined in Proarrow.Category.Enriched.Thin

Methods

withEntry :: forall (s0 :: y) (i :: Nat) r. SNat i -> (Lookup (s ': shape) i :~: 'Just s0) -> (c (Entry (x ': xs) i) => r) -> r Source Github #

type family IndexOf (a :: k) (xs :: [k]) :: Nat where ... Source Github #

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.

Equations

IndexOf (a2 :: a1) (a2 ': xs :: [a1]) = 'Z 
IndexOf (a :: k) (b ': xs :: [k]) = 'S (IndexOf a xs) 

data IndexedList (as :: [k]) where Source Github #

A type-level list of inhabitants, reflected to the value level with their indices.

Constructors

FNil :: forall {k}. IndexedList ('[] :: [k]) 
FCons :: forall {k} (a :: k) (as1 :: [k]). KnownIndex a => IndexedList as1 -> IndexedList (a ': as1) 

class HasFiniteDefault (xs :: [k]) where Source Github #

Every element of the list is numbered, so the list can be reflected to an IndexedList. So a kind that simply writes its objects out gets finite for free.

Methods

finiteDefault :: IndexedList xs Source Github #

Instances

Instances details
HasFiniteDefault ('[] :: [k]) Source Github # 
Instance details

Defined in Proarrow.Category.Enriched.Thin

Methods

finiteDefault :: IndexedList ('[] :: [k]) Source Github #

(KnownIndex a, HasFiniteDefault as) => HasFiniteDefault (a ': as :: [k]) Source Github # 
Instance details

Defined in Proarrow.Category.Enriched.Thin

Methods

finiteDefault :: IndexedList (a ': as) Source Github #

class Indexed k => Finite k where Source Github #

An Indexed kind with finitely many inhabitants, listed in Objects in the order of their indices: withAtLookup says that the list tabulates At.

Minimal complete definition

Nothing

Associated Types

type Objects k :: [k] Source Github #

Methods

finite :: IndexedList (Objects k) Source Github #

default finite :: HasFiniteDefault (Objects k) => IndexedList (Objects k) Source Github #

withAtLookup :: forall (i :: Nat) r. SNat i -> (Lookup (Objects k) i ~ At k i => r) -> r Source Github #

default withAtLookup :: forall (i :: Nat) r. At k i ~ Lookup (Objects k) i => SNat i -> (Lookup (Objects k) i ~ At k i => r) -> r Source Github #

Instances

Instances details
Finite BOOL Source Github # 
Instance details

Defined in Proarrow.Category.Enriched.Thin

Associated Types

type Objects BOOL 
Instance details

Defined in Proarrow.Category.Enriched.Thin

type Objects BOOL = '['FLS, 'TRU]

Methods

finite :: IndexedList (Objects BOOL) Source Github #

withAtLookup :: forall (i :: Nat) r. SNat i -> (Lookup (Objects BOOL) i ~ At BOOL i => r) -> r Source Github #

Finite VOID Source Github # 
Instance details

Defined in Proarrow.Category.Enriched.Thin

Associated Types

type Objects VOID 
Instance details

Defined in Proarrow.Category.Enriched.Thin

type Objects VOID = '[] :: [VOID]

Methods

finite :: IndexedList (Objects VOID) Source Github #

withAtLookup :: forall (i :: Nat) r. SNat i -> (Lookup (Objects VOID) i ~ At VOID i => r) -> r Source Github #

Finite () Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Unit

Associated Types

type Objects () 
Instance details

Defined in Proarrow.Category.Instance.Unit

type Objects () = '['()]

Methods

finite :: IndexedList (Objects ()) Source Github #

withAtLookup :: forall (i :: Nat) r. SNat i -> (Lookup (Objects ()) i ~ At () i => r) -> r Source Github #

Finite k => Finite (CODISCRETE k) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Discrete

Associated Types

type Objects (CODISCRETE k) 
Instance details

Defined in Proarrow.Category.Instance.Discrete

type Objects (CODISCRETE k) = MapWrap ('CD :: k -> CODISCRETE k) (Objects k)

Methods

finite :: IndexedList (Objects (CODISCRETE k)) Source Github #

withAtLookup :: forall (i :: Nat) r. SNat i -> (Lookup (Objects (CODISCRETE k)) i ~ At (CODISCRETE k) i => r) -> r Source Github #

Finite k => Finite (DISCRETE k) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Discrete

Associated Types

type Objects (DISCRETE k) 
Instance details

Defined in Proarrow.Category.Instance.Discrete

type Objects (DISCRETE k) = MapWrap ('D :: k -> DISCRETE k) (Objects k)

Methods

finite :: IndexedList (Objects (DISCRETE k)) Source Github #

withAtLookup :: forall (i :: Nat) r. SNat i -> (Lookup (Objects (DISCRETE k)) i ~ At (DISCRETE k) i => r) -> r Source Github #

Finite k => Finite (OPPOSITE k) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Opposite

Associated Types

type Objects (OPPOSITE k) 
Instance details

Defined in Proarrow.Category.Instance.Opposite

type Objects (OPPOSITE k) = MapWrap ('OP :: k -> OPPOSITE k) (Objects k)

Methods

finite :: IndexedList (Objects (OPPOSITE k)) Source Github #

withAtLookup :: forall (i :: Nat) r. SNat i -> (Lookup (Objects (OPPOSITE k)) i ~ At (OPPOSITE k) i => r) -> r Source Github #

SNatI n => Finite (ORDINAL n) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Ordinal

Associated Types

type Objects (ORDINAL n) 
Instance details

Defined in Proarrow.Category.Instance.Ordinal

type Objects (ORDINAL n) = OrdObjects n

Methods

finite :: IndexedList (Objects (ORDINAL n)) Source Github #

withAtLookup :: forall (i :: Nat) r. SNat i -> (Lookup (Objects (ORDINAL n)) i ~ At (ORDINAL n) i => r) -> r Source Github #

Finite k => Finite (KLEISLI p) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Kleisli

Associated Types

type Objects (KLEISLI p) 
Instance details

Defined in Proarrow.Category.Instance.Kleisli

type Objects (KLEISLI p) = MapWrap ('KL :: k -> KLEISLI p) (Objects k)

Methods

finite :: IndexedList (Objects (KLEISLI p)) Source Github #

withAtLookup :: forall (i :: Nat) r. SNat i -> (Lookup (Objects (KLEISLI p)) i ~ At (KLEISLI p) i => r) -> r Source Github #

Finite (MONOID m) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Monoid

Associated Types

type Objects (MONOID m) 
Instance details

Defined in Proarrow.Category.Instance.Monoid

type Objects (MONOID m) = '['M :: MONOID m]

Methods

finite :: IndexedList (Objects (MONOID m)) Source Github #

withAtLookup :: forall (i :: Nat) r. SNat i -> (Lookup (Objects (MONOID m)) i ~ At (MONOID m) i => r) -> r Source Github #

Finite k => Finite (PATHS p) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Paths

Associated Types

type Objects (PATHS p) 
Instance details

Defined in Proarrow.Category.Instance.Paths

type Objects (PATHS p) = MapWrap ('PTH :: k -> PATHS p) (Objects k)

Methods

finite :: IndexedList (Objects (PATHS p)) Source Github #

withAtLookup :: forall (i :: Nat) r. SNat i -> (Lookup (Objects (PATHS p)) i ~ At (PATHS p) i => r) -> r Source Github #

(InternalIn ik FINSET, SNatI (NumObs ik)) => Finite (INTERNAL ik) Source Github # 
Instance details

Defined in Proarrow.Category.Internal

Associated Types

type Objects (INTERNAL ik) 
Instance details

Defined in Proarrow.Category.Internal

type Objects (INTERNAL ik) = MapWrap ('IN :: ORDINAL (NumObs ik) -> INTERNAL ik) (Objects (ORDINAL (NumObs ik)))

Methods

finite :: IndexedList (Objects (INTERNAL ik)) Source Github #

withAtLookup :: forall (i :: Nat) r. SNat i -> (Lookup (Objects (INTERNAL ik)) i ~ At (INTERNAL ik) i => r) -> r Source Github #

Finite (BOOL, BOOL) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Product

Associated Types

type Objects (BOOL, BOOL) 
Instance details

Defined in Proarrow.Category.Instance.Product

type Objects (BOOL, BOOL) = '['('FLS, 'FLS), '('FLS, 'TRU), '('TRU, 'FLS), '('TRU, 'TRU)]

Methods

finite :: IndexedList (Objects (BOOL, BOOL)) Source Github #

withAtLookup :: forall (i :: Nat) r. SNat i -> (Lookup (Objects (BOOL, BOOL)) i ~ At (BOOL, BOOL) i => r) -> r Source Github #

(Finite j, Finite k) => Finite (COLLAGE p) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Collage

Associated Types

type Objects (COLLAGE p) 
Instance details

Defined in Proarrow.Category.Instance.Collage

type Objects (COLLAGE p) = CollageObjects p (Objects j)

Methods

finite :: IndexedList (Objects (COLLAGE p)) Source Github #

withAtLookup :: forall (i :: Nat) r. SNat i -> (Lookup (Objects (COLLAGE p)) i ~ At (COLLAGE p) i => r) -> r Source Github #

data Member (a :: k) (as :: [k]) where Source Github #

A proof that a occurs in the type-level list as.

Constructors

Here :: forall {k} (a :: k) (as1 :: [k]). Member a (a ': as1) 
There :: forall {k} (a :: k) (as1 :: [k]) (b :: k). Member a as1 -> Member a (b ': as1) 

memberIndex :: forall {k} (a :: k). (Finite k, KnownIndex a) => Member a (Objects k) Source Github #

Every numbered inhabitant of a finite kind occurs in its list: walk to its index.

class (CategoryOf k, Finite k) => Enumerable k where Source Github #

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.

Minimal complete definition

withIndex, (atOb | withOb)

Methods

withIndex :: forall (a :: k) r. Ob a => (KnownIndex a => r) -> r Source Github #

withOb :: forall (a :: k) r. KnownIndex a => (Ob a => r) -> r Source Github #

atOb :: forall (i :: Nat). SNat i -> AtOb k (At k i) Source Github #

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. The discrete kinds cannot, since they ask only that the kind they wrap be Finite.

Instances

Instances details
Enumerable BOOL Source Github # 
Instance details

Defined in Proarrow.Category.Enriched.Thin

Methods

withIndex :: forall (a :: BOOL) r. Ob a => (KnownIndex a => r) -> r Source Github #

withOb :: forall (a :: BOOL) r. KnownIndex a => (Ob a => r) -> r Source Github #

atOb :: forall (i :: Nat). SNat i -> AtOb BOOL (At BOOL i) Source Github #

Enumerable VOID Source Github # 
Instance details

Defined in Proarrow.Category.Enriched.Thin

Methods

withIndex :: forall (a :: VOID) r. Ob a => (KnownIndex a => r) -> r Source Github #

withOb :: forall (a :: VOID) r. KnownIndex a => (Ob a => r) -> r Source Github #

atOb :: forall (i :: Nat). SNat i -> AtOb VOID (At VOID i) Source Github #

Enumerable () Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Unit

Methods

withIndex :: forall (a :: ()) r. Ob a => (KnownIndex a => r) -> r Source Github #

withOb :: forall (a :: ()) r. KnownIndex a => (Ob a => r) -> r Source Github #

atOb :: forall (i :: Nat). SNat i -> AtOb () (At () i) Source Github #

Finite k => Enumerable (CODISCRETE k) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Discrete

Methods

withIndex :: forall (a :: CODISCRETE k) r. Ob a => (KnownIndex a => r) -> r Source Github #

withOb :: forall (a :: CODISCRETE k) r. KnownIndex a => (Ob a => r) -> r Source Github #

atOb :: forall (i :: Nat). SNat i -> AtOb (CODISCRETE k) (At (CODISCRETE k) i) Source Github #

Finite k => Enumerable (DISCRETE k) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Discrete

Methods

withIndex :: forall (a :: DISCRETE k) r. Ob a => (KnownIndex a => r) -> r Source Github #

withOb :: forall (a :: DISCRETE k) r. KnownIndex a => (Ob a => r) -> r Source Github #

atOb :: forall (i :: Nat). SNat i -> AtOb (DISCRETE k) (At (DISCRETE k) i) Source Github #

Enumerable k => Enumerable (OPPOSITE k) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Opposite

Methods

withIndex :: forall (a :: OPPOSITE k) r. Ob a => (KnownIndex a => r) -> r Source Github #

withOb :: forall (a :: OPPOSITE k) r. KnownIndex a => (Ob a => r) -> r Source Github #

atOb :: forall (i :: Nat). SNat i -> AtOb (OPPOSITE k) (At (OPPOSITE k) i) Source Github #

SNatI n => Enumerable (ORDINAL n) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Ordinal

Methods

withIndex :: forall (a :: ORDINAL n) r. Ob a => (KnownIndex a => r) -> r Source Github #

withOb :: forall (a :: ORDINAL n) r. KnownIndex a => (Ob a => r) -> r Source Github #

atOb :: forall (i :: Nat). SNat i -> AtOb (ORDINAL n) (At (ORDINAL n) i) Source Github #

(Enumerable k, Promonad p) => Enumerable (KLEISLI p) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Kleisli

Methods

withIndex :: forall (a :: KLEISLI p) r. Ob a => (KnownIndex a => r) -> r Source Github #

withOb :: forall (a :: KLEISLI p) r. KnownIndex a => (Ob a => r) -> r Source Github #

atOb :: forall (i :: Nat). SNat i -> AtOb (KLEISLI p) (At (KLEISLI p) i) Source Github #

Monoid m => Enumerable (MONOID m) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Monoid

Methods

withIndex :: forall (a :: MONOID m) r. Ob a => (KnownIndex a => r) -> r Source Github #

withOb :: forall (a :: MONOID m) r. KnownIndex a => (Ob a => r) -> r Source Github #

atOb :: forall (i :: Nat). SNat i -> AtOb (MONOID m) (At (MONOID m) i) Source Github #

(Enumerable k, Rewrite p) => Enumerable (PATHS p) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Paths

Methods

withIndex :: forall (a :: PATHS p) r. Ob a => (KnownIndex a => r) -> r Source Github #

withOb :: forall (a :: PATHS p) r. KnownIndex a => (Ob a => r) -> r Source Github #

atOb :: forall (i :: Nat). SNat i -> AtOb (PATHS p) (At (PATHS p) i) Source Github #

(InternalIn ik FINSET, SNatI (NumObs ik)) => Enumerable (INTERNAL ik) Source Github # 
Instance details

Defined in Proarrow.Category.Internal

Methods

withIndex :: forall (a :: INTERNAL ik) r. Ob a => (KnownIndex a => r) -> r Source Github #

withOb :: forall (a :: INTERNAL ik) r. KnownIndex a => (Ob a => r) -> r Source Github #

atOb :: forall (i :: Nat). SNat i -> AtOb (INTERNAL ik) (At (INTERNAL ik) i) Source Github #

Enumerable (BOOL, BOOL) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Product

Methods

withIndex :: forall (a :: (BOOL, BOOL)) r. Ob a => (KnownIndex a => r) -> r Source Github #

withOb :: forall (a :: (BOOL, BOOL)) r. KnownIndex a => (Ob a => r) -> r Source Github #

atOb :: forall (i :: Nat). SNat i -> AtOb (BOOL, BOOL) (At (BOOL, BOOL) i) Source Github #

(Enumerable j, Enumerable k, Profunctor p) => Enumerable (COLLAGE p) Source Github # 
Instance details

Defined in Proarrow.Category.Instance.Collage

Methods

withIndex :: forall (a :: COLLAGE p) r. Ob a => (KnownIndex a => r) -> r Source Github #

withOb :: forall (a :: COLLAGE p) r. KnownIndex a => (Ob a => r) -> r Source Github #

atOb :: forall (i :: Nat). SNat i -> AtOb (COLLAGE p) (At (COLLAGE p) i) Source Github #

member :: forall {k} (a :: k). (Enumerable k, Ob a) => Member a (Objects k) Source Github #

Locate an object in the object list.

data AtOb k (x :: Maybe k) where Source Github #

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. A wrapper kind needs this to recover the objects of the kind it wraps.

Constructors

AtNothing :: forall k. AtOb k ('Nothing :: Maybe k) 
AtJust :: forall k (a :: k). (Ob a, KnownIndex a) => AtOb k ('Just a) 

noIndex :: forall {k} (a :: k) r. KnownIndex a => (At k (Index a) :~: ('Nothing :: Maybe k)) -> r Source Github #

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.

type family FmapWrap (w :: j -> k) (x :: Maybe j) :: Maybe k where ... Source Github #

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).

Equations

FmapWrap (w :: j -> k) ('Nothing :: Maybe j) = 'Nothing :: Maybe k 
FmapWrap (w :: j -> a1) ('Just a2 :: Maybe j) = 'Just (w a2) 

type family MapWrap (w :: j -> k) (xs :: [j]) :: [k] where ... Source Github #

Equations

MapWrap (w :: j -> k) ('[] :: [j]) = '[] :: [k] 
MapWrap (w :: j -> k) (x ': xs :: [j]) = w x ': 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) Source Github #

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 Source Github #

wrapFinite :: forall {j} {k} (w :: j -> k). (Finite j, forall (a :: j). KnownIndex a => KnownIndex (w a)) => IndexedList (MapWrap w (Objects j)) Source Github #

The two Finite methods of a wrapper kind, which are the same for every wrapper.

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 Source Github #

lookupOb :: forall k (j :: Nat) (xs :: [k]). Enumerable k => SNat j -> IndexedList xs -> AtOb k (Lookup xs j) Source Github #

The default atOb: walk the object list to the index.