Proof.Equational

Documentation

data (a :: k) :~: (b :: k) :: forall k. k -> k -> Type where infix 4

Propositional equality. If a :~: b is inhabited by some terminating value, then the type a is the same as the type b. To use this equality in practice, pattern-match on the a :~: b to get out the Refl constructor; in the body of the pattern-match, the compiler knows that a ~ b.

Since: base-4.7.0.0

Constructors

Refl :: forall k (a :: k) (b :: k). a :~: a

Instances

Equality ((:=:) :: k -> k -> Type)

Defined in Proof.Equational

Methods

symmetry :: (a :=: b) -> b :=: a

Preorder ((:=:) :: k -> k -> Type)

Defined in Proof.Equational

Methods

reflexivity :: proxy a -> a :=: a

transitivity :: (a :=: b) -> (b :=: c) -> a :=: c

TestEquality ((:~:) a :: k -> Type)

Since: base-4.7.0.0

Defined in Data.Type.Equality

Methods

testEquality :: (a :~: a0) -> (a :~: b) -> Maybe (a0 :~: b)

a ~ b => Bounded (a :~: b)

Since: base-4.7.0.0

Defined in Data.Type.Equality

Methods

minBound :: a :~: b

maxBound :: a :~: b

a ~ b => Enum (a :~: b)

Since: base-4.7.0.0

Defined in Data.Type.Equality

Methods

succ :: (a :~: b) -> a :~: b

pred :: (a :~: b) -> a :~: b

toEnum :: Int -> a :~: b

fromEnum :: (a :~: b) -> Int

enumFrom :: (a :~: b) -> [a :~: b]

enumFromThen :: (a :~: b) -> (a :~: b) -> [a :~: b]

enumFromTo :: (a :~: b) -> (a :~: b) -> [a :~: b]

enumFromThenTo :: (a :~: b) -> (a :~: b) -> (a :~: b) -> [a :~: b]

Eq (a :~: b)

Since: base-4.7.0.0

Defined in Data.Type.Equality

Methods

(==) :: (a :~: b) -> (a :~: b) -> Bool

(/=) :: (a :~: b) -> (a :~: b) -> Bool

(a ~ b, Data a) => Data (a :~: b)

Since: base-4.7.0.0

Defined in Data.Data

Methods

gfoldl :: (forall d b0. Data d => c (d -> b0) -> d -> c b0) -> (forall g. g -> c g) -> (a :~: b) -> c (a :~: b)

gunfold :: (forall b0 r. Data b0 => c (b0 -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (a :~: b)

toConstr :: (a :~: b) -> Constr

dataTypeOf :: (a :~: b) -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (a :~: b))

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (a :~: b))

gmapT :: (forall b0. Data b0 => b0 -> b0) -> (a :~: b) -> a :~: b

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> (a :~: b) -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> (a :~: b) -> r

gmapQ :: (forall d. Data d => d -> u) -> (a :~: b) -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> (a :~: b) -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b)

Ord (a :~: b)

Since: base-4.7.0.0

Defined in Data.Type.Equality

Methods

compare :: (a :~: b) -> (a :~: b) -> Ordering

(<) :: (a :~: b) -> (a :~: b) -> Bool

(<=) :: (a :~: b) -> (a :~: b) -> Bool

(>) :: (a :~: b) -> (a :~: b) -> Bool

(>=) :: (a :~: b) -> (a :~: b) -> Bool

max :: (a :~: b) -> (a :~: b) -> a :~: b

min :: (a :~: b) -> (a :~: b) -> a :~: b

a ~ b => Read (a :~: b)

Since: base-4.7.0.0

Defined in Data.Type.Equality

Methods

readsPrec :: Int -> ReadS (a :~: b)

readList :: ReadS [a :~: b]

readPrec :: ReadPrec (a :~: b)

readListPrec :: ReadPrec [a :~: b]

Show (a :~: b)

Since: base-4.7.0.0

Defined in Data.Type.Equality

Methods

showsPrec :: Int -> (a :~: b) -> ShowS

show :: (a :~: b) -> String

showList :: [a :~: b] -> ShowS

Empty (False :~: True)

Defined in Proof.Propositional

Methods

eliminate :: (False :~: True) -> x

Empty (True :~: False)

Defined in Proof.Propositional

Methods

eliminate :: (True :~: False) -> x

Empty (LT :~: EQ)

Defined in Proof.Propositional

Methods

eliminate :: (LT :~: EQ) -> x

Empty (LT :~: GT)

Defined in Proof.Propositional

Methods

eliminate :: (LT :~: GT) -> x

Empty (EQ :~: LT)

Defined in Proof.Propositional

Methods

eliminate :: (EQ :~: LT) -> x

Empty (EQ :~: GT)

