Safe Haskell	Safe
Language	Haskell2010

Math.Tools.CoFunctor

Synopsis

type CoFunctor p = Contravariant p
inverse_image :: CoFunctor p => (a -> b) -> p b -> p a
(|>>) :: CoFunctor p => p b -> (a -> b) -> p a
class Representable p where
- type Representation p :: * -> *
- represent :: Representation p a -> p a
- (!>) :: p a -> (Representation p a -> p a) -> p a
class Propositional p where
- runProposition :: p a -> a -> p ()
class Propositional p => BinaryLogic p where
- toBool :: p () -> Bool
class CoFunctor p => Relational p where
- relation :: (a -> p b) -> p (a, b)
- unrelation :: p (a, b) -> a -> p b
class CoFunctor p => Existential p where
- direct_image :: (Universe a, Eq b) => (a -> b) -> p a -> p b
- universal_image :: (Universe a, Eq b) => (a -> b) -> p a -> p b
class CoFunctor p => Difference p minus | p -> minus where
- difference :: (p a -> p b) -> p (b `minus` a)
- undifference :: p (b `minus` a) -> p a -> p b
class (Eq c, CoFunctor p) => HasEqualizers p c where
- equalizer :: (a -> c) -> (a -> c) -> p a
- pullback :: (a -> c) -> (b -> c) -> p (a, b)
class Functor p => Topology p where
- arbitrary_union :: [p a] -> p a
- finite_intersect :: [p a] -> p a
class HasTerminalObject t where
- terminal_arrow :: a -> t
class CoFunctor p => HasVariables p t where
- variable :: String -> p t
class CoFunctor p => PropositionalLogic p where
- (-&-) :: p a -> p a -> p a
- (-|-) :: p a -> p a -> p a
- invert :: p a -> p a
class PropositionalLogic p => ModalLogic p where
- eventually :: p a -> p a
- always :: p a -> p a
class CoFunctor p => Continuous p where
- expand :: p (Either a b) -> (p a, p b)
class CoFunctor p => SubtractiveLogic p where
- (-\-) :: p a -> p a -> p a
class CoFunctor p => ImplicativeLogic p where
- (-=>-) :: p a -> p a -> p a
class CoFunctor p => BooleanLogic p where
- true :: p a
class CoFunctor p => UniversalLogic p where
- singleton :: Eq a => a -> p a
- all_members :: Universe a => p a
class CoFunctor p => Universal p where
- exist :: Universe b => p (a, b) -> p a
- univ :: Universe b => p (a, b) -> p a
member :: Propositional p => a -> p a -> p ()
isIn :: BinaryLogic p => a -> p a -> Bool
isNotIn :: BinaryLogic p => a -> p a -> Bool
terminal_part :: Propositional p => p () -> p ()
propositional_implication :: PropositionalLogic p => p a -> p a -> p a
relative_complement :: PropositionalLogic p => p a -> p a -> p a
intersect_list :: (BooleanLogic p, PropositionalLogic p) => [p a] -> p a
union_list :: (BooleanLogic p, PropositionalLogic p) => [p a] -> p a
characteristic :: BooleanLogic p => (a -> p ()) -> p a
false_prop :: (BooleanLogic p, PropositionalLogic p) => p a
(-<=>-) :: (ImplicativeLogic p, PropositionalLogic p) => p a -> p a -> p a
symmetric_difference :: (PropositionalLogic p, SubtractiveLogic p) => p a -> p a -> p a
boundary :: (PropositionalLogic p, BooleanLogic p, SubtractiveLogic p) => p a -> p a
curry_subst :: CoFunctor p => ((a, b) -> c) -> p (b -> c) -> p a
uncurry_subst :: CoFunctor p => (a -> b -> c) -> p c -> p (a, b)
dualize :: Difference p minus => (a -> b) -> p (a `minus` b)
coin1 :: CoFunctor p => p a -> p (a, b)
coin2 :: CoFunctor p => p b -> p (a, b)
cofst :: CoFunctor p => p (Either a b) -> p a
cosnd :: CoFunctor p => p (Either a b) -> p b
cocase :: CoFunctor p => (Either a b -> c) -> p c -> (p a, p b)
copair :: (Propositional p, BooleanLogic p) => p a -> p b -> p (Either a b)
pair_subst :: CoFunctor p => (a -> b) -> (a -> c) -> p (b, c) -> p a
graph_subst :: CoFunctor p => (a -> b) -> p (a, b) -> p a
data Assertion a
- = PrimAssert {
  - asserted_condition :: a -> Bool
  }
