Copyright | (c) Galois Inc 2014-2019 |
---|---|
Maintainer | Joe Hendrix <jhendrix@galois.com> |
Safe Haskell | Safe |
Language | Haskell2010 |
This module declares classes for working with types with the kind
k -> *
for any kind k
. These are generalizations of the
Data.Functor.Classes types as they work with any kind k
, and are
not restricted to *
.
Synopsis
- class TestEquality (f :: k -> Type) where
- testEquality :: forall (a :: k) (b :: k). f a -> f b -> Maybe (a :~: b)
- data (a :: k) :~: (b :: k) where
- class EqF (f :: k -> Type) where
- class PolyEq u v where
- class TestEquality ktp => OrdF (ktp :: k -> Type) where
- lexCompareF :: forall j k (f :: j -> Type) (a :: j) (b :: j) (c :: k) (d :: k). OrdF f => f a -> f b -> (a ~ b => OrderingF c d) -> OrderingF c d
- data OrderingF x y where
- joinOrderingF :: forall j k (a :: j) (b :: j) (c :: k) (d :: k). OrderingF a b -> (a ~ b => OrderingF c d) -> OrderingF c d
- orderingF_refl :: OrderingF x y -> Maybe (x :~: y)
- toOrdering :: OrderingF x y -> Ordering
- fromOrdering :: Ordering -> OrderingF x x
- ordFCompose :: forall k l (f :: k -> Type) (g :: l -> k) x y. (forall w z. f w -> f z -> OrderingF w z) -> Compose f g x -> Compose f g y -> OrderingF x y
- class ShowF (f :: k -> Type) where
- showsF :: ShowF f => f tp -> String -> String
- class HashableF (f :: k -> Type) where
- hashWithSaltF :: Int -> f tp -> Int
- hashF :: f tp -> Int
- class CoercibleF (rtp :: k -> Type) where
- coerceF :: rtp a -> rtp b
- newtype TypeAp (f :: k -> Type) (tp :: k) = TypeAp (f tp)
- type family IndexF (m :: Type) :: k -> Type
- type family IxValueF (m :: Type) :: k -> Type
- class IxedF k m where
- class IxedF k m => IxedF' k m where
- class IxedF k m => AtF k m where
- class KnownRepr (f :: k -> Type) (ctx :: k) where
- knownRepr :: f ctx
- class Hashable a where
- hashWithSalt :: Int -> a -> Int
- hash :: a -> Int
- isJust :: Maybe a -> Bool
Equality exports
class TestEquality (f :: k -> Type) where #
This class contains types where you can learn the equality of two types from information contained in terms. Typically, only singleton types should inhabit this class.
testEquality :: forall (a :: k) (b :: k). f a -> f b -> Maybe (a :~: b) #
Conditionally prove the equality of a
and b
.
Instances
data (a :: k) :~: (b :: 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: base-4.7.0.0
Instances
Category ((:~:) :: k -> k -> Type) | Since: base-4.7.0.0 |
TestEquality ((:~:) a :: k -> Type) | Since: base-4.7.0.0 |
Defined in Data.Type.Equality | |
NFData2 ((:~:) :: Type -> Type -> Type) | Since: deepseq-1.4.3.0 |
Defined in Control.DeepSeq | |
NFData1 ((:~:) a) | Since: deepseq-1.4.3.0 |
Defined in Control.DeepSeq | |
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 :: forall r r'. (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 |
NFData (a :~: b) | Since: deepseq-1.4.3.0 |
Defined in Control.DeepSeq | |
HasDict (a ~ b) (a :~: b) | |
Defined in Data.Constraint |
class EqF (f :: k -> Type) where Source #
EqF
provides a method eqF
for testing whether two parameterized
types are equal.
Unlike TestEquality
, this only works when the type arguments are
the same, and does not provide a proof that the types have the same
type when they are equal. Thus this can be implemented over
parameterized types that are unable to provide evidence that their
type arguments are equal.
class PolyEq u v where Source #
A polymorphic equality operator that generalizes TestEquality
.
Ordering generalization
class TestEquality ktp => OrdF (ktp :: k -> Type) where Source #
The OrdF
class is a total ordering over parameterized types so
that types with different parameters can be compared.
Instances of OrdF
are expected to satisfy the following laws:
- Transitivity
- if
leqF x y && leqF y z
=True
, thenleqF x = z
=True
- Reflexivity
leqF x x
=True
- Antisymmetry
- if
leqF x y && leqF y x
=True
, thentestEquality x y
=Just Refl
Note that the following operator interactions are expected to hold:
geqF x y
iffleqF y x
ltF x y
iffleqF x y && testEquality x y = Nothing
gtF x y
iffltF y x
ltF x y
iffcompareF x y == LTF
gtF x y
iffcompareF x y == GTF
isJust (testEquality x y)
iffcompareF x y == EQF
Furthermore, when x
and y
both have type (k tp)
, we expect:
compareF x y == EQF
equalscompare x y
whenOrd (k tp)
has an instance.isJust (testEquality x y)
equalsx == y
whenEq (k tp)
has an instance.
Minimal complete definition: either compareF
or leqF
.
Using compareF
can be more efficient for complex types.
compareF :: ktp x -> ktp y -> OrderingF x y Source #
leqF :: ktp x -> ktp y -> Bool Source #
ltF :: ktp x -> ktp y -> Bool Source #
Instances
OrdF BoolRepr Source # | |
Defined in Data.Parameterized.BoolRepr compareF :: forall (x :: k) (y :: k). BoolRepr x -> BoolRepr y -> OrderingF x y Source # leqF :: forall (x :: k) (y :: k). BoolRepr x -> BoolRepr y -> Bool Source # ltF :: forall (x :: k) (y :: k). BoolRepr x -> BoolRepr y -> Bool Source # geqF :: forall (x :: k) (y :: k). BoolRepr x -> BoolRepr y -> Bool Source # gtF :: forall (x :: k) (y :: k). BoolRepr x -> BoolRepr y -> Bool Source # | |
OrdF NatRepr Source # | |
Defined in Data.Parameterized.NatRepr.Internal compareF :: forall (x :: k) (y :: k). NatRepr x -> NatRepr y -> OrderingF x y Source # leqF :: forall (x :: k) (y :: k). NatRepr x -> NatRepr y -> Bool Source # ltF :: forall (x :: k) (y :: k). NatRepr x -> NatRepr y -> Bool Source # geqF :: forall (x :: k) (y :: k). NatRepr x -> NatRepr y -> Bool Source # gtF :: forall (x :: k) (y :: k). NatRepr x -> NatRepr y -> Bool Source # | |
OrdF SymbolRepr Source # | |
Defined in Data.Parameterized.SymbolRepr compareF :: forall (x :: k) (y :: k). SymbolRepr x -> SymbolRepr y -> OrderingF x y Source # leqF :: forall (x :: k) (y :: k). SymbolRepr x -> SymbolRepr y -> Bool Source # ltF :: forall (x :: k) (y :: k). SymbolRepr x -> SymbolRepr y -> Bool Source # geqF :: forall (x :: k) (y :: k). SymbolRepr x -> SymbolRepr y -> Bool Source # gtF :: forall (x :: k) (y :: k). SymbolRepr x -> SymbolRepr y -> Bool Source # | |
OrdF PeanoRepr Source # | |
Defined in Data.Parameterized.Peano compareF :: forall (x :: k) (y :: k). PeanoRepr x -> PeanoRepr y -> OrderingF x y Source # leqF :: forall (x :: k) (y :: k). PeanoRepr x -> PeanoRepr y -> Bool Source # ltF :: forall (x :: k) (y :: k). PeanoRepr x -> PeanoRepr y -> Bool Source # geqF :: forall (x :: k) (y :: k). PeanoRepr x -> PeanoRepr y -> Bool Source # gtF :: forall (x :: k) (y :: k). PeanoRepr x -> PeanoRepr y -> Bool Source # | |
OrdF (Nonce :: k -> Type) Source # | |
Defined in Data.Parameterized.Nonce.Unsafe compareF :: forall (x :: k0) (y :: k0). Nonce x -> Nonce y -> OrderingF x y Source # leqF :: forall (x :: k0) (y :: k0). Nonce x -> Nonce y -> Bool Source # ltF :: forall (x :: k0) (y :: k0). Nonce x -> Nonce y -> Bool Source # geqF :: forall (x :: k0) (y :: k0). Nonce x -> Nonce y -> Bool Source # gtF :: forall (x :: k0) (y :: k0). Nonce x -> Nonce y -> Bool Source # | |
OrdF (Nonce s :: k -> Type) Source # | |
Defined in Data.Parameterized.Nonce compareF :: forall (x :: k0) (y :: k0). Nonce s x -> Nonce s y -> OrderingF x y Source # leqF :: forall (x :: k0) (y :: k0). Nonce s x -> Nonce s y -> Bool Source # ltF :: forall (x :: k0) (y :: k0). Nonce s x -> Nonce s y -> Bool Source # geqF :: forall (x :: k0) (y :: k0). Nonce s x -> Nonce s y -> Bool Source # gtF :: forall (x :: k0) (y :: k0). Nonce s x -> Nonce s y -> Bool Source # | |
OrdF (Index l :: k -> Type) Source # | |
Defined in Data.Parameterized.List compareF :: forall (x :: k0) (y :: k0). Index l x -> Index l y -> OrderingF x y Source # leqF :: forall (x :: k0) (y :: k0). Index l x -> Index l y -> Bool Source # ltF :: forall (x :: k0) (y :: k0). Index l x -> Index l y -> Bool Source # geqF :: forall (x :: k0) (y :: k0). Index l x -> Index l y -> Bool Source # gtF :: forall (x :: k0) (y :: k0). Index l x -> Index l y -> Bool Source # | |
OrdF (Index ctx :: k -> Type) Source # | |
Defined in Data.Parameterized.Context.Unsafe compareF :: forall (x :: k0) (y :: k0). Index ctx x -> Index ctx y -> OrderingF x y Source # leqF :: forall (x :: k0) (y :: k0). Index ctx x -> Index ctx y -> Bool Source # ltF :: forall (x :: k0) (y :: k0). Index ctx x -> Index ctx y -> Bool Source # geqF :: forall (x :: k0) (y :: k0). Index ctx x -> Index ctx y -> Bool Source # gtF :: forall (x :: k0) (y :: k0). Index ctx x -> Index ctx y -> Bool Source # | |
OrdF f => OrdF (Compose f g :: k2 -> Type) Source # | |
Defined in Data.Parameterized.Classes compareF :: forall (x :: k) (y :: k). Compose f g x -> Compose f g y -> OrderingF x y Source # leqF :: forall (x :: k) (y :: k). Compose f g x -> Compose f g y -> Bool Source # ltF :: forall (x :: k) (y :: k). Compose f g x -> Compose f g y -> Bool Source # geqF :: forall (x :: k) (y :: k). Compose f g x -> Compose f g y -> Bool Source # gtF :: forall (x :: k) (y :: k). Compose f g x -> Compose f g y -> Bool Source # | |
OrdF f => OrdF (List f :: [k] -> Type) Source # | |
Defined in Data.Parameterized.List compareF :: forall (x :: k0) (y :: k0). List f x -> List f y -> OrderingF x y Source # leqF :: forall (x :: k0) (y :: k0). List f x -> List f y -> Bool Source # ltF :: forall (x :: k0) (y :: k0). List f x -> List f y -> Bool Source # geqF :: forall (x :: k0) (y :: k0). List f x -> List f y -> Bool Source # gtF :: forall (x :: k0) (y :: k0). List f x -> List f y -> Bool Source # | |
OrdF f => OrdF (Assignment f :: Ctx k -> Type) Source # | |
Defined in Data.Parameterized.Context.Unsafe compareF :: forall (x :: k0) (y :: k0). Assignment f x -> Assignment f y -> OrderingF x y Source # leqF :: forall (x :: k0) (y :: k0). Assignment f x -> Assignment f y -> Bool Source # ltF :: forall (x :: k0) (y :: k0). Assignment f x -> Assignment f y -> Bool Source # geqF :: forall (x :: k0) (y :: k0). Assignment f x -> Assignment f y -> Bool Source # gtF :: forall (x :: k0) (y :: k0). Assignment f x -> Assignment f y -> Bool Source # | |
(OrdF f, OrdF g) => OrdF (PairRepr f g :: (k1, k2) -> Type) Source # | |
Defined in Data.Parameterized.DataKind compareF :: forall (x :: k) (y :: k). PairRepr f g x -> PairRepr f g y -> OrderingF x y Source # leqF :: forall (x :: k) (y :: k). PairRepr f g x -> PairRepr f g y -> Bool Source # ltF :: forall (x :: k) (y :: k). PairRepr f g x -> PairRepr f g y -> Bool Source # geqF :: forall (x :: k) (y :: k). PairRepr f g x -> PairRepr f g y -> Bool Source # gtF :: forall (x :: k) (y :: k). PairRepr f g x -> PairRepr f g y -> Bool Source # |
lexCompareF :: forall j k (f :: j -> Type) (a :: j) (b :: j) (c :: k) (d :: k). OrdF f => f a -> f b -> (a ~ b => OrderingF c d) -> OrderingF c d Source #
Compare two values, and if they are equal compare the next values, otherwise return LTF or GTF
joinOrderingF :: forall j k (a :: j) (b :: j) (c :: k) (d :: k). OrderingF a b -> (a ~ b => OrderingF c d) -> OrderingF c d Source #
ordFCompose :: forall k l (f :: k -> Type) (g :: l -> k) x y. (forall w z. f w -> f z -> OrderingF w z) -> Compose f g x -> Compose f g y -> OrderingF x y Source #
If the "outer" functor has an OrdF
instance, then one can be generated
for the "inner" functor. The type-level evidence of equality is deduced
via generativity of g
, e.g. the inference g x ~ g y
implies x ~ y
.
Typeclass generalizations
class ShowF (f :: k -> Type) where Source #
A parameterized type that can be shown on all instances.
To implement
, one should implement an instance ShowF
g
for all argument types Show
(g tp)tp
, then write an empty instance
instance
.ShowF
g
Nothing
withShow :: p f -> q tp -> (Show (f tp) => a) -> a Source #
Provides a show instance for each type.
showF :: forall tp. f tp -> String Source #
showsPrecF :: forall tp. Int -> f tp -> String -> String Source #
Like showsPrec
, the precedence argument is one more than the
precedence of the enclosing context.
Instances
class HashableF (f :: k -> Type) where Source #
A parameterized type that is hashable on all instances.
Instances
HashableF BoolRepr Source # | |
HashableF NatRepr Source # | |
HashableF SymbolRepr Source # | |
Defined in Data.Parameterized.SymbolRepr hashWithSaltF :: forall (tp :: k). Int -> SymbolRepr tp -> Int Source # hashF :: forall (tp :: k). SymbolRepr tp -> Int Source # | |
HashableF PeanoRepr Source # | |
HashableF (Nonce :: k -> Type) Source # | |
Hashable a => HashableF (Const a :: k -> Type) Source # | |
HashableF (Nonce s :: k -> Type) Source # | |
HashableF (Index ctx :: k -> Type) Source # | |
HashableF f => HashableF (Assignment f :: Ctx k -> Type) Source # | |
Defined in Data.Parameterized.Context.Unsafe hashWithSaltF :: forall (tp :: k0). Int -> Assignment f tp -> Int Source # hashF :: forall (tp :: k0). Assignment f tp -> Int Source # |
class CoercibleF (rtp :: k -> Type) where Source #
An instance of CoercibleF
gives a way to coerce between
all the types of a family. We generally use this to witness
the fact that the type parameter to rtp
is a phantom type
by giving an implementation in terms of Data.Coerce.coerce.
Type function application constructor
newtype TypeAp (f :: k -> Type) (tp :: k) Source #
Captures the value obtained from applying a type to a function so that we can use parameterized class instance to provide unparameterized instances for specific types.
This is the same as Ap
from Control.Applicative
, but we introduce
our own new type to avoid orphan instances.
TypeAp (f tp) |
Instances
TestEquality f => Eq (TypeAp f tp) Source # | |
OrdF f => Ord (TypeAp f tp) Source # | |
Defined in Data.Parameterized.Classes | |
ShowF f => Show (TypeAp f tp) Source # | |
HashableF f => Hashable (TypeAp f tp) Source # | |
Defined in Data.Parameterized.Classes |
Optics generalizations
type family IndexF (m :: Type) :: k -> Type Source #
Instances
type IndexF (Assignment f ctx) Source # | |
Defined in Data.Parameterized.Context.Unsafe | |
type IndexF (MapF k2 v) Source # | |
Defined in Data.Parameterized.Map |
type family IxValueF (m :: Type) :: k -> Type Source #
Instances
type IxValueF (Assignment f ctx) Source # | |
Defined in Data.Parameterized.Context.Unsafe | |
type IxValueF (MapF k2 v) Source # | |
Defined in Data.Parameterized.Map |
class IxedF k m where Source #
Parameterized generalization of the lens Ixed
class.
ixF :: forall (x :: k). IndexF m x -> Traversal' m (IxValueF m x) Source #
Given an index into a container, build a traversal that visits the given element in the container, if it exists.
Instances
IxedF k (Assignment f ctx) Source # | |
Defined in Data.Parameterized.Context.Unsafe ixF :: forall (x :: k). IndexF (Assignment f ctx) x -> Traversal' (Assignment f ctx) (IxValueF (Assignment f ctx) x) Source # | |
OrdF k => IxedF a (MapF k v) Source # | Turn a map key into a traversal that visits the indicated element in the map, if it exists. |
class IxedF k m => IxedF' k m where Source #
Parameterized generalization of the lens Ixed
class,
but with the guarantee that indexes exist in the container.
ixF' :: forall (x :: k). IndexF m x -> Lens' m (IxValueF m x) Source #
Given an index into a container, build a lens that points into the given element in the container.
Instances
IxedF' k (Assignment f ctx) Source # | |
Defined in Data.Parameterized.Context.Unsafe ixF' :: forall (x :: k). IndexF (Assignment f ctx) x -> Lens' (Assignment f ctx) (IxValueF (Assignment f ctx) x) Source # |
class IxedF k m => AtF k m where Source #
Parameterized generalization of the lens At
class.
atF :: forall (x :: k). IndexF m x -> Lens' m (Maybe (IxValueF m x)) Source #
Given an index into a container, build a lens that points into
the given position in the container, whether or not it currently
exists. Setting values of atF
to a Just
value will insert
the value if it does not already exist.
KnownRepr
class KnownRepr (f :: k -> Type) (ctx :: k) where Source #
This class is parameterized by a kind k
(typically a data
kind), a type constructor f
of kind k -> *
(typically a GADT of
singleton types indexed by k
), and an index parameter ctx
of
kind k
.
Instances
Re-exports
The class of types that can be converted to a hash value.
Minimal implementation: hashWithSalt
.
Nothing
hashWithSalt :: Int -> a -> Int infixl 0 #
Return a hash value for the argument, using the given salt.
The general contract of hashWithSalt
is:
- If two values are equal according to the
==
method, then applying thehashWithSalt
method on each of the two values must produce the same integer result if the same salt is used in each case. - It is not required that if two values are unequal
according to the
==
method, then applying thehashWithSalt
method on each of the two values must produce distinct integer results. However, the programmer should be aware that producing distinct integer results for unequal values may improve the performance of hashing-based data structures. - This method can be used to compute different hash values for
the same input by providing a different salt in each
application of the method. This implies that any instance
that defines
hashWithSalt
must make use of the salt in its implementation.
Like hashWithSalt
, but no salt is used. The default
implementation uses hashWithSalt
with some default salt.
Instances might want to implement this method to provide a more
efficient implementation than the default implementation.