parameterized-utils-2.1.5.0: Classes and data structures for working with data-kind indexed types
Copyright(c) Galois Inc 2014-2019
MaintainerJoe Hendrix <jhendrix@galois.com>
Safe HaskellTrustworthy
LanguageHaskell2010

Data.Parameterized.NatRepr

Description

This defines a type NatRepr for representing a type-level natural at runtime. This can be used to branch on a type-level value. For each n, NatRepr n contains a single value containing the value n. This can be used to help use type-level variables on code with data dependendent types.

The TestEquality and DecidableEq instances for NatRepr are implemented using unsafeCoerce, as is the isZeroNat function. This should be typesafe because we maintain the invariant that the integer value contained in a NatRepr value matches its static type.

Synopsis

Documentation

data NatRepr (n :: Nat) Source #

A runtime presentation of a type-level Nat.

This can be used for performing dynamic checks on a type-level natural numbers.

Instances

Instances details
TestEquality NatRepr Source # 
Instance details

Defined in Data.Parameterized.NatRepr.Internal

Methods

testEquality :: forall (a :: k) (b :: k). NatRepr a -> NatRepr b -> Maybe (a :~: b) #

HashableF NatRepr Source # 
Instance details

Defined in Data.Parameterized.NatRepr.Internal

Methods

hashWithSaltF :: forall (tp :: k). Int -> NatRepr tp -> Int Source #

hashF :: forall (tp :: k). NatRepr tp -> Int Source #

ShowF NatRepr Source # 
Instance details

Defined in Data.Parameterized.NatRepr.Internal

Methods

withShow :: forall p q (tp :: k) a. p NatRepr -> q tp -> (Show (NatRepr tp) => a) -> a Source #

showF :: forall (tp :: k). NatRepr tp -> String Source #

showsPrecF :: forall (tp :: k). Int -> NatRepr tp -> String -> String Source #

OrdF NatRepr Source # 
Instance details

Defined in Data.Parameterized.NatRepr.Internal

Methods

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 #

DecidableEq NatRepr Source # 
Instance details

Defined in Data.Parameterized.NatRepr.Internal

Methods

decEq :: forall (a :: k) (b :: k). NatRepr a -> NatRepr b -> Either (a :~: b) ((a :~: b) -> Void) Source #

IsRepr NatRepr Source # 
Instance details

Defined in Data.Parameterized.WithRepr

Methods

withRepr :: forall (a :: k) r. NatRepr a -> (KnownRepr NatRepr a => r) -> r Source #

KnownNat n => KnownRepr NatRepr (n :: Nat) Source # 
Instance details

Defined in Data.Parameterized.NatRepr.Internal

Eq (NatRepr m) Source # 
Instance details

Defined in Data.Parameterized.NatRepr.Internal

Methods

(==) :: NatRepr m -> NatRepr m -> Bool #

(/=) :: NatRepr m -> NatRepr m -> Bool #

KnownNat n => Data (NatRepr n) Source # 
Instance details

Defined in Data.Parameterized.NatRepr.Internal

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> NatRepr n -> c (NatRepr n) #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (NatRepr n) #

toConstr :: NatRepr n -> Constr #

dataTypeOf :: NatRepr n -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (NatRepr n)) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (NatRepr n)) #

gmapT :: (forall b. Data b => b -> b) -> NatRepr n -> NatRepr n #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> NatRepr n -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> NatRepr n -> r #

gmapQ :: (forall d. Data d => d -> u) -> NatRepr n -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> NatRepr n -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> NatRepr n -> m (NatRepr n) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> NatRepr n -> m (NatRepr n) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> NatRepr n -> m (NatRepr n) #

Show (NatRepr n) Source # 
Instance details

Defined in Data.Parameterized.NatRepr.Internal

Methods

showsPrec :: Int -> NatRepr n -> ShowS #

show :: NatRepr n -> String #

showList :: [NatRepr n] -> ShowS #

Hashable (NatRepr n) Source # 
Instance details

Defined in Data.Parameterized.NatRepr.Internal

Methods

hashWithSalt :: Int -> NatRepr n -> Int #

hash :: NatRepr n -> Int #

PolyEq (NatRepr m) (NatRepr n) Source # 
Instance details

Defined in Data.Parameterized.NatRepr.Internal

natValue :: NatRepr n -> Natural Source #

