Copyright	(c) Galois Inc 2014-2015
Maintainer	Joe Hendrix <jhendrix@galois.com>
Safe Haskell	Safe
Language	Haskell98

Data.Parameterized.Classes

Contents

Equality exports
Ordering generalization
Typeclass generalizations
Optics generalizations
KnownRepr
Re-exports

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

Equality exports

class TestEquality k (f :: k -> *) 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.

Minimal complete definition

testEquality

Methods

testEquality :: f a -> f b -> Maybe ((:~:) k a b) #

Conditionally prove the equality of a and b.

Instances

TestEquality Nat NatRepr #
Methods testEquality :: f a -> f b -> Maybe ((NatRepr :~: a) b) #
TestEquality Symbol SymbolRepr #
Methods testEquality :: f a -> f b -> Maybe ((SymbolRepr :~: a) b) #
TestEquality k (Nonce k) #
Methods testEquality :: f a -> f b -> Maybe ((Nonce k :~: a) b) #
TestEquality k (Nonce k s) #
Methods testEquality :: f a -> f b -> Maybe ((Nonce k s :~: a) b) #
TestEquality k ((:~:) k a)	Since: 4.7.0.0
Methods testEquality :: f a -> f b -> Maybe (((k :~: a) :~: a) b) #
TestEquality k (Index k l) #
Methods testEquality :: f a -> f b -> Maybe ((Index k l :~: a) b) #
TestEquality k (Index k ctx) #
Methods testEquality :: f a -> f b -> Maybe ((Index k ctx :~: a) b) #
TestEquality k (Index k ctx) #
Methods testEquality :: f a -> f b -> Maybe ((Index k ctx :~: a) b) #
TestEquality k ((:~~:) k1 k a)	Since: 4.10.0.0
Methods testEquality :: f a -> f b -> Maybe (((k1 :~~: k) a :~: a) b) #
TestEquality k f => TestEquality [k] (List k f) #
Methods testEquality :: f a -> f b -> Maybe ((List k f :~: a) b) #
TestEquality k f => TestEquality (Ctx k) (Assignment k f) #
Methods testEquality :: f a -> f b -> Maybe ((Assignment k f :~: a) b) #
TestEquality k f => TestEquality (Ctx k) (Assignment k f) #
Methods testEquality :: f a -> f b -> Maybe ((Assignment k f :~: a) b) #

data (k :~: (a :: k)) (b :: k) :: 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

Constructors

Refl :: (:~:) k a a

Instances

Category k ((:~:) k)	Since: 4.7.0.0
Methods id :: cat a a # (.) :: cat b c -> cat a b -> cat a c #
TestEquality k ((:~:) k a)	Since: 4.7.0.0
Methods testEquality :: f a -> f b -> Maybe (((k :~: a) :~: a) b) #
NFData2 ((:~:) *)	Since: 1.4.3.0
Methods liftRnf2 :: (a -> ()) -> (b -> ()) -> (* :~: a) b -> () #
NFData1 ((:~:) * a)	Since: 1.4.3.0
Methods liftRnf :: (a -> ()) -> (* :~: a) a -> () #
(~) k a b => Bounded ((:~:) k a b)	Since: 4.7.0.0
Methods minBound :: (k :~: a) b # maxBound :: (k :~: a) b #
(~) k a b => Enum ((:~:) k a b)	Since: 4.7.0.0
Methods succ :: (k :~: a) b -> (k :~: a) b # pred :: (k :~: a) b -> (k :~: a) b # toEnum :: Int -> (k :~: a) b # fromEnum :: (k :~: a) b -> Int # enumFrom :: (k :~: a) b -> [(k :~: a) b] # enumFromThen :: (k :~: a) b -> (k :~: a) b -> [(k :~: a) b] # enumFromTo :: (k :~: a) b -> (k :~: a) b -> [(k :~: a) b] # enumFromThenTo :: (k :~: a) b -> (k :~: a) b -> (k :~: a) b -> [(k :~: a) b] #
Eq ((:~:) k a b)
Methods (==) :: (k :~: a) b -> (k :~: a) b -> Bool # (/=) :: (k :~: a) b -> (k :~: a) b -> Bool #
Ord ((:~:) k a b)
Methods compare :: (k :~: a) b -> (k :~: a) b -> Ordering # (<) :: (k :~: a) b -> (k :~: a) b -> Bool # (<=) :: (k :~: a) b -> (k :~: a) b -> Bool # (>) :: (k :~: a) b -> (k :~: a) b -> Bool # (>=) :: (k :~: a) b -> (k :~: a) b -> Bool # max :: (k :~: a) b -> (k :~: a) b -> (k :~: a) b # min :: (k :~: a) b -> (k :~: a) b -> (k :~: a) b #
(~) k a b => Read ((:~:) k a b)	Since: 4.7.0.0
Methods readsPrec :: Int -> ReadS ((k :~: a) b) # readList :: ReadS [(k :~: a) b] # readPrec :: ReadPrec ((k :~: a) b) # readListPrec :: ReadPrec [(k :~: a) b] #
Show ((:~:) k a b)
Methods showsPrec :: Int -> (k :~: a) b -> ShowS # show :: (k :~: a) b -> String # showList :: [(k :~: a) b] -> ShowS #
NFData ((:~:) k a b)	Since: 1.4.3.0
Methods rnf :: (k :~: a) b -> () #

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.

