Copyright | (c) Matt Noonan 2018 |
---|---|
License | BSD-style |
Maintainer | matt.noonan@gmail.com |
Portability | portable |
Safe Haskell | None |
Language | Haskell2010 |
Synopsis
- class Reflexive r where
- class Symmetric c where
- class Transitive c where
- transitive :: Proof (c p q) -> Proof (c q r) -> Proof (c p r)
- transitive' :: Transitive c => Proof (c q r) -> Proof (c p q) -> Proof (c p r)
- class Idempotent c where
- idempotent :: Proof (c p p == p)
- class Commutative c where
- commutative :: Proof (c p q == c q p)
- class Associative c where
- associative :: Proof (c p (c q r) == c (c p q) r)
- class DistributiveL c c' where
- distributiveL :: Proof (c p (c' q r) == c' (c p q) (c p r))
- class DistributiveR c c' where
- distributiveR :: Proof (c (c' p q) r == c' (c p r) (c q r))
- class Injective f where
Algebraic properties
class Reflexive r where Source #
A binary relation R is reflexive if, for all x,
R(x, x) is true. The Reflexive r
typeclass provides
a single method, refl :: Proof (r x x)
,
proving R(x, x) for an arbitrary x.
Within the module where the relation R
is defined, you can
declare R
to be reflexive with an empty instance:
-- Define a reflexive binary relation data SameColor p q instance Reflexive SameColor
Nothing
class Symmetric c where Source #
A binary relation R is symmetric if, for all x and y,
R(x, y) is true if and only if R(y, x) is true. The
Symmetric
typeclass provides
a single method, symmetric :: r x y -> Proof (r y x)
,
proving the implication "R(x, y) implies R(y, x)".
Within the module where R
is defined, you can
declare R
to be symmetric with an empty instance:
-- Define a symmetric binary relation data NextTo p q instance Symmetric NextTo
Nothing
class Transitive c where Source #
A binary relation R is transitive if, for all x, y, z,
if R(x, y) is true and R(y, z) is true, then R(x, z) is true.
The Transitive r
typeclass provides
a single method, transitive :: r x y -> r y z -> Proof (r x z)
,
proving R(x, z) from R(x, y) and R(y, z).
Within the module where R
is defined, you can
declare R
to be transitive with an empty instance:
-- Define a transitive binary relation data CanReach p q instance Transitive CanReach
Nothing
Instances
Transitive (Equals :: k -> k -> Type) Source # | |
Defined in Logic.Classes |
transitive' :: Transitive c => Proof (c q r) -> Proof (c p q) -> Proof (c p r) Source #
transitive
, with the arguments flipped.
class Idempotent c where Source #
A binary operation #
is idempotent if x # x == x
for all x
.
The Idempotent c
typeclass provides a single method,
idempotent :: Proof (c p p == p)
.
Within the module where F
is defined, you can declare F
to be
idempotent with an empty instance:
-- Define an idempotent binary operation data Union x y instance Idempotent Union
Nothing
idempotent :: Proof (c p p == p) Source #
class Commutative c where Source #
A binary operation #
is commutative if x x
for all x
and y
.
The Commutative c
typeclass provides a single method,
commutative :: Proof (c x y == c y x)
.
Within the module where F
is defined, you can declare F
to be
commutative with an empty instance:
-- Define a commutative binary operation data Union x y instance Commutative Union
Nothing
commutative :: Proof (c p q == c q p) Source #
class Associative c where Source #
A binary operation #
is associative if x z) == (x z
for
all x
, y
, and z
.
The Associative c
typeclass provides a single method,
associative :: Proof (c x (c y z) == c (c x y) z)
.
Within the module where F
is defined, you can declare F
to be
associative with an empty instance:
-- Define an associative binary operation data Union x y instance Associative Union
Nothing
associative :: Proof (c p (c q r) == c (c p q) r) Source #
Instances
Associative (Or :: Type -> Type -> Type) Source # | |
Defined in Logic.Propositional | |
Associative (And :: Type -> Type -> Type) Source # | |
Defined in Logic.Propositional |
class DistributiveL c c' where Source #
A binary operation #
distributes over %
on the left if
x y) % (x # z)
for
all x
, y
, and z
.
The DistributiveL c c'
typeclass provides a single method,
distributiveL :: Proof (c x (c' y z) == c' (c x y) (c x z))
.
Within the module where F
and G
are defined, you can declare F
to
distribute over G
on the left with an empty instance:
-- xUnion
(yIntersect
z) == (xUnion
y)Intersect
(xUnion
z) data Union x y data Intersect x y instance DistributiveL Union Intersect
Nothing
distributiveL :: Proof (c p (c' q r) == c' (c p q) (c p r)) Source #
Instances
DistributiveL (And :: k -> Type -> Type) (And :: Type -> Type -> Type) Source # | |
DistributiveL (Or :: k -> Type -> Type) (Or :: Type -> Type -> Type) Source # | |
DistributiveL (Or :: k -> Type -> Type) (And :: Type -> Type -> Type) Source # | |
DistributiveL (And :: k -> Type -> Type) (Or :: Type -> Type -> Type) Source # | |
class DistributiveR c c' where Source #
A binary operation #
distributes over %
on the right if
(x % y) z) % (y # z)
for
all x
, y
, and z
.
The DistributiveR c c'
typeclass provides a single method,
distributiveR :: Proof (c (c' x y) z == c' (c x z) (c y z))
.
Within the module where F
and G
are defined, you can declare F
to
distribute over G
on the left with an empty instance:
-- (xIntersect
y)Union
z == (xUnion
z)Intersect
(yUnion
z) data Union x y data Intersect x y instance DistributiveR Union Intersect
Nothing
distributiveR :: Proof (c (c' p q) r == c' (c p r) (c q r)) Source #
Instances
DistributiveR (And :: Type -> k -> Type) (And :: Type -> Type -> Type) Source # | |
DistributiveR (Or :: Type -> k -> Type) (Or :: Type -> Type -> Type) Source # | |
DistributiveR (Or :: Type -> k -> Type) (And :: Type -> Type -> Type) Source # | |
DistributiveR (And :: Type -> k -> Type) (Or :: Type -> Type -> Type) Source # | |
class Injective f where Source #
A function f
is injective if f x == f y
implies x == y
.
The Injective f
typeclass provides a single method,
elim_inj :: (f x == f y) -> Proof (x == y)
.
Within the module where F
is defined, you can declare F
to be
injective with an empty instance:
-- {x} == {y} implies x == y. data Singleton x instance Injective Singleton
Nothing