The underlying natural value of the number.

knownNat :: forall n. KnownNat n => NatRepr n Source #

This generates a NatRepr from a type-level context.

withKnownNat :: forall n r. NatRepr n -> (KnownNat n => r) -> r Source #

data IsZeroNat n where Source #

Constructors

ZeroNat :: IsZeroNat 0 
NonZeroNat :: IsZeroNat (n + 1) 

isZeroOrGT1 :: NatRepr n -> Either (n :~: 0) (LeqProof 1 n) Source #

Every nat is either zero or >= 1.

data NatComparison m n where Source #

Result of comparing two numbers.

Constructors

NatLT :: (x + 1) <= (x + (y + 1)) => !(NatRepr y) -> NatComparison x (x + (y + 1)) 
NatEQ :: NatComparison x x 
NatGT :: (x + 1) <= (x + (y + 1)) => !(NatRepr y) -> NatComparison (x + (y + 1)) x 

decNat :: 1 <= n => NatRepr n -> NatRepr (n - 1) Source #

Decrement a NatRepr

predNat :: NatRepr (n + 1) -> NatRepr n Source #

Get the predecessor of a nat

incNat :: NatRepr n -> NatRepr (n + 1) Source #

Increment a NatRepr

addNat :: NatRepr m -> NatRepr n -> NatRepr (m + n) Source #

subNat :: n <= m => NatRepr m -> NatRepr n -> NatRepr (m - n) Source #

divNat :: 1 <= n => NatRepr (m * n) -> NatRepr n -> NatRepr m Source #

withDivModNat :: forall n m a. NatRepr n -> NatRepr m -> (forall div mod. n ~ ((div * m) + mod) => NatRepr div -> NatRepr mod -> a) -> a Source #

someNat :: Integral a => a -> Maybe (Some NatRepr) Source #

Turn an Integral value into a NatRepr. Returns Nothing if the given value is negative.

mkNatRepr :: Natural -> Some NatRepr Source #

Turn a Natural into the corresponding NatRepr

maxNat :: NatRepr m -> NatRepr n -> Some NatRepr Source #

Return the maximum of two nat representations.

natRec Source #

Arguments

:: forall p f. NatRepr p 
-> f 0

base case

-> (forall n. NatRepr n -> f n -> f (n + 1)) 
-> f p 

Recursor for natural numbeers.

natRecStrong Source #

Arguments

:: forall p f. NatRepr p 
-> f 0

base case

-> (forall n. NatRepr n -> (forall m. m <= n => NatRepr m -> f m) -> f (n + 1))

inductive step

-> f p 

Strong induction variant of the recursor.

natRecBounded :: forall m h f. m <= h => NatRepr m -> NatRepr h -> f 0 -> (forall n. n <= h => NatRepr n -> f n -> f (n + 1)) -> f (m + 1) Source #

Bounded recursor for natural numbers.

If you can prove: - Base case: f 0 - Inductive step: if n <= h and (f n) then (f (n + 1)) You can conclude: for all n <= h, (f (n + 1)).

natForEach :: forall l h a. NatRepr l -> NatRepr h -> (forall n. (l <= n, n <= h) => NatRepr n -> a) -> [a] Source #

Apply a function to each element in a range; return the list of values obtained.

natFromZero :: forall h a. NatRepr h -> (forall n. n <= h => NatRepr n -> a) -> [a] Source #

Apply a function to each element in a range starting at zero; return the list of values obtained.

data NatCases m n where Source #

Constructors

NatCaseLT :: LeqProof (m + 1) n -> NatCases m n 
NatCaseEQ :: NatCases m m 
NatCaseGT :: LeqProof (n + 1) m -> NatCases m n 

testNatCases :: forall m n. NatRepr m -> NatRepr n -> NatCases m n Source #

Strict order

lessThanIrreflexive :: forall f (a :: Nat). f a -> LeqProof (1 + a) a -> Void Source #

The strict order (<), defined by n < m <-> n + 1 <= m, is irreflexive.

lessThanAsymmetric :: forall m f n. LeqProof (n + 1) m -> LeqProof (m + 1) n -> f n -> Void Source #

The strict order on the naturals is asymmetric

Bitvector utilities

widthVal :: NatRepr n -> Int Source #

Return the value of the nat representation.

minUnsigned :: NatRepr w -> Integer Source #

