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

Methods

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

Symmetric Equals

Methods

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

Reflexive Equals

Methods

refl :: Proof (Equals x x)

Argument * Nat (Equals x y) 1

Associated Types

type GetArg 1 (Equals x y) (f :: Equals x y) (n :: 1) :: k1

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

Argument * Nat (Equals x y) 0

Associated Types

type GetArg 0 (Equals x y) (f :: Equals x y) (n :: 0) :: k1

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

Argument * * (Equals x y) RHS

Associated Types

type GetArg RHS (Equals x y) (f :: Equals x y) (n :: RHS) :: k1

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

Argument * * (Equals x y) LHS

Associated Types

type GetArg LHS (Equals x y) (f :: Equals x y) (n :: LHS) :: k1

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

type GetArg Nat * (Equals x y) 1

type GetArg Nat * (Equals x y) 1 = y

type GetArg Nat * (Equals x y) 0

type GetArg Nat * (Equals x y) 0 = x

type SetArg Nat * (Equals x y) 1 y'

type SetArg Nat * (Equals x y) 1 y' = Equals x y'

type SetArg Nat * (Equals x y) 0 x'

type SetArg Nat * (Equals x y) 0 x' = Equals x' y

type GetArg * * (Equals x y) RHS

type GetArg * * (Equals x y) RHS = y

type GetArg * * (Equals x y) LHS

type GetArg * * (Equals x y) LHS = x

type SetArg * * (Equals x y) RHS y'

type SetArg * * (Equals x y) RHS y' = Equals x y'

type SetArg * * (Equals x y) LHS x'

type SetArg * * (Equals x y) 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 -> (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

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

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