Safe Haskell | None |
---|---|
Language | Haskell98 |
- data (k :~: a) b :: forall k. k -> k -> * where
- type (:=:) = (:~:)
- sym :: (:~:) k a b -> (:~:) k b a
- trans :: (:~:) k a b -> (:~:) k b c -> (:~:) k a c
- class Preorder eq => Equality eq where
- class Preorder eq where
- reflexivity' :: (SingI x, 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 -> Sing y -> r x y
- data Leibniz a b = Leibniz {
- apply :: forall f. f a -> f b
- data Reason eq x y where
- because :: Sing y -> eq x y -> Reason eq x y
- by :: Sing y -> eq x y -> Reason eq x y
- (===) :: Equality eq => eq x y -> Reason eq y z -> eq x z
- start :: Preorder eq => Sing a -> eq a a
- byDefinition :: (SingI a, Preorder eq) => eq a a
- admitted :: Reason eq x y
- data Proxy k t :: forall k. k -> * = Proxy
- cong :: forall f a b. Proxy f -> (a :=: b) -> f a :=: f b
- cong' :: (Sing m -> Sing (f m)) -> (a :=: b) -> f a :=: f b
- class Proposition f where
- type OriginalProp (f :: k -> *) (n :: k) :: *
- 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, SingI b) => (a :=: b) -> eq a b
- fromLeibniz :: (Preorder eq, SingI a) => 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.Singletons
- module Data.Proxy
Documentation
data (k :~: a) b :: forall k. k -> k -> * 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: 4.7.0.0
Equality k ((:=:) k) Source # | |
Preorder k ((:=:) k) Source # | |
TestCoercion k ((:~:) k a) | |
TestEquality k ((:~:) k a) | |
(~) k a b => Bounded ((:~:) k a b) | |
(~) k a b => Enum ((:~:) k a b) | |
Eq ((:~:) k a b) | |
((~) * a b, Data a) => Data ((:~:) * a b) | |
Ord ((:~:) k a b) | |
(~) k a b => Read ((:~:) k a b) | |
Show ((:~:) k a b) | |
class Preorder eq where Source #
reflexivity :: Sing a -> eq a a Source #
transitivity :: eq a b -> eq b c -> eq a c Source #
reflexivity' :: (SingI x, Preorder r) => r x x Source #
byDefinition :: (SingI a, Preorder eq) => eq a a Source #
data Proxy k t :: forall k. k -> * #
A concrete, poly-kinded proxy type
Monad (Proxy *) | |
Functor (Proxy *) | |
Applicative (Proxy *) | |
Foldable (Proxy *) | |
Traversable (Proxy *) | |
Generic1 (Proxy *) | |
Eq1 (Proxy *) | Since: 4.9.0.0 |
Ord1 (Proxy *) | Since: 4.9.0.0 |
Read1 (Proxy *) | Since: 4.9.0.0 |
Show1 (Proxy *) | Since: 4.9.0.0 |
Alternative (Proxy *) | |
MonadPlus (Proxy *) | |
Bounded (Proxy k s) | |
Enum (Proxy k s) | |
Eq (Proxy k s) | |
Data t => Data (Proxy * t) | |
Ord (Proxy k s) | |
Read (Proxy k s) | |
Show (Proxy k s) | |
Ix (Proxy k s) | |
Generic (Proxy k t) | |
Semigroup (Proxy k s) | |
Monoid (Proxy k s) | |
type Rep1 (Proxy *) | |
type Rep (Proxy k t) | |
class Proposition f 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
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.Singletons
module Data.Proxy