Data.Parameterized.NatRepr

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.

Documentation

data NatRepr (n :: Nat)

A runtime presentation of a type-level Nat.

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

Instances

TestEquality NatRepr

Defined in Data.Parameterized.NatRepr.Internal

Methods

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

EqF NatRepr

Defined in Data.Parameterized.NatRepr.Internal

Methods

eqF :: forall (a :: k). NatRepr a -> NatRepr a -> Bool

HashableF NatRepr

Defined in Data.Parameterized.NatRepr.Internal

Methods

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

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

OrdF NatRepr

Defined in Data.Parameterized.NatRepr.Internal

Methods

compareF :: forall (x :: k) (y :: k). NatRepr x -> NatRepr y -> OrderingF x y

leqF :: forall (x :: k) (y :: k). NatRepr x -> NatRepr y -> Bool

ltF :: forall (x :: k) (y :: k). NatRepr x -> NatRepr y -> Bool

geqF :: forall (x :: k) (y :: k). NatRepr x -> NatRepr y -> Bool

gtF :: forall (x :: k) (y :: k). NatRepr x -> NatRepr y -> Bool

ShowF NatRepr

Defined in Data.Parameterized.NatRepr.Internal

Methods

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

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

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

DecidableEq NatRepr

Defined in Data.Parameterized.NatRepr.Internal

Methods

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

IsRepr NatRepr

Defined in Data.Parameterized.WithRepr

Methods

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

KnownNat n => KnownRepr NatRepr (n :: Nat)

Defined in Data.Parameterized.NatRepr.Internal

Methods

knownRepr :: NatRepr n

KnownNat n => Data (NatRepr n)

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)

Defined in Data.Parameterized.NatRepr.Internal

Methods

showsPrec :: Int -> NatRepr n -> ShowS

show :: NatRepr n -> String

showList :: [NatRepr n] -> ShowS

Eq (NatRepr m)

Defined in Data.Parameterized.NatRepr.Internal

Methods

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

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

Hashable (NatRepr n)

Defined in Data.Parameterized.NatRepr.Internal

Methods

hashWithSalt :: Int -> NatRepr n -> Int

hash :: NatRepr n -> Int

PolyEq (NatRepr m) (NatRepr n)

Defined in Data.Parameterized.NatRepr.Internal

Methods

polyEqF :: NatRepr m -> NatRepr n -> Maybe (NatRepr m :~: NatRepr n)

polyEq :: NatRepr m -> NatRepr n -> Bool

natValue :: NatRepr n -> Natural

The underlying natural value of the number.

intValue :: NatRepr n -> Integer

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

This generates a NatRepr from a type-level context.

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

data IsZeroNat n where

Constructors

ZeroNat :: IsZeroNat 0

NonZeroNat :: IsZeroNat (n + 1)

isZeroNat :: NatRepr n -> IsZeroNat n

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

Every nat is either zero or >= 1.

data NatComparison m n where

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

compareNat :: NatRepr m -> NatRepr n -> NatComparison m n

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

Decrement a NatRepr

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

Get the predecessor of a nat

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

Increment a NatRepr

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

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

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

halfNat :: NatRepr (n + n) -> NatRepr n

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

natMultiply :: NatRepr n -> NatRepr m -> NatRepr (n * m)

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

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

mkNatRepr :: Natural -> Some NatRepr

Turn a Natural into the corresponding NatRepr

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

Return the maximum of two nat representations.

natRec

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

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)

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)).

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

A version of natRecBounded which doesn't require the type index of the result to be greater than 0 and provides a strict inequality constraint.

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

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]

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

data NatCases m n where

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

Strict order

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

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

The strict order on the naturals is asymmetric

Bitvector utilities

widthVal :: NatRepr n -> Int

Return the value of the nat representation.

minUnsigned :: NatRepr w -> Integer

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

maxUnsigned :: NatRepr w -> Integer

Return maximum unsigned value for bitvector with given width.

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

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

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

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

toUnsigned :: NatRepr w -> Integer -> Integer

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

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

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

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

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

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

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)

(<=) is a decidable relation on nats.

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

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)

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

Apply reflexivity to LeqProof

leqSucc :: forall f z. f z -> LeqProof z (z + 1)

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

Apply transitivity to LeqProof

leqZero :: LeqProof 0 n

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)

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)

Subtract sides of two inequalities.

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

Congruence rule for multiplication

LeqProof combinators

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

Create a leqProof using two proxies

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

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

Test whether natural number is positive.

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

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

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)

Multiplying two positive numbers results in a positive number.

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

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

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

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

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

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

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

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

Arithmetic proof

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

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)