Minimal complete definition

eqF

Methods

eqF :: f a -> f a -> Bool Source #

Instances

Eq a => EqF k (Const k a) Source #
Methods eqF :: f a -> f a -> Bool Source #

class PolyEq u v where Source #

A polymorphic equality operator that generalizes TestEquality.

Minimal complete definition

polyEqF

Methods

polyEqF :: u -> v -> Maybe (u :~: v) Source #

polyEq :: u -> v -> Bool Source #

Instances

PolyEq (NatRepr m) (NatRepr n) Source #
Methods polyEqF :: NatRepr m -> NatRepr n -> Maybe ((* :~: NatRepr m) (NatRepr n)) Source # polyEq :: NatRepr m -> NatRepr n -> Bool Source #
TestEquality k f => PolyEq (Assignment k f x) (Assignment k f y) Source #
Methods polyEqF :: Assignment k f x -> Assignment k f y -> Maybe ((* :~: Assignment k f x) (Assignment k f y)) Source # polyEq :: Assignment k f x -> Assignment k 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

compareF

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 #

geqF :: ktp x -> ktp y -> Bool Source #

gtF :: ktp x -> ktp y -> Bool Source #

Instances

OrdF Nat NatRepr Source #
Methods compareF :: ktp x -> ktp y -> OrderingF NatRepr x y Source # leqF :: ktp x -> ktp y -> Bool Source # ltF :: ktp x -> ktp y -> Bool Source # geqF :: ktp x -> ktp y -> Bool Source # gtF :: ktp x -> ktp y -> Bool Source #
OrdF Symbol SymbolRepr Source #
Methods compareF :: ktp x -> ktp y -> OrderingF SymbolRepr x y Source # leqF :: ktp x -> ktp y -> Bool Source # ltF :: ktp x -> ktp y -> Bool Source # geqF :: ktp x -> ktp y -> Bool Source # gtF :: ktp x -> ktp y -> Bool Source #
OrdF k (Nonce k) Source #
Methods compareF :: ktp x -> ktp y -> OrderingF (Nonce k) x y Source # leqF :: ktp x -> ktp y -> Bool Source # ltF :: ktp x -> ktp y -> Bool Source # geqF :: ktp x -> ktp y -> Bool Source # gtF :: ktp x -> ktp y -> Bool Source #
OrdF k (Nonce k s) Source #
Methods compareF :: ktp x -> ktp y -> OrderingF (Nonce k s) x y Source # leqF :: ktp x -> ktp y -> Bool Source # ltF :: ktp x -> ktp y -> Bool Source # geqF :: ktp x -> ktp y -> Bool Source # gtF :: ktp x -> ktp y -> Bool Source #
OrdF k (Index k l) Source #
Methods compareF :: ktp x -> ktp y -> OrderingF (Index k l) x y Source # leqF :: ktp x -> ktp y -> Bool Source # ltF :: ktp x -> ktp y -> Bool Source # geqF :: ktp x -> ktp y -> Bool Source # gtF :: ktp x -> ktp y -> Bool Source #
OrdF k (Index k ctx) Source #
Methods compareF :: ktp x -> ktp y -> OrderingF (Index k ctx) x y Source # leqF :: ktp x -> ktp y -> Bool Source # ltF :: ktp x -> ktp y -> Bool Source # geqF :: ktp x -> ktp y -> Bool Source # gtF :: ktp x -> ktp y -> Bool Source #
OrdF k (Index k ctx) Source #
Methods compareF :: ktp x -> ktp y -> OrderingF (Index k ctx) x y Source # leqF :: ktp x -> ktp y -> Bool Source # ltF :: ktp x -> ktp y -> Bool Source # geqF :: ktp x -> ktp y -> Bool Source # gtF :: ktp x -> ktp y -> Bool Source #
OrdF k f => OrdF [k] (List k f) Source #
Methods compareF :: ktp x -> ktp y -> OrderingF (List k f) x y Source # leqF :: ktp x -> ktp y -> Bool Source # ltF :: ktp x -> ktp y -> Bool Source # geqF :: ktp x -> ktp y -> Bool Source # gtF :: ktp x -> ktp y -> Bool Source #
OrdF k f => OrdF (Ctx k) (Assignment k f) Source #
Methods compareF :: ktp x -> ktp y -> OrderingF (Assignment k f) x y Source # leqF :: ktp x -> ktp y -> Bool Source # ltF :: ktp x -> ktp y -> Bool Source # geqF :: ktp x -> ktp y -> Bool Source # gtF :: ktp x -> ktp y -> Bool Source #
OrdF k f => OrdF (Ctx k) (Assignment k f) Source #
Methods compareF :: ktp x -> ktp y -> OrderingF (Assignment k f) x y Source # leqF :: ktp x -> ktp y -> Bool Source # ltF :: ktp x -> ktp y -> Bool Source # geqF :: ktp x -> ktp y -> Bool Source # gtF :: ktp x -> ktp y -> Bool Source #

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