Defined in Proof.Propositional

Methods

eliminate :: (EQ :~: GT) -> x

Empty (GT :~: LT)

Defined in Proof.Propositional

Methods

eliminate :: (GT :~: LT) -> x

Empty (GT :~: EQ)

Defined in Proof.Propositional

Methods

eliminate :: (GT :~: EQ) -> x

Empty (() :~: Int)

Defined in Proof.Propositional

Methods

eliminate :: (() :~: Int) -> x

Empty (0 :~: 1)

Defined in Proof.Propositional

Methods

eliminate :: (0 :~: 1) -> x

Inhabited (n :~: n)

Defined in Proof.Propositional

Methods

trivial :: n :~: n

type (:=:) = (:~:) infix 4

sym :: (a :~: b) -> b :~: a

Symmetry of equality

trans :: (a :~: b) -> (b :~: c) -> a :~: c

Transitivity of equality

class Preorder eq => Equality (eq :: k -> k -> *) where

Methods

symmetry :: eq a b -> eq b a

Instances

Equality ((:=:) :: k -> k -> Type)

Defined in Proof.Equational

Methods

symmetry :: (a :=: b) -> b :=: a

Equality (Leibniz :: k -> k -> Type)

Defined in Proof.Equational

Methods

symmetry :: Leibniz a b -> Leibniz b a

class Preorder (eq :: k -> k -> *) where

Methods

reflexivity :: proxy a -> eq a a

transitivity :: eq a b -> eq b c -> eq a c

Instances

Preorder (Leibniz :: k -> k -> Type)

Defined in Proof.Equational

Methods

reflexivity :: proxy a -> Leibniz a a

transitivity :: Leibniz a b -> Leibniz b c -> Leibniz a c

Preorder ((:=:) :: k -> k -> Type)

Defined in Proof.Equational

Methods

reflexivity :: proxy a -> a :=: a

transitivity :: (a :=: b) -> (b :=: c) -> a :=: c

Preorder ((->) :: Type -> Type -> Type)

Defined in Proof.Equational

Methods

reflexivity :: proxy a -> a -> a

transitivity :: (a -> b) -> (b -> c) -> a -> c

reflexivity' :: Preorder r => r x x

type (:\/:) a b = Either a b infixr 2

type (:/\:) a b = (a, b) infixr 3

(=<=) :: Preorder r => r x y -> Reason r y z -> r x z infixl 4

(=>=) :: Preorder r => r y z -> Reason r x y -> r x z infixl 4

(=~=) :: r x y -> proxy y -> r x y infixl 4

data Leibniz a b

Constructors

Leibniz

Fields

• apply :: forall f. f a -> f b

Instances

Equality (Leibniz :: k -> k -> Type)

Defined in Proof.Equational

Methods

symmetry :: Leibniz a b -> Leibniz b a

Preorder (Leibniz :: k -> k -> Type)

Defined in Proof.Equational

Methods

reflexivity :: proxy a -> Leibniz a a

transitivity :: Leibniz a b -> Leibniz b c -> Leibniz a c

data Reason eq x y where

Constructors

Because :: proxy y -> eq x y -> Reason eq x y infix 5

because :: proxy y -> eq x y -> Reason eq x y infix 5

by :: proxy y -> eq x y -> Reason eq x y

(===) :: Equality eq => eq x y -> Reason eq y z -> eq x z infixl 4

start :: Preorder eq => proxy a -> eq a a

byDefinition :: Preorder eq => eq a a

admitted :: Reason eq x y

Warning: There are some goals left yet unproven.

data Proxy (t :: k) :: forall k. k -> Type

Proxy is a type that holds no data, but has a phantom parameter of arbitrary type (or even kind). Its use is to provide type information, even though there is no value available of that type (or it may be too costly to create one).

Historically, Proxy :: Proxy a is a safer alternative to the 'undefined :: a' idiom.

>>> Proxy :: Proxy (Void, Int -> Int)
Proxy

Proxy can even hold types of higher kinds,

>>> Proxy :: Proxy Either
Proxy

>>> Proxy :: Proxy Functor
Proxy

>>> Proxy :: Proxy complicatedStructure
Proxy

Constructors

Proxy

Instances

Generic1 (Proxy :: k -> Type)

Defined in GHC.Generics

Associated Types

type Rep1 Proxy :: k -> Type

Methods

from1 :: Proxy a -> Rep1 Proxy a

to1 :: Rep1 Proxy a -> Proxy a

Monad (Proxy :: Type -> Type)

Since: base-4.7.0.0

Defined in Data.Proxy

Methods

(>>=) :: Proxy a -> (a -> Proxy b) -> Proxy b

(>>) :: Proxy a -> Proxy b -> Proxy b

return :: a -> Proxy a

fail :: String -> Proxy a

