Safe Haskell | None |
---|---|
Language | Haskell98 |
- data a :=: b where
- class Preorder eq => Equality eq where
- symmetry :: eq a b -> eq b a
- class Preorder eq where
- reflexivity :: Sing a -> eq a a
- transitivity :: eq a b -> eq b c -> eq a c
- 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
- (=~=) :: Preorder r => 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 t :: 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 n :: *
- unWrap :: f n -> OriginalProp f n
- wrap :: OriginalProp f n -> f n
- type family xs :~> a :: *
- class FromBool c where
- 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
- module Data.Singletons
- module Data.Proxy
Documentation
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 t :: k -> *
A concrete, poly-kinded proxy type
class Proposition f where Source
type OriginalProp f n :: * Source
unWrap :: f n -> OriginalProp f n Source
wrap :: OriginalProp f n -> f n Source
Conversion between equalities
fromLeibniz :: (Preorder eq, SingI a) => 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.
Re-exported modules
module Data.Singletons
module Data.Proxy