data OrderingF x y where Source #

Ordering over two distinct types with a proof they are equal.

Constructors

LTF :: OrderingF x y
EQF :: OrderingF x x
GTF :: OrderingF x y

joinOrderingF :: forall (a :: j) (b :: j) (c :: k) (d :: k). OrderingF a b -> (a ~ b => OrderingF c d) -> OrderingF c d Source #

`joinOrderingF x y` first compares on x, returning an equivalent value if it is not EQF. If it is EQF, it returns y.

orderingF_refl :: OrderingF x y -> Maybe (x :~: y) Source #

toOrdering :: OrderingF x y -> Ordering Source #

Convert OrderingF to standard ordering.

fromOrdering :: Ordering -> OrderingF x x Source #

Convert standard ordering to OrderingF.

Typeclass generalizations

class ShowF (f :: k -> *) where Source #

A parameterized type that can be shown on all instances.

To implement ShowF g, one should implement an instance Show (g tp) for all argument types tp, then write an empty instance instance ShowF g.

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 #

showsF :: forall tp. f tp -> String -> String Source #

Instances

ShowF Nat NatRepr Source #
Methods withShow :: p f -> q tp -> (Show (f tp) -> a) -> a Source # showF :: f tp -> String Source # showsF :: f tp -> String -> String Source #
ShowF Symbol SymbolRepr Source #
Methods withShow :: p f -> q tp -> (Show (f tp) -> a) -> a Source # showF :: f tp -> String Source # showsF :: f tp -> String -> String Source #
ShowF k (Nonce k) Source #
Methods withShow :: p f -> q tp -> (Show (f tp) -> a) -> a Source # showF :: f tp -> String Source # showsF :: f tp -> String -> String Source #
Show x => ShowF k (Const k x) Source #
Methods withShow :: p f -> q tp -> (Show (f tp) -> a) -> a Source # showF :: f tp -> String Source # showsF :: f tp -> String -> String Source #
ShowF k (Nonce k s) Source #
Methods withShow :: p f -> q tp -> (Show (f tp) -> a) -> a Source # showF :: f tp -> String Source # showsF :: f tp -> String -> String Source #
ShowF k (Index k l) Source #
Methods withShow :: p f -> q tp -> (Show (f tp) -> a) -> a Source # showF :: f tp -> String Source # showsF :: f tp -> String -> String Source #
ShowF k (Index k ctx) Source #
Methods withShow :: p f -> q tp -> (Show (f tp) -> a) -> a Source # showF :: f tp -> String Source # showsF :: f tp -> String -> String Source #
ShowF k (Index k ctx) Source #
Methods withShow :: p f -> q tp -> (Show (f tp) -> a) -> a Source # showF :: f tp -> String Source # showsF :: f tp -> String -> String Source #
ShowF k f => ShowF [k] (List k f) Source #
Methods withShow :: p f -> q tp -> (Show (f tp) -> a) -> a Source # showF :: f tp -> String Source # showsF :: f tp -> String -> String Source #
ShowF k f => ShowF (Ctx k) (Assignment k f) Source #
Methods withShow :: p f -> q tp -> (Show (f tp) -> a) -> a Source # showF :: f tp -> String Source # showsF :: f tp -> String -> String Source #
ShowF k f => ShowF (Ctx k) (Assignment k f) Source #
Methods withShow :: p f -> q tp -> (Show (f tp) -> a) -> a Source # showF :: f tp -> String Source # showsF :: f tp -> String -> String Source #