Produce evidence that + is associative.

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

Produce evidence that * is commutative.

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

Cancel an add followed by a subtract

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

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

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

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

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

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

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

Used in Vector

Re-exports typelists basics

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

Addition of type-level naturals.

Since: base-4.7.0.0

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

Subtraction of type-level naturals.

Since: base-4.7.0.0

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

Multiplication of type-level naturals.

Since: base-4.7.0.0

type (<=) (x :: t) (y :: t) = Assert (x <=? y) (LeErrMsg x y :: Constraint) infix 4

Comparison (<=) of comparable types, as a constraint.

Since: base-4.16.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.

The result should be Just Refl if and only if the types applied to f are equal:

testEquality (x :: f a) (y :: f b) = Just Refl ⟺ a = b

Typically, only singleton types should inhabit this class. In that case type argument equality coincides with term equality:

testEquality (x :: f a) (y :: f b) = Just Refl ⟺ a = b ⟺ x = y

isJust (testEquality x y) = x == y

Singleton types are not required, however, and so the latter two would-be laws are not in fact valid in general.

Methods

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

Conditionally prove the equality of a and b.

Instances

TestEquality SNat

Since: base-4.18.0.0

Defined in GHC.TypeNats

Methods

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

TestEquality NatRepr

Defined in Data.Parameterized.NatRepr.Internal

Methods

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

TestEquality PeanoRepr

Defined in Data.Parameterized.Peano

Methods

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

TestEquality BoolRepr

Defined in Data.Parameterized.BoolRepr

Methods

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

TestEquality SChar

Since: base-4.18.0.0

Defined in GHC.TypeLits

Methods

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

TestEquality SSymbol

Since: base-4.18.0.0

Defined in GHC.TypeLits

Methods

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

TestEquality SymbolRepr

Defined in Data.Parameterized.SymbolRepr

Methods

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

TestEquality (TypeRep :: k -> Type)

Defined in Data.Typeable.Internal

Methods

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

TestEquality (Nonce :: k -> Type)

Defined in Data.Parameterized.Nonce.Unsafe

Methods

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

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

Since: base-4.7.0.0

Defined in Data.Type.Equality

Methods

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

TestEquality (Index ctx :: k -> Type)

Defined in Data.Parameterized.Context.Unsafe

Methods

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

TestEquality (Index l :: k -> Type)

Defined in Data.Parameterized.List

Methods

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

TestEquality (Nonce s :: k -> Type)

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.10.0.0

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

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 (Assignment f :: Ctx k -> Type)

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 (List f :: [k] -> Type)

Defined in Data.Parameterized.List

Methods

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

(TestEquality f, TestEquality g) => TestEquality (PairRepr f g :: (k1, k2) -> Type)

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

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

Since: base-4.7.0.0

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

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

Defined in Control.DeepSeq

Methods

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

NFData1 ((:~:) a)

Since: deepseq-1.4.3.0

Defined in Control.DeepSeq

Methods

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

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

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

Since: base-4.7.0.0

Defined in Data.Type.Equality

Methods

minBound :: a :~: b

maxBound :: a :~: b

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

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]

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

Since: base-4.7.0.0

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

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

Defined in Control.DeepSeq

Methods

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

Eq (a :~: b)

Since: base-4.7.0.0

Defined in Data.Type.Equality

Methods

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

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

Ord (a :~: b)

Since: base-4.7.0.0

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

HasDict (a ~ b) (a :~: b)

Defined in Data.Constraint

Methods

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

data Some (f :: k -> Type)

Instances

OrdC (Some :: (k -> Type) -> Type)

Defined in Data.Parameterized.ClassesC

Methods

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

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

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

Defined in Data.Parameterized.ClassesC

Methods

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

FoldableF (Some :: (k -> Type) -> Type)

Defined in Data.Parameterized.Some

Methods

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

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

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

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

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

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

FunctorF (Some :: (k -> Type) -> Type)

Defined in Data.Parameterized.Some

Methods

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

TraversableF (Some :: (k -> Type) -> Type)

Defined in Data.Parameterized.Some

Methods

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

ShowF f => Show (Some f)

Defined in Data.Parameterized.Some

Methods

showsPrec :: Int -> Some f -> ShowS

show :: Some f -> String

showList :: [Some f] -> ShowS

TestEquality f => Eq (Some f)

Defined in Data.Parameterized.Some

Methods

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

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

OrdF f => Ord (Some f)

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

(HashableF f, TestEquality f) => Hashable (Some f)

Defined in Data.Parameterized.Some

Methods

hashWithSalt :: Int -> Some f -> Int

hash :: Some f -> Int