Module

Data.Leibniz

Package
purescript-leibniz
Repository
paf31/purescript-leibniz

This module defines a data type for Leibniz equality.

#Leibniz Source

newtype Leibniz a b

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

Constructors

Instances

#type (~) Source

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

#runLeibniz Source

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

Unpack a Leibniz equality.

#coerce Source

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

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

#coerceSymm Source

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

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

#symm Source

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

Equality is symmetric.

#liftLeibniz Source

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

Lift equality over a type constructor.

#liftLeibniz1of2 Source

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

Lift equality over a type constructor.

#liftLeibniz2of2 Source

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

Lift equality over a type constructor.

#liftLeibniz1of3 Source

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

Lift equality over a type constructor.

#liftLeibniz2of3 Source

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

Lift equality over a type constructor.

#liftLeibniz3of3 Source

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

Lift equality over a type constructor.

#applyLeibniz Source

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

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

#applyLeibniz1of2 Source

applyLeibniz1of2 :: forall c b a g2 g1 f2 f1 g f. (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 Source

applyLeibniz2of2 :: forall c b a g2 g1 f2 f1 g f. (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 Source

applyLeibniz1of3 :: forall d c b a g3 g2 g1 f3 f2 f1 g f. (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 Source

applyLeibniz2of3 :: forall d c b a g3 g2 g1 f3 f2 f1 g f. (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 Source

applyLeibniz3of3 :: forall d c b a g3 g2 g1 f3 f2 f1 g f. (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 Source

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

Every type constructor in PureScript is injective.

#lowerLeibniz1of2 Source

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

Every type constructor in PureScript is injective.

#lowerLeibniz2of2 Source

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

Every type constructor in PureScript is injective.

#lowerLeibniz1of3 Source

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

Every type constructor in PureScript is injective.

#lowerLeibniz2of3 Source

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

Every type constructor in PureScript is injective.

#lowerLeibniz3of3 Source

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

Every type constructor in PureScript is injective.

#Distinguish Source

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

#refute Source

refute :: forall r b a. 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.

Modules
Data.Leibniz