class HashableF (f :: k -> *) where Source #

A parameterized type that is hashable on all instances.

Minimal complete definition

hashWithSaltF

Methods

hashWithSaltF :: Int -> f tp -> Int Source #

hashF :: f tp -> Int Source #

Hash with default salt.

Instances

HashableF Nat NatRepr Source #
Methods hashWithSaltF :: Int -> f tp -> Int Source # hashF :: f tp -> Int Source #
HashableF Symbol SymbolRepr Source #
Methods hashWithSaltF :: Int -> f tp -> Int Source # hashF :: f tp -> Int Source #
HashableF k (Nonce k) Source #
Methods hashWithSaltF :: Int -> f tp -> Int Source # hashF :: f tp -> Int Source #
Hashable a => HashableF k (Const k a) Source #
Methods hashWithSaltF :: Int -> f tp -> Int Source # hashF :: f tp -> Int Source #
HashableF k (Nonce k s) Source #
Methods hashWithSaltF :: Int -> f tp -> Int Source # hashF :: f tp -> Int Source #
HashableF k (Index k ctx) Source #
Methods hashWithSaltF :: Int -> f tp -> Int Source # hashF :: f tp -> Int Source #
HashableF k (Index k ctx) Source #
Methods hashWithSaltF :: Int -> f tp -> Int Source # hashF :: f tp -> Int Source #
HashableF k f => HashableF (Ctx k) (Assignment k f) Source #
Methods hashWithSaltF :: Int -> f tp -> Int Source # hashF :: f tp -> Int Source #
HashableF k f => HashableF (Ctx k) (Assignment k f) Source #
Methods hashWithSaltF :: Int -> f tp -> Int Source # hashF :: 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.

Minimal complete definition

coerceF

Methods

coerceF :: rtp a -> rtp b Source #

Instances

CoercibleF k (Const k x) Source #
Methods coerceF :: rtp a -> rtp b Source #

Optics generalizations

type family IndexF (m :: *) :: k -> * Source #

Instances

type IndexF k (Assignment k f ctx) Source #
type IndexF k (Assignment k f ctx) = Index k ctx
type IndexF k (Assignment k f ctx) Source #
type IndexF k (Assignment k f ctx) = Index k ctx
type IndexF k1 (MapF k1 k2 v) Source #
type IndexF k1 (MapF k1 k2 v) = k2