- | NotAssert {
  - asserted_negations :: Assertion a
  }
- | AndAssert {
  - asserted_conjunctions :: [Assertion a]
  }
- | OrAssert {
  - asserted_disjunctions :: [Assertion a]
  }

Documentation

type CoFunctor p = Contravariant p Source #

For exposition of classical logic used here, see "Lawvere,Rosebrugh: Sets for mathematics".

(x |>> f) |>> g == x |>> (f . g)
inverse_image g (inverse_image f x) == inverse_image (f . g) x

Notice, CoFunctor is nowadays in base, so please use Data.Functor.Contravariant.Contravariant

inverse_image :: CoFunctor p => (a -> b) -> p b -> p a Source #

(|>>) :: CoFunctor p => p b -> (a -> b) -> p a Source #

class Representable p where Source #

Associated Types

type Representation p :: * -> * Source #

Methods

represent :: Representation p a -> p a Source #

(!>) :: p a -> (Representation p a -> p a) -> p a Source #

Instances

Instances details

Representable IO Source #
Instance details Defined in Math.Tools.CoFunctor Associated Types type Representation IO :: Type -> Type Source # Methods represent :: Representation IO a -> IO a Source # (!>) :: IO a -> (Representation IO a -> IO a) -> IO a Source #
Representable List Source #
Instance details Defined in Math.Tools.CoFunctor Associated Types type Representation List :: Type -> Type Source # Methods represent :: Representation List a -> [a] Source # (!>) :: [a] -> (Representation List a -> [a]) -> [a] Source #

class Propositional p where Source #

Methods

runProposition :: p a -> a -> p () Source #

Instances

Instances details

Propositional Assertion Source #
Instance details Defined in Math.Tools.CoFunctor Methods runProposition :: Assertion a -> a -> Assertion () Source #
Propositional Prop Source #
Instance details Defined in Math.Tools.Prop Methods runProposition :: Prop a -> a -> Prop () Source #
Propositional ((:<-:) soc) Source #
Instance details Defined in Math.Graph.Action Methods runProposition :: (soc :<-: a) -> a -> soc :<-: () Source #

class Propositional p => BinaryLogic p where Source #

Methods

toBool :: p () -> Bool Source #

Instances

Instances details

BinaryLogic Assertion Source #
Instance details Defined in Math.Tools.CoFunctor Methods toBool :: Assertion () -> Bool Source #
BinaryLogic Prop Source #
Instance details Defined in Math.Tools.Prop Methods toBool :: Prop () -> Bool Source #

class CoFunctor p => Relational p where Source #

Methods

relation :: (a -> p b) -> p (a, b) Source #

unrelation :: p (a, b) -> a -> p b Source #

Instances

Instances details

Relational Prop Source #	relation and unrelation represent the natural isomorphism \[Hom(-,P(A)) \cong Sub(- \times A)\]
Instance details Defined in Math.Tools.Prop Methods relation :: (a -> Prop b) -> Prop (a, b) Source # unrelation :: Prop (a, b) -> a -> Prop b Source #
Relational ((:<-:) Bool) Source #
Instance details Defined in Math.Graph.Action Methods relation :: (a -> Bool :<-: b) -> Bool :<-: (a, b) Source # unrelation :: (Bool :<-: (a, b)) -> a -> Bool :<-: b Source #

class CoFunctor p => Existential p where Source #

Methods

direct_image :: (Universe a, Eq b) => (a -> b) -> p a -> p b Source #

universal_image :: (Universe a, Eq b) => (a -> b) -> p a -> p b Source #

Instances

Instances details

Existential Prop Source #
Instance details Defined in Math.Tools.Prop Methods direct_image :: (Universe a, Eq b) => (a -> b) -> Prop a -> Prop b Source # universal_image :: (Universe a, Eq b) => (a -> b) -> Prop a -> Prop b Source #

class CoFunctor p => Difference p minus | p -> minus where Source #

Methods

difference :: (p a -> p b) -> p (b `minus` a) Source #

undifference :: p (b `minus` a) -> p a -> p b Source #