Return minimum unsigned value for bitvector with given width (always 0).

maxUnsigned :: NatRepr w -> Integer Source #

Return maximum unsigned value for bitvector with given width.

minSigned :: 1 <= w => NatRepr w -> Integer Source #

Return minimum value for bitvector in two's complement with given width.

maxSigned :: 1 <= w => NatRepr w -> Integer Source #

Return maximum value for bitvector in two's complement with given width.

toUnsigned :: NatRepr w -> Integer -> Integer Source #

toUnsigned w i maps i to a i mod 2^w.

toSigned :: 1 <= w => NatRepr w -> Integer -> Integer Source #

toSigned w i interprets the least-significant w bits in i as a signed number in two's complement notation and returns that value.

unsignedClamp :: NatRepr w -> Integer -> Integer Source #

unsignedClamp w i rounds i to the nearest value between 0 and 2^w-1 (inclusive).

signedClamp :: 1 <= w => NatRepr w -> Integer -> Integer Source #

signedClamp w i rounds i to the nearest value between -2^(w-1) and 2^(w-1)-1 (inclusive).

LeqProof

data LeqProof (m :: Nat) (n :: Nat) where Source #

LeqProof m n is a type whose values are only inhabited when m is less than or equal to n.

Constructors

LeqProof :: m <= n => LeqProof m n 

decideLeq :: NatRepr a -> NatRepr b -> Either (LeqProof a b) (LeqProof a b -> Void) Source #

(<=) is a decidable relation on nats.

testLeq :: forall m n. NatRepr m -> NatRepr n -> Maybe (LeqProof m n) Source #

x testLeq y checks whether x is less than or equal to y.

testStrictLeq :: forall m n. m <= n => NatRepr m -> NatRepr n -> Either (LeqProof (m + 1) n) (m :~: n) Source #

leqRefl :: forall f n. f n -> LeqProof n n Source #

Apply reflexivity to LeqProof

leqTrans :: LeqProof m n -> LeqProof n p -> LeqProof m p Source #

Apply transitivity to LeqProof

leqZero :: LeqProof 0 n Source #

Zero is less than or equal to any Nat.

leqAdd2 :: LeqProof x_l x_h -> LeqProof y_l y_h -> LeqProof (x_l + y_l) (x_h + y_h) Source #

Add both sides of two inequalities

leqSub2 :: LeqProof x_l x_h -> LeqProof y_l y_h -> LeqProof (x_l - y_h) (x_h - y_l) Source #

Subtract sides of two inequalities.

leqMulCongr :: LeqProof a x -> LeqProof b y -> LeqProof (a * b) (x * y) Source #

Congruence rule for multiplication

LeqProof combinators

leqProof :: m <= n => f m -> g n -> LeqProof m n Source #

Create a leqProof using two proxies

withLeqProof :: LeqProof m n -> (m <= n => a) -> a Source #

isPosNat :: NatRepr n -> Maybe (LeqProof 1 n) Source #

Test whether natural number is positive.

leqAdd :: forall f m n p. LeqProof m n -> f p -> LeqProof m (n + p) Source #

Produce proof that adding a value to the larger element in an LeqProof is larger

leqSub :: forall m n p. LeqProof m n -> LeqProof p m -> LeqProof (m - p) n Source #

Produce proof that subtracting a value from the smaller element is smaller.

leqMulPos :: forall p q x y. (1 <= x, 1 <= y) => p x -> q y -> LeqProof 1 (x * y) Source #

Multiplying two positive numbers results in a positive number.

leqAddPos :: (1 <= m, 1 <= n) => p m -> q n -> LeqProof 1 (m + n) Source #

addIsLeq :: f n -> g m -> LeqProof n (n + m) Source #

withAddLeq :: forall n m a. NatRepr n -> NatRepr m -> (n <= (n + m) => NatRepr (n + m) -> a) -> a Source #

addPrefixIsLeq :: f m -> g n -> LeqProof n (m + n) Source #

withAddPrefixLeq :: NatRepr n -> NatRepr m -> (m <= (n + m) => a) -> a Source #

addIsLeqLeft1 :: forall n n' m. LeqProof (n + n') m -> LeqProof n m Source #

dblPosIsPos :: forall n. LeqProof 1 n -> LeqProof 1 (n + n) Source #

leqMulMono :: 1 <= x => p x -> q y -> LeqProof y (x * y) Source #

