Theory.Equality

Documentation

data Equals x y

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 :: k -> k -> Type)

Defined in Logic.Classes

Methods

transitive :: Proof (Equals p q) -> Proof (Equals q r) -> Proof (Equals p r)

Symmetric (Equals :: k -> k -> Type)

Defined in Logic.Classes

Methods

symmetric :: Proof (Equals p q) -> Proof (Equals q p)

Reflexive (Equals :: k -> k -> Type)

Defined in Logic.Classes

Methods

refl :: Proof (Equals x x)

Argument (Equals x y :: Type) 1

Defined in Theory.Equality

Associated Types

type GetArg (Equals x y) 1 :: k

type SetArg (Equals x y) 1 x :: k1

Argument (Equals x y :: Type) 0

Defined in Theory.Equality

Associated Types

type GetArg (Equals x y) 0 :: k

type SetArg (Equals x y) 0 x :: k1

Argument (Equals x y :: Type) RHS

Defined in Theory.Equality

Associated Types

type GetArg (Equals x y) RHS :: k

type SetArg (Equals x y) RHS x :: k1

Argument (Equals x y :: Type) LHS

Defined in Theory.Equality

Associated Types

type GetArg (Equals x y) LHS :: k

type SetArg (Equals x y) LHS x :: k1

type GetArg (Equals x y :: Type) 1

Defined in Theory.Equality

type GetArg (Equals x y :: Type) 1 = y

type GetArg (Equals x y :: Type) 0

Defined in Theory.Equality

type GetArg (Equals x y :: Type) 0 = x

type SetArg (Equals x y :: Type) 1 y'

Defined in Theory.Equality

type SetArg (Equals x y :: Type) 1 y' = Equals x y'

type SetArg (Equals x y :: Type) 0 x'

Defined in Theory.Equality

type SetArg (Equals x y :: Type) 0 x' = Equals x' y

type GetArg (Equals x y :: Type) RHS

Defined in Theory.Equality

type GetArg (Equals x y :: Type) RHS = y

type GetArg (Equals x y :: Type) LHS

Defined in Theory.Equality

type GetArg (Equals x y :: Type) LHS = x

type SetArg (Equals x y :: Type) RHS y'

Defined in Theory.Equality

type SetArg (Equals x y :: Type) RHS y' = Equals x y'

type SetArg (Equals x y :: Type) LHS x'

Defined in Theory.Equality

type SetArg (Equals x y :: Type) LHS x' = Equals x' y

type (==) x y = x `Equals` y infix 4

An infix alias for Equals.

Substitutions and equational reasoning

(==.) :: Proof (x == y) -> Proof (y == z) -> Proof (x == z)

Chain equalities, a la Liquid Haskell.

apply :: forall f n x x'. (Argument f n, GetArg f n ~ x) => Arg n -> Proof (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 -> Proof (x == x') -> f -> Proof (SetArg f n x')

Given a formula and an equality over one 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 -> Proof (x == x') -> Proof (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 -> Proof (x == x') -> Proof (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

propEq :: (x :~: y) -> Proof (x == y)

Convert a propositional equality between the types x and y into a proof of x == y.