| Copyright | (c) Matt Noonan 2018 |
|---|---|
| License | BSD-style |
| Maintainer | matt.noonan@gmail.com |
| Portability | portable |
| Safe Haskell | None |
| Language | Haskell2010 |
Theory.Equality
Description
Synopsis
- data Equals x y
- type (==) x y = x `Equals` y
- (==.) :: Proof (x == y) -> Proof (y == z) -> Proof (x == z)
- apply :: forall f n x x'. (Argument f n, GetArg f n ~ x) => Arg n -> (x == x') -> Proof (f == SetArg f n x')
- substitute :: (Argument f n, GetArg f n ~ x) => Arg n -> (x == x') -> f -> Proof (SetArg f n x')
- substituteL :: (Argument f n, GetArg f n ~ x) => Arg n -> (x == x') -> (f == g) -> Proof (SetArg f n x' == g)
- substituteR :: (Argument f n, GetArg f n ~ x) => Arg n -> (x == x') -> (g == f) -> Proof (g == SetArg f n x')
- same :: Lawful Eq a => (a ~~ x) -> (a ~~ y) -> Maybe (Proof (x == y))
- reflectEq :: Proof (x == y) -> x :~: y
- propEq :: (x :~: y) -> Proof (x == y)
Documentation
The Equals relation is used to express equality between two entities.
Given an equality, you are then able to substitute one side of the equality
for the other, anywhere you please.
Instances
| Transitive Equals # | |
Defined in Logic.Classes | |
| Symmetric Equals # | |
| Reflexive Equals # | |
Defined in Logic.Classes | |
| Argument (Equals x y :: *) 1 # | |
| Argument (Equals x y :: *) 0 # | |
| Argument (Equals x y :: *) RHS # | |
| Argument (Equals x y :: *) LHS # | |
| type GetArg (Equals x y :: *) 1 # | |
Defined in Theory.Equality | |
| type GetArg (Equals x y :: *) 0 # | |
Defined in Theory.Equality | |
| type SetArg (Equals x y :: *) 1 y' # | |
Defined in Theory.Equality | |
| type SetArg (Equals x y :: *) 0 x' # | |
Defined in Theory.Equality | |
| type GetArg (Equals x y :: *) RHS # | |
Defined in Theory.Equality | |
| type GetArg (Equals x y :: *) LHS # | |
Defined in Theory.Equality | |
| type SetArg (Equals x y :: *) RHS y' # | |
| type SetArg (Equals x y :: *) LHS x' # | |
Substitutions and equational reasoning
apply :: forall f n x x'. (Argument f n, GetArg f n ~ x) => Arg n -> (x == x') -> Proof (f == SetArg f n x') #
Apply a function to both sides of an equality.
substitute :: (Argument f n, GetArg f n ~ x) => Arg n -> (x == x') -> f -> Proof (SetArg f n x') #
Given a formula and an equality over ones of its arguments, replace the left-hand side of the equality with the right-hand side.
substituteL :: (Argument f n, GetArg f n ~ x) => Arg n -> (x == x') -> (f == g) -> Proof (SetArg f n x' == g) #
Substitute x' for x under the function f, on the left-hand side
of an equality.
substituteR :: (Argument f n, GetArg f n ~ x) => Arg n -> (x == x') -> (g == f) -> Proof (g == SetArg f n x') #
Substitute x' for x under the function f, on the right-hand side
of an equality.
Relating to other forms of equality
same :: Lawful Eq a => (a ~~ x) -> (a ~~ y) -> Maybe (Proof (x == y)) #
Test if the two named arguments are equal and, if so, produce a proof of equality for the names.
reflectEq :: Proof (x == y) -> x :~: y #
Reflect an equality between x and y into a propositional
equality between the types x and y.
newtype Bob = Bob Defn bob :: Int ~~ Bob bob = defn 42 needsBob :: (Int ~~ Bob) -> Int needsBob x = the x + the x isBob :: (Int ~~ name) -> Maybe (Proof (name == Bob)) isBob = same x bob f :: (Int ~~ name) -> Int f x = case reflectEq <$> isBob x of Nothing -> 17 Just Refl -> needsBob x x