type family IxValueF (m :: *) :: k -> * Source #

Instances

type IxValueF k (Assignment k f ctx) Source #
type IxValueF k (Assignment k f ctx) = f
type IxValueF k (Assignment k f ctx) Source #
type IxValueF k (Assignment k f ctx) = f
type IxValueF k1 (MapF k1 k2 v) Source #
type IxValueF k1 (MapF k1 k2 v) = v

class IxedF k m where Source #

Parameterized generalization of the lens Ixed class.

Minimal complete definition

ixF

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 k f ctx) Source #
Methods ixF :: IndexF k (Assignment k f ctx) x -> Traversal' (Assignment k f ctx) (IxValueF k (Assignment k f ctx) x) Source #
IxedF k (Assignment k f ctx) Source #
Methods ixF :: IndexF k (Assignment k f ctx) x -> Traversal' (Assignment k f ctx) (IxValueF k (Assignment k f ctx) x) Source #
OrdF a k => IxedF a (MapF a k v) Source #	Turn a map key into a traversal that visits the indicated element in the map, if it exists.
Methods ixF :: IndexF a (MapF a k v) x -> Traversal' (MapF a k v) (IxValueF a (MapF a k v) x) Source #

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.

Minimal complete definition

ixF'

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 k f ctx) Source #
Methods ixF' :: IndexF k (Assignment k f ctx) x -> Lens' (Assignment k f ctx) (IxValueF k (Assignment k f ctx) x) Source #
IxedF' k (Assignment k f ctx) Source #
Methods ixF' :: IndexF k (Assignment k f ctx) x -> Lens' (Assignment k f ctx) (IxValueF k (Assignment k f ctx) x) Source #

class IxedF k m => AtF k m where Source #

Parameterized generalization of the lens At class.

Minimal complete definition

atF

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.

Instances

OrdF a k => AtF a (MapF a k v) Source #	Turn a map key into a lens that points into the indicated position in the map.
Methods atF :: IndexF a (MapF a k v) x -> Lens' (MapF a k v) (Maybe (IxValueF a (MapF a k v) x)) Source #

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.

Minimal complete definition

knownRepr

Methods

knownRepr :: f ctx Source #

Instances

KnownNat n => KnownRepr Nat NatRepr n Source #
Methods knownRepr :: n ctx Source #
KnownSymbol s => KnownRepr Symbol SymbolRepr s Source #
Methods knownRepr :: s ctx Source #
KnownRepr [k] (List k f) ([] k) Source #
Methods knownRepr :: [k] ctx Source #
KnownRepr (Ctx k) (Assignment k f) (EmptyCtx k) Source #
Methods knownRepr :: EmptyCtx k ctx Source #
KnownRepr (Ctx k) (Assignment k f) (EmptyCtx k) Source #
Methods knownRepr :: EmptyCtx k ctx Source #
(KnownRepr a f s, KnownRepr [a] (List a f) sh) => KnownRepr [a] (List a f) ((:) a s sh) Source #
Methods knownRepr :: (a ': s) sh ctx Source #
(KnownRepr (Ctx k) (Assignment k f) ctx, KnownRepr k f bt) => KnownRepr (Ctx k) (Assignment k f) ((::>) k ctx bt) Source #
Methods knownRepr :: (k ::> ctx) bt ctx Source #
(KnownRepr (Ctx k) (Assignment k f) ctx, KnownRepr k f bt) => KnownRepr (Ctx k) (Assignment k f) ((::>) k ctx bt) Source #
Methods knownRepr :: (k ::> ctx) bt ctx Source #

Re-exports

isJust :: Maybe a -> Bool #

The isJust function returns True iff its argument is of the form Just _.

Examples

Basic usage:

>>> isJust (Just 3)
True

>>> isJust (Just ())
True

>>> isJust Nothing
False

Only the outer constructor is taken into consideration:

>>> isJust (Just Nothing)
True