Arithmetic proof

plusComm :: forall f m g n. f m -> g n -> (m + n) :~: (n + m) Source #

Produce evidence that + is commutative.

plusAssoc :: forall f m g n h o. f m -> g n -> h o -> (m + (n + o)) :~: ((m + n) + o) Source #

Produce evidence that + is associative.

mulComm :: forall f m g n. f m -> g n -> (m * n) :~: (n * m) Source #

Produce evidence that * is commutative.

plusMinusCancel :: forall f m g n. f m -> g n -> ((m + n) - n) :~: m Source #

Cancel an add followed by a subtract

minusPlusCancel :: forall f m g n. n <= m => f m -> g n -> ((m - n) + n) :~: m Source #

addMulDistribRight :: forall n m p f g h. f n -> g m -> h p -> ((n * p) + (m * p)) :~: ((n + m) * p) Source #

withAddMulDistribRight :: forall n m p f g h a. f n -> g m -> h p -> (((n * p) + (m * p)) ~ ((n + m) * p) => a) -> a Source #

withSubMulDistribRight :: forall n m p f g h a. m <= n => f n -> g m -> h p -> (((n * p) - (m * p)) ~ ((n - m) * p) => a) -> a Source #

mulCancelR :: (1 <= c, (n1 * c) ~ (n2 * c)) => f1 n1 -> f2 n2 -> f3 c -> n1 :~: n2 Source #

mul2Plus :: forall f n. f n -> (n + n) :~: (2 * n) Source #

lemmaMul :: 1 <= n => p w -> q n -> (w + ((n - 1) * w)) :~: (n * w) Source #

Used in Vector

Re-exports typelists basics

type family (a :: Nat) + (b :: Nat) :: Nat where ... infixl 6 #

Addition of type-level naturals.

Since: base-4.7.0.0

type family (a :: Nat) - (b :: Nat) :: Nat where ... infixl 6 #

Subtraction of type-level naturals.

Since: base-4.7.0.0

type family (a :: Nat) * (b :: Nat) :: Nat where ... infixl 7 #

Multiplication of type-level naturals.

Since: base-4.7.0.0

type (<=) (x :: Nat) (y :: Nat) = (x <=? y) ~ 'True infix 4 #

Comparison of type-level naturals, as a constraint.

Since: base-4.7.0.0

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.

Methods

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

Conditionally prove the equality of a and b.

Instances

Instances details
TestEquality BoolRepr Source # 
Instance details

Defined in Data.Parameterized.BoolRepr

Methods

testEquality :: forall (a :: k) (b :: k). BoolRepr a -> BoolRepr b -> Maybe (a :~: b) #

TestEquality NatRepr Source # 
Instance details

Defined in Data.Parameterized.NatRepr.Internal

Methods

testEquality :: forall (a :: k) (b :: k). NatRepr a -> NatRepr b -> Maybe (a :~: b) #

TestEquality SymbolRepr Source # 
Instance details

Defined in Data.Parameterized.SymbolRepr

Methods

testEquality :: forall (a :: k) (b :: k). SymbolRepr a -> SymbolRepr b -> Maybe (a :~: b) #

TestEquality PeanoRepr Source # 
Instance details

Defined in Data.Parameterized.Peano

Methods

testEquality :: forall (a :: k) (b :: k). PeanoRepr a -> PeanoRepr b -> Maybe (a :~: b) #

TestEquality (Nonce :: k -> Type) Source # 
Instance details

Defined in Data.Parameterized.Nonce.Unsafe

Methods

testEquality :: forall (a :: k0) (b :: k0). Nonce a -> Nonce b -> Maybe (a :~: b) #

TestEquality (TypeRep :: k -> Type) 
Instance details

Defined in Data.Typeable.Internal

Methods

testEquality :: forall (a :: k0) (b :: k0). TypeRep a -> TypeRep b -> Maybe (a :~: b) #

TestEquality (Nonce s :: k -> Type) Source # 
Instance details

Defined in Data.Parameterized.Nonce

Methods

testEquality :: forall (a :: k0) (b :: k0). Nonce s a -> Nonce s b -> Maybe (a :~: b) #

TestEquality ((:~:) a :: k -> Type)

Since: base-4.7.0.0

Instance details

Defined in Data.Type.Equality

Methods