class (Eq c, CoFunctor p) => HasEqualizers p c where Source #

Minimal complete definition

equalizer

Methods

equalizer :: (a -> c) -> (a -> c) -> p a Source #

pullback :: (a -> c) -> (b -> c) -> p (a, b) Source #

Instances

Instances details

Eq c => HasEqualizers Prop c Source #
Instance details Defined in Math.Tools.Prop Methods equalizer :: (a -> c) -> (a -> c) -> Prop a Source # pullback :: (a -> c) -> (b -> c) -> Prop (a, b) Source #
HasEqualizers ((:<-:) Bool) (Bool :<-: Bool) Source #
Instance details Defined in Math.Graph.Action Methods equalizer :: (a -> Bool :<-: Bool) -> (a -> Bool :<-: Bool) -> Bool :<-: a Source # pullback :: (a -> Bool :<-: Bool) -> (b -> Bool :<-: Bool) -> Bool :<-: (a, b) Source #

class Functor p => Topology p where Source #

Methods

arbitrary_union :: [p a] -> p a Source #

finite_intersect :: [p a] -> p a Source #

class HasTerminalObject t where Source #

Methods

terminal_arrow :: a -> t Source #

Instances

Instances details

HasTerminalObject () Source #
Instance details Defined in Math.Tools.CoFunctor Methods terminal_arrow :: a -> () Source #

class CoFunctor p => HasVariables p t where Source #

Methods

variable :: String -> p t Source #

class CoFunctor p => PropositionalLogic p where Source #

Methods

(-&-) :: p a -> p a -> p a Source #

(-|-) :: p a -> p a -> p a Source #

invert :: p a -> p a Source #

Instances

Instances details

PropositionalLogic Assertion Source #
Instance details Defined in Math.Tools.CoFunctor Methods (-&-) :: Assertion a -> Assertion a -> Assertion a Source # (-\|-) :: Assertion a -> Assertion a -> Assertion a Source # invert :: Assertion a -> Assertion a Source #
PropositionalLogic Prop Source #
Instance details Defined in Math.Tools.Prop Methods (-&-) :: Prop a -> Prop a -> Prop a Source # (-\|-) :: Prop a -> Prop a -> Prop a Source # invert :: Prop a -> Prop a Source #
PropositionalLogic ((:<-:) Bool) Source #
Instance details Defined in Math.Graph.Action Methods (-&-) :: (Bool :<-: a) -> (Bool :<-: a) -> Bool :<-: a Source # (-\|-) :: (Bool :<-: a) -> (Bool :<-: a) -> Bool :<-: a Source # invert :: (Bool :<-: a) -> Bool :<-: a Source #

class PropositionalLogic p => ModalLogic p where Source #

https://en.wikipedia.org/wiki/Modal_logic

Minimal complete definition

Nothing

Methods

eventually :: p a -> p a Source #

always :: p a -> p a Source #

class CoFunctor p => Continuous p where Source #

Methods

expand :: p (Either a b) -> (p a, p b) Source #

class CoFunctor p => SubtractiveLogic p where Source #

Methods

(-\-) :: p a -> p a -> p a Source #

Instances

Instances details

SubtractiveLogic Prop Source #
Instance details Defined in Math.Tools.Prop Methods (-\-) :: Prop a -> Prop a -> Prop a Source #

class CoFunctor p => ImplicativeLogic p where Source #

Methods

(-=>-) :: p a -> p a -> p a Source #

Instances

Instances details

ImplicativeLogic Assertion Source #
Instance details Defined in Math.Tools.CoFunctor Methods (-=>-) :: Assertion a -> Assertion a -> Assertion a Source #
ImplicativeLogic Prop Source #
Instance details Defined in Math.Tools.Prop Methods (-=>-) :: Prop a -> Prop a -> Prop a Source #
ImplicativeLogic ((:<-:) Bool) Source #
Instance details Defined in Math.Graph.Action Methods (-=>-) :: (Bool :<-: a) -> (Bool :<-: a) -> Bool :<-: a Source #

class CoFunctor p => BooleanLogic p where Source #

Methods

true :: p a Source #

Instances

Instances details

