Data.Leibniz

newtype Leibniz a b

Two types are equal if they are equal in all contexts.

Constructors

• Leibniz (forall f. f a -> f b)

Instances

• Semigroupoid Leibniz
• Category Leibniz

Operator alias for Data.Leibniz.Leibniz (non-associative / precedence 4)

runLeibniz :: forall f a b. a ~ b -> f a -> f b

Unpack a Leibniz equality.

coerce :: forall a b. a ~ b -> a -> b

Coerce a value of type a to a value of the Leibniz-equal type b.

coerceSymm :: forall a b. a ~ b -> b -> a

Coerce a value of type b to a value of the Leibniz-equal type a.

symm :: forall a b. a ~ b -> b ~ a

Equality is symmetric.

liftLeibniz :: forall f a b. a ~ b -> (f a) ~ (f b)

Lift equality over a type constructor.

liftLeibniz1of2 :: forall f a b c. a ~ b -> (f a c) ~ (f b c)

Lift equality over a type constructor.

liftLeibniz2of2 :: forall f a b c. a ~ b -> (f c a) ~ (f c b)

Lift equality over a type constructor.

liftLeibniz1of3 :: forall f a b c d. a ~ b -> (f a c d) ~ (f b c d)

Lift equality over a type constructor.

liftLeibniz2of3 :: forall f a b c d. a ~ b -> (f c a d) ~ (f c b d)

Lift equality over a type constructor.

liftLeibniz3of3 :: forall f a b c d. a ~ b -> (f c d a) ~ (f c d b)

Lift equality over a type constructor.

applyLeibniz :: forall f g a b c d. (f c) ~ (g d) -> a ~ b -> (f a) ~ (g b)

Apply an equality of type constructors to an equality of types.

applyLeibniz1of2 :: forall f g f1 f2 g1 g2 a b c. (f f1 f2) ~ (g g1 g2) -> a ~ b -> (f a c) ~ (g b c)

Apply an equality of type constructors to an equality of types.

applyLeibniz2of2 :: forall f g f1 f2 g1 g2 a b c. (f f1 f2) ~ (g g1 g2) -> a ~ b -> (f c a) ~ (g c b)

Apply an equality of type constructors to an equality of types.

applyLeibniz1of3 :: forall f g f1 f2 f3 g1 g2 g3 a b c d. (f f1 f2 f3) ~ (g g1 g2 g3) -> a ~ b -> (f a c d) ~ (g b c d)

Apply an equality of type constructors to an equality of types.

applyLeibniz2of3 :: forall f g f1 f2 f3 g1 g2 g3 a b c d. (f f1 f2 f3) ~ (g g1 g2 g3) -> a ~ b -> (f c a d) ~ (g c b d)

Apply an equality of type constructors to an equality of types.

applyLeibniz3of3 :: forall f g f1 f2 f3 g1 g2 g3 a b c d. (f f1 f2 f3) ~ (g g1 g2 g3) -> a ~ b -> (f c d a) ~ (g c d b)

Apply an equality of type constructors to an equality of types.

lowerLeibniz :: forall f g a b. (f a) ~ (g b) -> a ~ b

Every type constructor in PureScript is injective.

lowerLeibniz1of2 :: forall f g a b c d. (f a c) ~ (g b d) -> a ~ b

Every type constructor in PureScript is injective.

lowerLeibniz2of2 :: forall f g a b c d. (f a c) ~ (g b d) -> c ~ d

Every type constructor in PureScript is injective.

lowerLeibniz1of3 :: forall f g a b c d e h. (f a b c) ~ (g d e h) -> a ~ d

Every type constructor in PureScript is injective.

lowerLeibniz2of3 :: forall f g a b c d e h. (f a b c) ~ (g d e h) -> b ~ e

Every type constructor in PureScript is injective.

lowerLeibniz3of3 :: forall f g a b c d e h. (f a b c) ~ (g d e h) -> c ~ h

Every type constructor in PureScript is injective.

class Distinguish a b c o | a b c -> o

This class is used in the definition of the refute function.

Its job is to distinguish the two types a and b (if possible) by mapping them to the different output types Unit and Void respectively.

Instances

• Distinguish a b a Unit
• Distinguish a b b Void

refute :: forall a b r. Distinguish a b b Void => a ~ b -> r

Refute a type equality for two types which are not definitionally equal.

For example, in the REPL:

> import Data.Leibniz

> :type \(l :: String ~ Int) -> refute l
forall r. Leibniz String Int -> r

> :type \(l :: String ~ String) -> refute l
Error found:
  Could not match type Unit with type Void

The error message here is due to the way in which the Distinguish class decides apartness.