testEquality :: forall (a0 :: k0) (b :: k0). (a :~: a0) -> (a :~: b) -> Maybe (a0 :~: b) #

TestEquality (Index l :: k -> Type) Source # 
Instance details

Defined in Data.Parameterized.List

Methods

testEquality :: forall (a :: k0) (b :: k0). Index l a -> Index l b -> Maybe (a :~: b) #

TestEquality (Index ctx :: k -> Type) Source # 
Instance details

Defined in Data.Parameterized.Context.Unsafe

Methods

testEquality :: forall (a :: k0) (b :: k0). Index ctx a -> Index ctx b -> Maybe (a :~: b) #

TestEquality ((:~~:) a :: k -> Type)

Since: base-4.10.0.0

Instance details

Defined in Data.Type.Equality

Methods

testEquality :: forall (a0 :: k0) (b :: k0). (a :~~: a0) -> (a :~~: b) -> Maybe (a0 :~: b) #

TestEquality f => TestEquality (Compose f g :: k2 -> Type)

The deduction (via generativity) that if g x :~: g y then x :~: y.

Since: base-4.14.0.0

Instance details

Defined in Data.Functor.Compose

Methods

testEquality :: forall (a :: k) (b :: k). Compose f g a -> Compose f g b -> Maybe (a :~: b) #

TestEquality f => TestEquality (List f :: [k] -> Type) Source # 
Instance details

Defined in Data.Parameterized.List

Methods

testEquality :: forall (a :: k0) (b :: k0). List f a -> List f b -> Maybe (a :~: b) #

TestEquality f => TestEquality (Assignment f :: Ctx k -> Type) Source # 
Instance details

Defined in Data.Parameterized.Context.Unsafe

Methods

testEquality :: forall (a :: k0) (b :: k0). Assignment f a -> Assignment f b -> Maybe (a :~: b) #

(TestEquality f, TestEquality g) => TestEquality (PairRepr f g :: (k1, k2) -> Type) Source # 
Instance details

Defined in Data.Parameterized.DataKind

Methods

testEquality :: forall (a :: k) (b :: k). PairRepr f g a -> PairRepr f g b -> Maybe (a :~: b) #

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

Constructors

Refl :: forall k (a :: k). a :~: a 

Instances

Instances details
Category ((:~:) :: k -> k -> Type)

Since: base-4.7.0.0

Instance details

Defined in Control.Category

Methods

id :: forall (a :: k0). a :~: a #

(.) :: forall (b :: k0) (c :: k0) (a :: k0). (b :~: c) -> (a :~: b) -> a :~: c #

TestEquality ((:~:) a :: k -> Type)

Since: base-4.7.0.0

Instance details

Defined in Data.Type.Equality

Methods

testEquality :: forall (a0 :: k0) (b :: k0). (a :~: a0) -> (a :~: b) -> Maybe (a0 :~: b) #

NFData2 ((:~:) :: Type -> Type -> Type)

Since: deepseq-1.4.3.0

Instance details

Defined in Control.DeepSeq

Methods

liftRnf2 :: (a -> ()) -> (b -> ()) -> (a :~: b) -> () #

NFData1 ((:~:) a)

Since: deepseq-1.4.3.0

Instance details

Defined in Control.DeepSeq

Methods

liftRnf :: (a0 -> ()) -> (a :~: a0) -> () #

a ~ b => Bounded (a :~: b)

Since: base-4.7.0.0

Instance details

Defined in Data.Type.Equality

Methods

minBound :: a :~: b #

maxBound :: a :~: b #

a ~ b => Enum (a :~: b)

Since: base-4.7.0.0

Instance details

Defined in Data.Type.Equality

Methods

succ :: (a :~: b) -> a :~: b #

pred :: (a :~: b) -> a :~: b #

toEnum :: Int -> 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

Instance details

Defined in Data.Type.Equality

Methods

(==) :: (a :~: b) -> (a :~: b) -> Bool #

(/=) :: (a :~: b) -> (a :~: b) -> Bool #

(a ~ b, Data a) => Data (a :~: b)

Since: base-4.7.0.0

Instance details

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 :: 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

Instance details

Defined in Data.Type.Equality

Methods

compare :: (a :~: b) -> (a :~: b) -> Ordering #

(<) :: (a :~: b) -> (a :~: b) -> Bool #

