Safe Haskell | None |
---|---|
Language | Haskell2010 |
Synopsis
- data (a :: k) :~: (b :: k) :: forall k. k -> k -> Type where
- type (:=:) = (:~:)
- sym :: (a :~: b) -> b :~: a
- trans :: (a :~: b) -> (b :~: c) -> a :~: c
- class Preorder eq => Equality (eq :: k -> k -> *) where
- symmetry :: eq a b -> eq b a
- class Preorder (eq :: k -> k -> *) where
- reflexivity :: proxy a -> eq a a
- transitivity :: eq a b -> eq b c -> eq a c
- reflexivity' :: Preorder r => r x x
- type (:\/:) a b = Either a b
- type (:/\:) a b = (a, b)
- (=<=) :: Preorder r => r x y -> Reason r y z -> r x z
- (=>=) :: Preorder r => r y z -> Reason r x y -> r x z
- (=~=) :: r x y -> proxy y -> r x y
- data Leibniz a b = Leibniz {
- apply :: forall f. f a -> f b
- data Reason eq x y where
- because :: proxy y -> eq x y -> Reason eq x y
- by :: proxy y -> eq x y -> Reason eq x y
- (===) :: Equality eq => eq x y -> Reason eq y z -> eq x z
- start :: Preorder eq => proxy a -> eq a a
- byDefinition :: Preorder eq => eq a a
- admitted :: Reason eq x y
- data Proxy (t :: k) :: forall k. k -> Type = Proxy
- 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
- type OriginalProp (f :: k -> *) (n :: k) :: *
- unWrap :: f n -> OriginalProp f n
- wrap :: OriginalProp f n -> f n
- data HVec (xs :: [*]) where
- class FromBool (c :: *) where
- 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
- 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
- coerce :: (a :=: b) -> f a -> f b
- coerce' :: (a :=: b) -> a -> b
- withRefl :: forall a b r. (a :~: b) -> (a ~ b => r) -> r
- module Data.Proxy
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
Instances
Equality ((:=:) :: k -> k -> Type) Source # | |
Preorder ((:=:) :: k -> k -> Type) Source # | |
Defined in Proof.Equational reflexivity :: proxy a -> a :=: a Source # | |
TestEquality ((:~:) a :: k -> Type) | Since: base-4.7.0.0 |
Defined in Data.Type.Equality | |
a ~ b => Bounded (a :~: b) | Since: base-4.7.0.0 |
a ~ b => Enum (a :~: b) | Since: base-4.7.0.0 |
Defined in Data.Type.Equality | |
Eq (a :~: b) | Since: base-4.7.0.0 |
(a ~ b, Data a) => Data (a :~: b) | Since: base-4.7.0.0 |
Defined in Data.Data 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 | |
a ~ b => Read (a :~: b) | Since: base-4.7.0.0 |
Show (a :~: b) | Since: base-4.7.0.0 |
Empty (False :~: True) Source # | |
Empty (True :~: False) Source # | |
Empty (LT :~: EQ) Source # | |
Empty (LT :~: GT) Source # | |
Empty (EQ :~: LT) Source # | |
Empty (EQ :~: GT) Source # | |
Empty (GT :~: LT) Source # | |
Empty (GT :~: EQ) Source # | |
Empty (() :~: Int) Source # | |
Empty (0 :~: 1) Source # | |
Defined in Proof.Propositional | |
Inhabited (n :~: n) Source # | |
Defined in Proof.Propositional |
class Preorder (eq :: k -> k -> *) where Source #
reflexivity :: proxy a -> eq a a Source #
transitivity :: eq a b -> eq b c -> eq a c Source #
Instances
Preorder (Leibniz :: k -> k -> Type) Source # | |
Defined in Proof.Equational reflexivity :: proxy a -> Leibniz a a Source # transitivity :: Leibniz a b -> Leibniz b c -> Leibniz a c Source # | |
Preorder ((:=:) :: k -> k -> Type) Source # | |
Defined in Proof.Equational reflexivity :: proxy a -> a :=: a Source # | |
Preorder ((->) :: Type -> Type -> Type) Source # | |
Defined in Proof.Equational reflexivity :: proxy a -> a -> a Source # transitivity :: (a -> b) -> (b -> c) -> a -> c Source # |
reflexivity' :: Preorder r => r x x Source #
byDefinition :: Preorder eq => eq a a Source #
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,
is a safer alternative to the
Proxy
:: Proxy
a'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
Instances
Generic1 (Proxy :: k -> Type) | |
Monad (Proxy :: Type -> Type) | Since: base-4.7.0.0 |
Functor (Proxy :: Type -> Type) | Since: base-4.7.0.0 |
Applicative (Proxy :: Type -> Type) | Since: base-4.7.0.0 |
Foldable (Proxy :: Type -> Type) | Since: base-4.7.0.0 |
Defined in Data.Foldable 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 # elem :: Eq a => a -> Proxy a -> Bool # maximum :: Ord a => Proxy a -> a # minimum :: Ord a => Proxy a -> a # | |
Traversable (Proxy :: Type -> Type) | Since: base-4.7.0.0 |
Alternative (Proxy :: Type -> Type) | Since: base-4.9.0.0 |
MonadPlus (Proxy :: Type -> Type) | Since: base-4.9.0.0 |
Bounded (Proxy t) | Since: base-4.7.0.0 |
Enum (Proxy s) | Since: base-4.7.0.0 |
Eq (Proxy s) | Since: base-4.7.0.0 |
Data t => Data (Proxy t) | Since: base-4.7.0.0 |
Defined in Data.Data 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 |
Read (Proxy t) | Since: base-4.7.0.0 |
Show (Proxy s) | Since: base-4.7.0.0 |
Ix (Proxy s) | Since: base-4.7.0.0 |
Generic (Proxy t) | |
Semigroup (Proxy s) | Since: base-4.9.0.0 |
Monoid (Proxy s) | Since: base-4.7.0.0 |
type Rep1 (Proxy :: k -> Type) | Since: base-4.6.0.0 |
type Rep (Proxy t) | Since: base-4.6.0.0 |
class Proposition (f :: k -> *) where Source #
type OriginalProp (f :: k -> *) (n :: k) :: * Source #
unWrap :: f n -> OriginalProp f n Source #
wrap :: OriginalProp f n -> f n Source #
applyNAry' :: KnownTypeList ts => proxy ts -> proxy' c -> (HVec ts -> c) -> ts :~> c Source #
fromBool' :: forall proxy c. (KnownTypeList (Args c), FromBool c, Predicate c ~ True) => proxy c -> Args c :~> c Source #
Conversion between equalities
fromLeibniz :: Preorder eq => Leibniz a b -> eq a b Source #
reflToLeibniz :: (a :=: b) -> Leibniz a b Source #
leibnizToRefl :: Leibniz a b -> a :=: b Source #
Coercion
coerce :: (a :=: b) -> f a -> f b Source #
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.
withRefl :: forall a b r. (a :~: b) -> (a ~ b => r) -> r Source #
Solves equality constraint without explicit coercion.
It has the same effect as
,
but some hacks is done to reduce runtime overhead.gcastWith
Re-exported modules
module Data.Proxy