Functor (Proxy :: Type -> Type)

Since: base-4.7.0.0

Defined in Data.Proxy

Methods

fmap :: (a -> b) -> Proxy a -> Proxy b

(<$) :: a -> Proxy b -> Proxy a

Applicative (Proxy :: Type -> Type)

Since: base-4.7.0.0

Defined in Data.Proxy

Methods

pure :: a -> Proxy a

(<*>) :: Proxy (a -> b) -> Proxy a -> Proxy b

liftA2 :: (a -> b -> c) -> Proxy a -> Proxy b -> Proxy c

(*>) :: Proxy a -> Proxy b -> Proxy b

(<*) :: Proxy a -> Proxy b -> Proxy a

Foldable (Proxy :: Type -> Type)

Since: base-4.7.0.0

Defined in Data.Foldable

Methods

fold :: Monoid m => Proxy m -> m

foldMap :: Monoid m => (a -> m) -> Proxy a -> m

foldr :: (a -> b -> b) -> b -> Proxy a -> b

foldr' :: (a -> b -> b) -> b -> Proxy a -> b

foldl :: (b -> a -> b) -> b -> Proxy a -> b

foldl' :: (b -> a -> b) -> b -> Proxy a -> b

foldr1 :: (a -> a -> a) -> Proxy a -> a

foldl1 :: (a -> a -> a) -> Proxy a -> a

toList :: Proxy a -> [a]

null :: Proxy a -> Bool

length :: Proxy a -> Int

elem :: Eq a => a -> Proxy a -> Bool

maximum :: Ord a => Proxy a -> a

minimum :: Ord a => Proxy a -> a

sum :: Num a => Proxy a -> a

product :: Num a => Proxy a -> a

Traversable (Proxy :: Type -> Type)

Since: base-4.7.0.0

Defined in Data.Traversable

Methods

traverse :: Applicative f => (a -> f b) -> Proxy a -> f (Proxy b)

sequenceA :: Applicative f => Proxy (f a) -> f (Proxy a)

mapM :: Monad m => (a -> m b) -> Proxy a -> m (Proxy b)

sequence :: Monad m => Proxy (m a) -> m (Proxy a)

Alternative (Proxy :: Type -> Type)

Since: base-4.9.0.0

Defined in Data.Proxy

Methods

empty :: Proxy a

(<|>) :: Proxy a -> Proxy a -> Proxy a

some :: Proxy a -> Proxy [a]

many :: Proxy a -> Proxy [a]

MonadPlus (Proxy :: Type -> Type)

Since: base-4.9.0.0

Defined in Data.Proxy

Methods

mzero :: Proxy a

mplus :: Proxy a -> Proxy a -> Proxy a

Bounded (Proxy t)

Since: base-4.7.0.0

Defined in Data.Proxy

Methods

minBound :: Proxy t

maxBound :: Proxy t

Enum (Proxy s)

Since: base-4.7.0.0

Defined in Data.Proxy

Methods

succ :: Proxy s -> Proxy s

pred :: Proxy s -> Proxy s

toEnum :: Int -> Proxy s

fromEnum :: Proxy s -> Int

enumFrom :: Proxy s -> [Proxy s]

enumFromThen :: Proxy s -> Proxy s -> [Proxy s]

enumFromTo :: Proxy s -> Proxy s -> [Proxy s]

enumFromThenTo :: Proxy s -> Proxy s -> Proxy s -> [Proxy s]

Eq (Proxy s)

Since: base-4.7.0.0

Defined in Data.Proxy

Methods

(==) :: Proxy s -> Proxy s -> Bool

(/=) :: Proxy s -> Proxy s -> Bool

Data t => Data (Proxy t)

Since: base-4.7.0.0

Defined in Data.Data

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Proxy t -> c (Proxy t)

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Proxy t)

toConstr :: Proxy t -> Constr

dataTypeOf :: Proxy t -> DataType

dataCast1 :: Typeable t0 => (forall d. Data d => c (t0 d)) -> Maybe (c (Proxy t))

dataCast2 :: Typeable t0 => (forall d e. (Data d, Data e) => c (t0 d e)) -> Maybe (c (Proxy t))

gmapT :: (forall b. Data b => b -> b) -> Proxy t -> Proxy t

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Proxy t -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Proxy t -> r

gmapQ :: (forall d. Data d => d -> u) -> Proxy t -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Proxy t -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Proxy t -> m (Proxy t)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Proxy t -> m (Proxy t)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Proxy t -> m (Proxy t)

Ord (Proxy s)

Since: base-4.7.0.0

Defined in Data.Proxy

Methods

compare :: Proxy s -> Proxy s -> Ordering

(<) :: Proxy s -> Proxy s -> Bool