BooleanLogic Assertion Source #
Instance details Defined in Math.Tools.CoFunctor Methods true :: Assertion a Source #
BooleanLogic Prop Source #
Instance details Defined in Math.Tools.Prop Methods true :: Prop a Source #
BooleanLogic ((:<-:) Bool) Source #
Instance details Defined in Math.Graph.Action Methods true :: Bool :<-: a Source #

class CoFunctor p => UniversalLogic p where Source #

Methods

singleton :: Eq a => a -> p a Source #

all_members :: Universe a => p a Source #

Instances

Instances details

UniversalLogic Prop Source #
Instance details Defined in Math.Tools.Prop Methods singleton :: Eq a => a -> Prop a Source # all_members :: Universe a => Prop a Source #

class CoFunctor p => Universal p where Source #

Methods

exist :: Universe b => p (a, b) -> p a Source #

univ :: Universe b => p (a, b) -> p a Source #

member :: Propositional p => a -> p a -> p () Source #

isIn :: BinaryLogic p => a -> p a -> Bool Source #

isNotIn :: BinaryLogic p => a -> p a -> Bool Source #

terminal_part :: Propositional p => p () -> p () Source #

propositional_implication :: PropositionalLogic p => p a -> p a -> p a Source #

relative_complement :: PropositionalLogic p => p a -> p a -> p a Source #

intersect_list :: (BooleanLogic p, PropositionalLogic p) => [p a] -> p a Source #

union_list :: (BooleanLogic p, PropositionalLogic p) => [p a] -> p a Source #

characteristic :: BooleanLogic p => (a -> p ()) -> p a Source #

false_prop :: (BooleanLogic p, PropositionalLogic p) => p a Source #

(-<=>-) :: (ImplicativeLogic p, PropositionalLogic p) => p a -> p a -> p a Source #

symmetric_difference :: (PropositionalLogic p, SubtractiveLogic p) => p a -> p a -> p a Source #

boundary :: (PropositionalLogic p, BooleanLogic p, SubtractiveLogic p) => p a -> p a Source #

curry_subst :: CoFunctor p => ((a, b) -> c) -> p (b -> c) -> p a Source #

uncurry_subst :: CoFunctor p => (a -> b -> c) -> p c -> p (a, b) Source #

dualize :: Difference p minus => (a -> b) -> p (a `minus` b) Source #

coin1 :: CoFunctor p => p a -> p (a, b) Source #

coin2 :: CoFunctor p => p b -> p (a, b) Source #

cofst :: CoFunctor p => p (Either a b) -> p a Source #

cosnd :: CoFunctor p => p (Either a b) -> p b Source #

cocase :: CoFunctor p => (Either a b -> c) -> p c -> (p a, p b) Source #

copair :: (Propositional p, BooleanLogic p) => p a -> p b -> p (Either a b) Source #

pair_subst :: CoFunctor p => (a -> b) -> (a -> c) -> p (b, c) -> p a Source #

graph_subst :: CoFunctor p => (a -> b) -> p (a, b) -> p a Source #

data Assertion a Source #

Constructors

PrimAssert
Fields asserted_condition :: a -> Bool
NotAssert
Fields asserted_negations :: Assertion a
AndAssert
Fields asserted_conjunctions :: [Assertion a]
OrAssert
Fields asserted_disjunctions :: [Assertion a]

Instances

Instances details

Contravariant Assertion Source #
Instance details Defined in Math.Tools.CoFunctor Methods contramap :: (a' -> a) -> Assertion a -> Assertion a' # (>$) :: b -> Assertion b -> Assertion a #
BinaryLogic Assertion Source #
Instance details Defined in Math.Tools.CoFunctor Methods toBool :: Assertion () -> Bool Source #
BooleanLogic Assertion Source #
Instance details Defined in Math.Tools.CoFunctor Methods true :: Assertion a Source #
ImplicativeLogic Assertion Source #
Instance details Defined in Math.Tools.CoFunctor Methods (-=>-) :: Assertion a -> Assertion a -> Assertion a Source #
Propositional Assertion Source #
Instance details Defined in Math.Tools.CoFunctor Methods runProposition :: Assertion a -> a -> Assertion () Source #
PropositionalLogic Assertion Source #
Instance details Defined in Math.Tools.CoFunctor Methods (-&-) :: Assertion a -> Assertion a -> Assertion a Source # (-\|-) :: Assertion a -> Assertion a -> Assertion a Source # invert :: Assertion a -> Assertion a Source #