| Copyright | (c) Galois Inc 2014-2019 |
|---|---|
| Maintainer | Joe Hendrix <jhendrix@galois.com> |
| Safe Haskell | Safe |
| Language | Haskell98 |
Data.Parameterized.Classes
Contents
Description
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 :: f a -> f b -> Maybe (a :~: b)
- data (a :: k) :~: (b :: k) :: forall k. k -> k -> Type where
- class EqF (f :: k -> *) where
- class PolyEq u v where
- class TestEquality ktp => OrdF (ktp :: k -> *) where
- lexCompareF :: forall (f :: j -> *) (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 (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 (f :: k -> *) (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 -> *) where
- showsF :: ShowF f => f tp -> String -> String
- class HashableF (f :: k -> *) where
- hashWithSaltF :: Int -> f tp -> Int
- hashF :: f tp -> Int
- class CoercibleF (rtp :: k -> *) where
- coerceF :: rtp a -> rtp b
- type family IndexF (m :: *) :: k -> *
- type family IxValueF (m :: *) :: k -> *
- 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 -> *) (ctx :: k) where
- knownRepr :: f ctx
- 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.
Instances
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
| 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 Methods succ :: (a :~: b) -> a :~: b # pred :: (a :~: b) -> 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 |
| (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 | |
| 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 | |
class EqF (f :: k -> *) 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.
Minimal complete definition
Instances
| PolyEq (NatRepr m) (NatRepr n) Source # | |
| PolyEq (BoolRepr m) (BoolRepr n) Source # | |
| PolyEq (PeanoRepr m) (PeanoRepr n) Source # | |
| TestEquality f => PolyEq (Assignment f x) (Assignment f y) Source # | |
Defined in Data.Parameterized.Context.Safe Methods polyEqF :: Assignment f x -> Assignment f y -> Maybe (Assignment f x :~: Assignment f y) Source # polyEq :: Assignment f x -> Assignment f y -> Bool Source # | |
Ordering generalization
class TestEquality ktp => OrdF (ktp :: k -> *) where Source #
A parameterized type that can be compared on distinct instances.
Minimal complete definition
Methods
compareF :: ktp x -> ktp y -> OrderingF x y Source #
compareF compares two keys with different type parameters. Instances must ensure that keys are only equal if the type parameters are equal.
leqF :: ktp x -> ktp y -> Bool Source #
ltF :: ktp x -> ktp y -> Bool Source #
Instances
lexCompareF :: forall (f :: j -> *) (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 (a :: j) (b :: j) (c :: k) (d :: k). OrderingF a b -> (a ~ b => OrderingF c d) -> OrderingF c d Source #
ordFCompose :: forall (f :: k -> *) (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 -> *) where Source #
A parameterized type that can be shown on all instances.
To implement ShowF gShow
(g tp)tp, then write an empty instance
instance .ShowF g
Minimal complete definition
Nothing
Methods
withShow :: p f -> q tp -> (Show (f tp) => a) -> a Source #
Provides a show instance for each type.
withShow :: Show (f tp) => 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 -> *) where Source #
A parameterized type that is hashable on all instances.
Minimal complete definition
Instances
| HashableF BoolRepr Source # | |
| HashableF NatRepr Source # | |
| HashableF SymbolRepr Source # | |
Defined in Data.Parameterized.SymbolRepr | |
| 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 (Index ctx :: k -> Type) Source # | |
| HashableF f => HashableF (Assignment f :: Ctx k -> Type) Source # | |
Defined in Data.Parameterized.Context.Unsafe Methods hashWithSaltF :: Int -> Assignment f tp -> Int Source # hashF :: Assignment f tp -> Int Source # | |
| HashableF f => HashableF (Assignment f :: Ctx k -> Type) Source # | |
Defined in Data.Parameterized.Context.Safe Methods hashWithSaltF :: Int -> Assignment f tp -> Int Source # hashF :: Assignment f tp -> Int Source # | |
class CoercibleF (rtp :: k -> *) 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.
Optics generalizations
type family IndexF (m :: *) :: k -> * Source #
Instances
| type IndexF (Assignment f ctx) Source # | |
Defined in Data.Parameterized.Context.Unsafe | |
| type IndexF (Assignment f ctx) Source # | |
Defined in Data.Parameterized.Context.Safe | |
| type IndexF (MapF k2 v) Source # | |
Defined in Data.Parameterized.Map | |
type family IxValueF (m :: *) :: k -> * Source #
Instances
| type IxValueF (Assignment f ctx) Source # | |
Defined in Data.Parameterized.Context.Unsafe | |
| type IxValueF (Assignment f ctx) Source # | |
Defined in Data.Parameterized.Context.Safe | |
| type IxValueF (MapF k2 v) Source # | |
Defined in Data.Parameterized.Map | |
class IxedF k m where Source #
Parameterized generalization of the lens Ixed class.
Methods
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 Methods ixF :: IndexF (Assignment f ctx) x -> Traversal' (Assignment f ctx) (IxValueF (Assignment f ctx) x) Source # | |
| IxedF k (Assignment f ctx) Source # | |
Defined in Data.Parameterized.Context.Safe Methods ixF :: 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.
Methods
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 Methods ixF' :: IndexF (Assignment f ctx) x -> Lens' (Assignment f ctx) (IxValueF (Assignment f ctx) x) Source # | |
| IxedF' k (Assignment f ctx) Source # | |
Defined in Data.Parameterized.Context.Safe Methods ixF' :: 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.
Methods
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 -> *) (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.