(<=) :: Proxy s -> Proxy s -> Bool

(>) :: Proxy s -> Proxy s -> Bool

(>=) :: Proxy s -> Proxy s -> Bool

max :: Proxy s -> Proxy s -> Proxy s

min :: Proxy s -> Proxy s -> Proxy s

Read (Proxy t)

Since: base-4.7.0.0

Defined in Data.Proxy

Methods

readsPrec :: Int -> ReadS (Proxy t)

readList :: ReadS [Proxy t]

readPrec :: ReadPrec (Proxy t)

readListPrec :: ReadPrec [Proxy t]

Show (Proxy s)

Since: base-4.7.0.0

Defined in Data.Proxy

Methods

showsPrec :: Int -> Proxy s -> ShowS

show :: Proxy s -> String

showList :: [Proxy s] -> ShowS

Ix (Proxy s)

Since: base-4.7.0.0

Defined in Data.Proxy

Methods

range :: (Proxy s, Proxy s) -> [Proxy s]

index :: (Proxy s, Proxy s) -> Proxy s -> Int

unsafeIndex :: (Proxy s, Proxy s) -> Proxy s -> Int

inRange :: (Proxy s, Proxy s) -> Proxy s -> Bool

rangeSize :: (Proxy s, Proxy s) -> Int

unsafeRangeSize :: (Proxy s, Proxy s) -> Int

Generic (Proxy t)

Defined in GHC.Generics

Associated Types

type Rep (Proxy t) :: Type -> Type

Methods

from :: Proxy t -> Rep (Proxy t) x

to :: Rep (Proxy t) x -> Proxy t

Semigroup (Proxy s)

Since: base-4.9.0.0

Defined in Data.Proxy

Methods

(<>) :: Proxy s -> Proxy s -> Proxy s

sconcat :: NonEmpty (Proxy s) -> Proxy s

stimes :: Integral b => b -> Proxy s -> Proxy s

Monoid (Proxy s)

Since: base-4.7.0.0

Defined in Data.Proxy

Methods

mempty :: Proxy s

mappend :: Proxy s -> Proxy s -> Proxy s

mconcat :: [Proxy s] -> Proxy s

type Rep1 (Proxy :: k -> Type)

Since: base-4.6.0.0

Defined in GHC.Generics

type Rep1 (Proxy :: k -> Type) = D1 (MetaData "Proxy" "Data.Proxy" "base" False) (C1 (MetaCons "Proxy" PrefixI False) (U1 :: k -> Type))

type Rep (Proxy t)

Since: base-4.6.0.0

Defined in GHC.Generics

type Rep (Proxy t) = D1 (MetaData "Proxy" "Data.Proxy" "base" False) (C1 (MetaCons "Proxy" PrefixI False) (U1 :: Type -> Type))

cong :: forall f a b. Proxy f -> (a :=: b) -> f a :=: f b

cong' :: (pxy m -> pxy (f m)) -> (a :=: b) -> f a :=: f b

class Proposition (f :: k -> *) where

Associated Types

type OriginalProp (f :: k -> *) (n :: k) :: *

Methods

unWrap :: f n -> OriginalProp f n

wrap :: OriginalProp f n -> f n

data HVec (xs :: [*]) where

Constructors

HNil :: HVec '[]

(:-) :: x -> HVec xs -> HVec (x ': xs) infixr 9

class FromBool (c :: *) where

Associated Types

type Predicate c :: Bool

type Args c :: [*]

Methods

fromBool :: Predicate c ~ True => HVec (Args c) -> c

applyNAry :: forall ts c. KnownTypeList ts => (HVec ts -> c) -> ts :~> c

applyNAry' :: KnownTypeList ts => proxy ts -> proxy' c -> (HVec ts -> c) -> ts :~> c

fromBool' :: forall proxy c. (KnownTypeList (Args c), FromBool c, Predicate c ~ True) => proxy c -> Args c :~> c

Conversion between equalities

fromRefl :: Preorder eq => (a :=: b) -> eq a b

fromLeibniz :: Preorder eq => Leibniz a b -> eq a b

reflToLeibniz :: (a :=: b) -> Leibniz a b

leibnizToRefl :: Leibniz a b -> a :=: b

Coercion

coerce :: (a :=: b) -> f a -> f b

Type coercion. coerce is using unsafeCoerce a. So, please, please do not provide the undefined as the proof. Using this function instead of pattern-matching on equality proof, you can reduce the overhead introduced by run-time proof.

coerce' :: (a :=: b) -> a -> b

Coercion for identity types.

withRefl :: forall a b r. (a :~: b) -> (a ~ b => r) -> r

Solves equality constraint without explicit coercion. It has the same effect as gcastWith, but some hacks is done to reduce runtime overhead.

Re-exported modules

module Data.Proxy