(<=) :: (a :~: b) -> (a :~: b) -> Bool #

(>) :: (a :~: b) -> (a :~: b) -> Bool #

(>=) :: (a :~: b) -> (a :~: b) -> Bool #

max :: (a :~: b) -> (a :~: b) -> a :~: b #

min :: (a :~: b) -> (a :~: b) -> a :~: b #

a ~ b => Read (a :~: b)

Since: base-4.7.0.0

Instance details

Defined in Data.Type.Equality

Methods

readsPrec :: Int -> ReadS (a :~: b) #

readList :: ReadS [a :~: b] #

readPrec :: ReadPrec (a :~: b) #

readListPrec :: ReadPrec [a :~: b] #

Show (a :~: b)

Since: base-4.7.0.0

Instance details

Defined in Data.Type.Equality

Methods

showsPrec :: Int -> (a :~: b) -> ShowS #

show :: (a :~: b) -> String #

showList :: [a :~: b] -> ShowS #

NFData (a :~: b)

Since: deepseq-1.4.3.0

Instance details

Defined in Control.DeepSeq

Methods

rnf :: (a :~: b) -> () #

HasDict (a ~ b) (a :~: b) 
Instance details

Defined in Data.Constraint

Methods

evidence :: (a :~: b) -> Dict (a ~ b) #

data Some (f :: k -> Type) Source #

Instances

Instances details
TraversableF (Some :: (k -> Type) -> Type) Source # 
Instance details

Defined in Data.Parameterized.Some

Methods

traverseF :: Applicative m => (forall (s :: k0). e s -> m (f s)) -> Some e -> m (Some f) Source #

FoldableF (Some :: (k -> Type) -> Type) Source # 
Instance details

Defined in Data.Parameterized.Some

Methods

foldMapF :: Monoid m => (forall (s :: k0). e s -> m) -> Some e -> m Source #

foldrF :: (forall (s :: k0). e s -> b -> b) -> b -> Some e -> b Source #

foldlF :: (forall (s :: k0). b -> e s -> b) -> b -> Some e -> b Source #

foldrF' :: (forall (s :: k0). e s -> b -> b) -> b -> Some e -> b Source #

foldlF' :: (forall (s :: k0). b -> e s -> b) -> b -> Some e -> b Source #

toListF :: (forall (tp :: k0). f tp -> a) -> Some f -> [a] Source #

FunctorF (Some :: (k -> Type) -> Type) Source # 
Instance details

Defined in Data.Parameterized.Some

Methods

fmapF :: (forall (x :: k0). f x -> g x) -> Some f -> Some g Source #

OrdC (Some :: (k -> Type) -> Type) Source # 
Instance details

Defined in Data.Parameterized.ClassesC

Methods

compareC :: (forall (x :: k0) (y :: k0). f x -> g y -> OrderingF x y) -> Some f -> Some g -> Ordering Source #

TestEqualityC (Some :: (k -> Type) -> Type) Source #

This instance demonstrates where the above class is useful: namely, in types with existential quantification.

Instance details

Defined in Data.Parameterized.ClassesC

Methods

testEqualityC :: (forall (x :: k0) (y :: k0). f x -> f y -> Maybe (x :~: y)) -> Some f -> Some f -> Bool Source #

TestEquality f => Eq (Some f) Source # 
Instance details

Defined in Data.Parameterized.Some

Methods

(==) :: Some f -> Some f -> Bool #

(/=) :: Some f -> Some f -> Bool #

OrdF f => Ord (Some f) Source # 
Instance details

Defined in Data.Parameterized.Some

Methods

compare :: Some f -> Some f -> Ordering #

(<) :: Some f -> Some f -> Bool #

(<=) :: Some f -> Some f -> Bool #

(>) :: Some f -> Some f -> Bool #

(>=) :: Some f -> Some f -> Bool #

max :: Some f -> Some f -> Some f #

min :: Some f -> Some f -> Some f #

ShowF f => Show (Some f) Source # 
Instance details

Defined in Data.Parameterized.Some

Methods

showsPrec :: Int -> Some f -> ShowS #

show :: Some f -> String #

showList :: [Some f] -> ShowS #

HashableF f => Hashable (Some f) Source # 
Instance details

Defined in Data.Parameterized.Some

Methods

hashWithSalt :: Int -> Some f -> Int #

hash :: Some f -> Int #