parameterized-utils-2.1.11.0: Classes and data structures for working with data-kind indexed types

Copyright | (c) Galois Inc 2019
Safe Haskell | None
Language | Haskell2010

Data.Parameterized.Peano

Contents

- Peano
- Basic arithmetic
- Counting
- Comparisons
- Runtime representation
- 'Some Peano'
- Properties
- Re-exports

Description

This defines a type `Peano` and `PeanoRepr` for representing a type-level natural at runtime. These type-level numbers are defined inductively instead of using GHC.TypeLits.

As a result, type-level computation defined recursively over these numbers works more smoothly. (For example, see the type-level function `Repeat` below.)

Note: as in NatRepr, in UNSAFE mode, the runtime representation of these type-level natural numbers is `Word64`.

Synopsis

- data Peano
- type Z = 'Z
- type S = 'S
- type family Plus (a :: Peano) (b :: Peano) :: Peano where ...
- type family Minus (a :: Peano) (b :: Peano) :: Peano where ...
- type family Mul (a :: Peano) (b :: Peano) :: Peano where ...
- type family Max (a :: Peano) (b :: Peano) :: Peano where ...
- type family Min (a :: Peano) (b :: Peano) :: Peano where ...
- plusP :: forall (a :: Peano) (b :: Peano). PeanoRepr a -> PeanoRepr b -> PeanoRepr (Plus a b)
- minusP :: forall (a :: Peano) (b :: Peano). PeanoRepr a -> PeanoRepr b -> PeanoRepr (Minus a b)
- mulP :: forall (a :: Peano) (b :: Peano). PeanoRepr a -> PeanoRepr b -> PeanoRepr (Mul a b)
- maxP :: forall (a :: Peano) (b :: Peano). PeanoRepr a -> PeanoRepr b -> PeanoRepr (Max a b)
- minP :: forall (a :: Peano) (b :: Peano). PeanoRepr a -> PeanoRepr b -> PeanoRepr (Min a b)
- zeroP :: PeanoRepr Z
- succP :: forall (n :: Peano). PeanoRepr n -> PeanoRepr (S n)
- predP :: forall (n :: Peano). PeanoRepr (S n) -> PeanoRepr n
- type family Repeat (m :: Peano) (f :: k -> k) (s :: k) :: k where ...
- type family CtxSizeP (ctx :: Ctx k) :: Peano where ...
- repeatP :: forall {k} (m :: Peano) repr (f :: k -> k) (s :: k). PeanoRepr m -> (forall (a :: k). repr a -> repr (f a)) -> repr s -> repr (Repeat m f s)
- ctxSizeP :: forall {k} (f :: k -> Type) (ctx :: Ctx k). Assignment f ctx -> PeanoRepr (CtxSizeP ctx)
- type family Le (a :: Peano) (b :: Peano) :: Bool where ...
- type family Lt (a :: Peano) (b :: Peano) :: Bool where ...
- type family Gt (a :: Peano) (b :: Peano) :: Bool where ...
- type family Ge (a :: Peano) (b :: Peano) :: Bool where ...
- leP :: forall (a :: Peano) (b :: Peano). PeanoRepr a -> PeanoRepr b -> BoolRepr (Le a b)
- ltP :: forall (a :: Peano) (b :: Peano). PeanoRepr a -> PeanoRepr b -> BoolRepr (Lt a b)
- gtP :: forall (a :: Peano) (b :: Peano). PeanoRepr a -> PeanoRepr b -> BoolRepr (Gt a b)
- geP :: forall (a :: Peano) (b :: Peano). PeanoRepr a -> PeanoRepr b -> BoolRepr (Ge a b)
- type KnownPeano = KnownRepr PeanoRepr
- data PeanoRepr (n :: Peano)
- data PeanoView (n :: Peano) where
  - ZRepr :: PeanoView 'Z
  - SRepr :: forall (n1 :: Peano). PeanoRepr n1 -> PeanoView ('S n1)
- peanoView :: forall (n :: Peano). PeanoRepr n -> PeanoView n
- viewRepr :: forall (n :: Peano). PeanoView n -> PeanoRepr n
- mkPeanoRepr :: Word64 -> Some PeanoRepr
- peanoValue :: PeanoRepr n -> Word64
- somePeano :: Integral a => a -> Maybe (Some PeanoRepr)
- maxPeano :: forall (m :: Peano) (n :: Peano). PeanoRepr m -> PeanoRepr n -> Some PeanoRepr
- minPeano :: forall (m :: Peano) (n :: Peano). PeanoRepr m -> PeanoRepr n -> Some PeanoRepr
- peanoLength :: [a] -> Some PeanoRepr
- plusCtxSizeAxiom :: forall {k} (t1 :: Ctx k) (t2 :: Ctx k) (f :: k -> Type). Assignment f t1 -> Assignment f t2 -> CtxSizeP (t1 <+> t2) :~: Plus (CtxSizeP t2) (CtxSizeP t1)
- minusPlusAxiom :: forall (n :: Peano) (t :: Peano) (t' :: Peano). PeanoRepr n -> PeanoRepr t -> PeanoRepr t' -> Minus n (Plus t' t) :~: Minus (Minus n t') t
- ltMinusPlusAxiom :: forall (n :: Peano) (t :: Peano) (t' :: Peano). Lt t (Minus n t') ~ 'True => PeanoRepr n -> PeanoRepr t -> PeanoRepr t' -> Lt (Plus t' t) n :~: 'True
- 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
  - Refl :: forall {k} (a :: k). a :~: a
- data Some (f :: k -> Type)

# Peano

data Peano Source #

Unary representation for natural numbers

#### Instances

Instances details

TestEquality PeanoRepr Source # |
Instance details Defined in Data.Parameterized.Peano Methods testEquality :: forall (a :: Peano) (b :: Peano). PeanoRepr a -> PeanoRepr b -> Maybe (a :~: b) Source #
EqF PeanoRepr Source # |
Instance details Defined in Data.Parameterized.Peano Methods eqF :: forall (a :: Peano). PeanoRepr a -> PeanoRepr a -> Bool Source #
HashableF PeanoRepr Source # |
Instance details Defined in Data.Parameterized.Peano Methods hashWithSaltF :: forall (tp :: Peano). Int -> PeanoRepr tp -> Int Source # hashF :: forall (tp :: Peano). PeanoRepr tp -> Int Source #
OrdF PeanoRepr Source # |

Instance details

Defined in Data.Parameterized.Peano

Methods

compareF :: forall (x :: Peano) (y :: Peano). PeanoRepr x -> PeanoRepr y -> OrderingF x y Source #

leqF :: forall (x :: Peano) (y :: Peano). PeanoRepr x -> PeanoRepr y -> Bool Source #

ltF :: forall (x :: Peano) (y :: Peano). PeanoRepr x -> PeanoRepr y -> Bool Source #

geqF :: forall (x :: Peano) (y :: Peano). PeanoRepr x -> PeanoRepr y -> Bool Source #

gtF :: forall (x :: Peano) (y :: Peano). PeanoRepr x -> PeanoRepr y -> Bool Source #

ShowF PeanoRepr Source # |
Instance details Defined in Data.Parameterized.Peano Methods withShow :: forall p q (tp :: Peano) a. p PeanoRepr -> q tp -> (Show (PeanoRepr tp) => a) -> a Source # showF :: forall (tp :: Peano). PeanoRepr tp -> String Source # showsPrecF :: forall (tp :: Peano). Int -> PeanoRepr tp -> String -> String Source #
DecidableEq PeanoRepr Source # |
Instance details Defined in Data.Parameterized.Peano Methods decEq :: forall (a :: Peano) (b :: Peano). PeanoRepr a -> PeanoRepr b -> Either (a :~: b) ((a :~: b) -> Void) Source #
IsRepr PeanoRepr Source # |
Instance details Defined in Data.Parameterized.WithRepr Methods withRepr :: forall (a :: Peano) r. PeanoRepr a -> (KnownRepr PeanoRepr a => r) -> r Source #
KnownRepr PeanoRepr Z Source # |
Instance details Defined in Data.Parameterized.Peano Methods knownRepr :: PeanoRepr Z Source #
KnownRepr PeanoRepr n => KnownRepr PeanoRepr (S n :: Peano) Source # |
Instance details Defined in Data.Parameterized.Peano Methods knownRepr :: PeanoRepr (S n) Source #

type Z = 'Z Source #

Peano zero

type S = 'S Source #

Peano successor

# Basic arithmetic

type family Plus (a :: Peano) (b :: Peano) :: Peano where ... Source #

Addition

Equations

Plus Z b = b |
Plus (S a) b = S (Plus a b) |

type family Minus (a :: Peano) (b :: Peano) :: Peano where ... Source #

Subtraction

Equations

Minus Z b = Z |
Minus (S a) (S b) = Minus a b |
Minus a Z = a |

type family Mul (a :: Peano) (b :: Peano) :: Peano where ... Source #

Multiplication

Equations

Mul Z b = Z |
Mul (S a) b = Plus a (Mul a b) |

type family Max (a :: Peano) (b :: Peano) :: Peano where ... Source #

Maximum

Equations

Max Z b = b |
Max a Z = a |
Max (S a) (S b) = S (Max a b) |

type family Min (a :: Peano) (b :: Peano) :: Peano where ... Source #

Minimum

Equations

Min Z b = Z |
Min a Z = Z |
Min (S a) (S b) = S (Min a b) |

plusP :: forall (a :: Peano) (b :: Peano). PeanoRepr a -> PeanoRepr b -> PeanoRepr (Plus a b) Source #

Addition

minusP :: forall (a :: Peano) (b :: Peano). PeanoRepr a -> PeanoRepr b -> PeanoRepr (Minus a b) Source #

Subtraction

mulP :: forall (a :: Peano) (b :: Peano). PeanoRepr a -> PeanoRepr b -> PeanoRepr (Mul a b) Source #

Multiplication

maxP :: forall (a :: Peano) (b :: Peano). PeanoRepr a -> PeanoRepr b -> PeanoRepr (Max a b) Source #

Maximum

minP :: forall (a :: Peano) (b :: Peano). PeanoRepr a -> PeanoRepr b -> PeanoRepr (Min a b) Source #

Minimum

zeroP :: PeanoRepr Z Source #

Zero

succP :: forall (n :: Peano). PeanoRepr n -> PeanoRepr (S n) Source #

Successor, Increment

predP :: forall (n :: Peano). PeanoRepr (S n) -> PeanoRepr n Source #

Get the predecessor (decrement)

# Counting

type family Repeat (m :: Peano) (f :: k -> k) (s :: k) :: k where ... Source #

Apply a constructor `f` n-times to an argument `s`

Equations

Repeat Z (f :: k -> k) (s :: k) = s |
Repeat (S m) (f :: k -> k) (s :: k) = f (Repeat m f s) |

type family CtxSizeP (ctx :: Ctx k) :: Peano where ... Source #

Calculate the size of a context

Equations

CtxSizeP ('EmptyCtx :: Ctx k) = Z |
CtxSizeP (xs '::> x :: Ctx k) = S (CtxSizeP xs) |

repeatP :: forall {k} (m :: Peano) repr (f :: k -> k) (s :: k). PeanoRepr m -> (forall (a :: k). repr a -> repr (f a)) -> repr s -> repr (Repeat m f s) Source #

Apply a constructor `f` n-times to an argument `s`

ctxSizeP :: forall {k} (f :: k -> Type) (ctx :: Ctx k). Assignment f ctx -> PeanoRepr (CtxSizeP ctx) Source #

Calculate the size of a context

# Comparisons

type family Le (a :: Peano) (b :: Peano) :: Bool where ... Source #

Less-than-or-equal

Equations

Le Z b = 'True |
Le a Z = 'False |
Le (S a) (S b) = Le a b |

type family Lt (a :: Peano) (b :: Peano) :: Bool where ... Source #

Less-than

Equations

Lt a b = Le (S a) b |

type family Gt (a :: Peano) (b :: Peano) :: Bool where ... Source #

Greater-than

Equations

Gt a b = Le b a |

type family Ge (a :: Peano) (b :: Peano) :: Bool where ... Source #

Greater-than-or-equal

Equations

Ge a b = Lt b a |

leP :: forall (a :: Peano) (b :: Peano). PeanoRepr a -> PeanoRepr b -> BoolRepr (Le a b) Source #

Less-than-or-equal-to

ltP :: forall (a :: Peano) (b :: Peano). PeanoRepr a -> PeanoRepr b -> BoolRepr (Lt a b) Source #

Less-than

gtP :: forall (a :: Peano) (b :: Peano). PeanoRepr a -> PeanoRepr b -> BoolRepr (Gt a b) Source #

Greater-than

geP :: forall (a :: Peano) (b :: Peano). PeanoRepr a -> PeanoRepr b -> BoolRepr (Ge a b) Source #

Greater-than-or-equal-to

# Runtime representation

type KnownPeano = KnownRepr PeanoRepr Source #

Implicit runtime representation

data PeanoRepr (n :: Peano) Source #

The run time value, stored as an Word64 As these are unary numbers, we don't worry about overflow.

#### Instances

Instances details

TestEquality PeanoRepr Source # |
Instance details Defined in Data.Parameterized.Peano Methods testEquality :: forall (a :: Peano) (b :: Peano). PeanoRepr a -> PeanoRepr b -> Maybe (a :~: b) Source #
EqF PeanoRepr Source # |
Instance details Defined in Data.Parameterized.Peano Methods eqF :: forall (a :: Peano). PeanoRepr a -> PeanoRepr a -> Bool Source #
HashableF PeanoRepr Source # |
Instance details Defined in Data.Parameterized.Peano Methods hashWithSaltF :: forall (tp :: Peano). Int -> PeanoRepr tp -> Int Source # hashF :: forall (tp :: Peano). PeanoRepr tp -> Int Source #
OrdF PeanoRepr Source # |

Instance details

Defined in Data.Parameterized.Peano

Methods

compareF :: forall (x :: Peano) (y :: Peano). PeanoRepr x -> PeanoRepr y -> OrderingF x y Source #

leqF :: forall (x :: Peano) (y :: Peano). PeanoRepr x -> PeanoRepr y -> Bool Source #

ltF :: forall (x :: Peano) (y :: Peano). PeanoRepr x -> PeanoRepr y -> Bool Source #

geqF :: forall (x :: Peano) (y :: Peano). PeanoRepr x -> PeanoRepr y -> Bool Source #

gtF :: forall (x :: Peano) (y :: Peano). PeanoRepr x -> PeanoRepr y -> Bool Source #

ShowF PeanoRepr Source # |
Instance details Defined in Data.Parameterized.Peano Methods withShow :: forall p q (tp :: Peano) a. p PeanoRepr -> q tp -> (Show (PeanoRepr tp) => a) -> a Source # showF :: forall (tp :: Peano). PeanoRepr tp -> String Source # showsPrecF :: forall (tp :: Peano). Int -> PeanoRepr tp -> String -> String Source #
DecidableEq PeanoRepr Source # |
Instance details Defined in Data.Parameterized.Peano Methods decEq :: forall (a :: Peano) (b :: Peano). PeanoRepr a -> PeanoRepr b -> Either (a :~: b) ((a :~: b) -> Void) Source #
IsRepr PeanoRepr Source # |
Instance details Defined in Data.Parameterized.WithRepr Methods withRepr :: forall (a :: Peano) r. PeanoRepr a -> (KnownRepr PeanoRepr a => r) -> r Source #
KnownRepr PeanoRepr Z Source # |
Instance details Defined in Data.Parameterized.Peano Methods knownRepr :: PeanoRepr Z Source #
KnownRepr PeanoRepr n => KnownRepr PeanoRepr (S n :: Peano) Source # |
Instance details Defined in Data.Parameterized.Peano Methods knownRepr :: PeanoRepr (S n) Source #
Show (PeanoRepr p) Source # |
Instance details Defined in Data.Parameterized.Peano Methods showsPrec :: Int -> PeanoRepr p -> ShowS Source # show :: PeanoRepr p -> String Source # showList :: [PeanoRepr p] -> ShowS Source #
Eq (PeanoRepr m) Source # |
Instance details Defined in Data.Parameterized.Peano Methods (==) :: PeanoRepr m -> PeanoRepr m -> Bool Source # (/=) :: PeanoRepr m -> PeanoRepr m -> Bool Source #
Hashable (PeanoRepr n) Source # |
Instance details Defined in Data.Parameterized.Peano Methods hashWithSalt :: Int -> PeanoRepr n -> Int Source # hash :: PeanoRepr n -> Int Source #
PolyEq (PeanoRepr m) (PeanoRepr n) Source # |
Instance details Defined in Data.Parameterized.Peano Methods polyEqF :: PeanoRepr m -> PeanoRepr n -> Maybe (PeanoRepr m :~: PeanoRepr n) Source # polyEq :: PeanoRepr m -> PeanoRepr n -> Bool Source #

data PeanoView (n :: Peano) where Source #

When we have optimized the runtime representation, we need to have a "view" that decomposes the representation into the standard form.

Constructors

ZRepr :: PeanoView 'Z |
SRepr :: forall (n1 :: Peano). PeanoRepr n1 -> PeanoView ('S n1) |

peanoView :: forall (n :: Peano). PeanoRepr n -> PeanoView n Source #

Test whether a number is Zero or Successor

viewRepr :: forall (n :: Peano). PeanoView n -> PeanoRepr n Source #

convert the view back to the runtime representation

# 'Some Peano'

mkPeanoRepr :: Word64 -> Some PeanoRepr Source #

Convert a `Word64` to a `PeanoRepr`

peanoValue :: PeanoRepr n -> Word64 Source #

somePeano :: Integral a => a -> Maybe (Some PeanoRepr) Source #

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

maxPeano :: forall (m :: Peano) (n :: Peano). PeanoRepr m -> PeanoRepr n -> Some PeanoRepr Source #

Return the maximum of two representations.

minPeano :: forall (m :: Peano) (n :: Peano). PeanoRepr m -> PeanoRepr n -> Some PeanoRepr Source #

Return the minimum of two representations.

peanoLength :: [a] -> Some PeanoRepr Source #

List length as a Peano number

# Properties

plusCtxSizeAxiom :: forall {k} (t1 :: Ctx k) (t2 :: Ctx k) (f :: k -> Type). Assignment f t1 -> Assignment f t2 -> CtxSizeP (t1 <+> t2) :~: Plus (CtxSizeP t2) (CtxSizeP t1) Source #

Context size commutes with context append

minusPlusAxiom :: forall (n :: Peano) (t :: Peano) (t' :: Peano). PeanoRepr n -> PeanoRepr t -> PeanoRepr t' -> Minus n (Plus t' t) :~: Minus (Minus n t') t Source #

Minus distributes over plus

ltMinusPlusAxiom :: forall (n :: Peano) (t :: Peano) (t' :: Peano). Lt t (Minus n t') ~ 'True => PeanoRepr n -> PeanoRepr t -> PeanoRepr t' -> Lt (Plus t' t) n :~: 'True Source #

We can reshuffle minus with less than

# Re-exports

class TestEquality (f :: k -> Type) where Source #

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) Source #

Conditionally prove the equality of `a` and `b`.

#### Instances

Instances details

TestEquality SNat | Since: base-4.18.0.0
Instance details Defined in GHC.Internal.TypeNats Methods testEquality :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> Maybe (a :~: b) Source #
TestEquality NatRepr Source # |
Instance details Defined in Data.Parameterized.NatRepr.Internal Methods testEquality :: forall (a :: Nat) (b :: Nat). NatRepr a -> NatRepr b -> Maybe (a :~: b) Source #
TestEquality PeanoRepr Source # |
Instance details Defined in Data.Parameterized.Peano Methods testEquality :: forall (a :: Peano) (b :: Peano). PeanoRepr a -> PeanoRepr b -> Maybe (a :~: b) Source #
TestEquality BoolRepr Source # |
Instance details Defined in Data.Parameterized.BoolRepr Methods testEquality :: forall (a :: Bool) (b :: Bool). BoolRepr a -> BoolRepr b -> Maybe (a :~: b) Source #
TestEquality SChar | Since: base-4.18.0.0
Instance details Defined in GHC.Internal.TypeLits Methods testEquality :: forall (a :: Char) (b :: Char). SChar a -> SChar b -> Maybe (a :~: b) Source #
TestEquality SSymbol | Since: base-4.18.0.0
Instance details Defined in GHC.Internal.TypeLits Methods testEquality :: forall (a :: Symbol) (b :: Symbol). SSymbol a -> SSymbol b -> Maybe (a :~: b) Source #
TestEquality SymbolRepr Source # |
Instance details Defined in Data.Parameterized.SymbolRepr Methods testEquality :: forall (a :: Symbol) (b :: Symbol). SymbolRepr a -> SymbolRepr b -> Maybe (a :~: b) Source #
TestEquality (TypeRep :: k -> Type) |
Instance details Defined in GHC.Internal.Data.Typeable.Internal Methods testEquality :: forall (a :: k) (b :: k). TypeRep a -> TypeRep b -> Maybe (a :~: b) Source #
TestEquality (Nonce :: k -> Type) Source # |
Instance details Defined in Data.Parameterized.Nonce.Unsafe Methods testEquality :: forall (a :: k) (b :: k). Nonce a -> Nonce b -> Maybe (a :~: b) Source #
TestEquality ((:~:) a :: k -> Type) | Since: base-4.7.0.0
Instance details Defined in GHC.Internal.Data.Type.Equality Methods testEquality :: forall (a0 :: k) (b :: k). (a :~: a0) -> (a :~: b) -> Maybe (a0 :~: b) Source #
TestEquality (Index ctx :: k -> Type) Source # |
Instance details Defined in Data.Parameterized.Context.Unsafe Methods testEquality :: forall (a :: k) (b :: k). Index ctx a -> Index ctx b -> Maybe (a :~: b) Source #
TestEquality (Index l :: k -> Type) Source # |
Instance details Defined in Data.Parameterized.List Methods testEquality :: forall (a :: k) (b :: k). Index l a -> Index l b -> Maybe (a :~: b) Source #
TestEquality (Nonce s :: k -> Type) Source # |
Instance details Defined in Data.Parameterized.Nonce Methods testEquality :: forall (a :: k) (b :: k). Nonce s a -> Nonce s b -> Maybe (a :~: b) Source #
TestEquality ((:~~:) a :: k -> Type) | Since: base-4.10.0.0
Instance details Defined in GHC.Internal.Data.Type.Equality Methods testEquality :: forall (a0 :: k) (b :: k). (a :~~: a0) -> (a :~~: b) -> Maybe (a0 :~: b) Source #
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 :: k2) (b :: k2). Compose f g a -> Compose f g b -> Maybe (a :~: b) Source #
TestEquality f => TestEquality (Assignment f :: Ctx k -> Type) Source # |
Instance details Defined in Data.Parameterized.Context.Unsafe Methods testEquality :: forall (a :: Ctx k) (b :: Ctx k). Assignment f a -> Assignment f b -> Maybe (a :~: b) Source #
TestEquality f => TestEquality (List f :: [k] -> Type) Source # |
Instance details Defined in Data.Parameterized.List Methods testEquality :: forall (a :: [k]) (b :: [k]). List f a -> List f b -> Maybe (a :~: b) Source #
(TestEquality f, TestEquality g) => TestEquality (PairRepr f g :: (k1, k2) -> Type) Source # |
Instance details Defined in Data.Parameterized.DataKind Methods testEquality :: forall (a :: (k1, k2)) (b :: (k1, k2)). PairRepr f g a -> PairRepr f g b -> Maybe (a :~: b) Source #

data (a :: k) :~: (b :: k) where infix 4 Source #

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 GHC.Internal.Control.Category Methods id :: forall (a :: k). a :~: a Source # (.) :: forall (b :: k) (c :: k) (a :: k). (b :~: c) -> (a :~: b) -> a :~: c Source #
TestEquality ((:~:) a :: k -> Type) | Since: base-4.7.0.0
Instance details Defined in GHC.Internal.Data.Type.Equality Methods testEquality :: forall (a0 :: k) (b :: k). (a :~: a0) -> (a :~: b) -> Maybe (a0 :~: b) Source #
NFData2 ((:~:) :: Type -> Type -> Type) | Since: deepseq-1.4.3.0
Instance details Defined in Control.DeepSeq Methods liftRnf2 :: (a -> ()) -> (b -> ()) -> (a :~: b) -> () Source #
NFData1 ((:~:) a) | Since: deepseq-1.4.3.0
Instance details Defined in Control.DeepSeq Methods liftRnf :: (a0 -> ()) -> (a :~: a0) -> () Source #
NFData (a :~: b) | Since: deepseq-1.4.3.0
Instance details Defined in Control.DeepSeq Methods rnf :: (a :~: b) -> () Source #
(a ~ b, Data a) => Data (a :~: b) | Since: base-4.7.0.0

Instance details

Defined in GHC.Internal.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) Source #

gunfold :: (forall b0 r. Data b0 => c (b0 -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (a :~: b) Source #

toConstr :: (a :~: b) -> Constr Source #

dataTypeOf :: (a :~: b) -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (a :~: b)) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (a :~: b)) Source #

gmapT :: (forall b0. Data b0 => b0 -> b0) -> (a :~: b) -> a :~: b Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> (a :~: b) -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> (a :~: b) -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> (a :~: b) -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> (a :~: b) -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b) Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b) Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b) Source #

a ~ b => Bounded (a :~: b) | Since: base-4.7.0.0
Instance details Defined in GHC.Internal.Data.Type.Equality Methods minBound :: a :~: b Source # maxBound :: a :~: b Source #
a ~ b => Enum (a :~: b) | Since: base-4.7.0.0

Instance details

Defined in GHC.Internal.Data.Type.Equality

Methods

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

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

toEnum :: Int -> a :~: b Source #

fromEnum :: (a :~: b) -> Int Source #

enumFrom :: (a :~: b) -> [a :~: b] Source #

enumFromThen :: (a :~: b) -> (a :~: b) -> [a :~: b] Source #

enumFromTo :: (a :~: b) -> (a :~: b) -> [a :~: b] Source #

enumFromThenTo :: (a :~: b) -> (a :~: b) -> (a :~: b) -> [a :~: b] Source #

a ~ b => Read (a :~: b) | Since: base-4.7.0.0
Instance details Defined in GHC.Internal.Data.Type.Equality Methods readsPrec :: Int -> ReadS (a :~: b) Source # readList :: ReadS [a :~: b] Source # readPrec :: ReadPrec (a :~: b) Source # readListPrec :: ReadPrec [a :~: b] Source #
Show (a :~: b) | Since: base-4.7.0.0
Instance details Defined in GHC.Internal.Data.Type.Equality Methods showsPrec :: Int -> (a :~: b) -> ShowS Source # show :: (a :~: b) -> String Source # showList :: [a :~: b] -> ShowS Source #
Eq (a :~: b) | Since: base-4.7.0.0
Instance details Defined in GHC.Internal.Data.Type.Equality Methods (==) :: (a :~: b) -> (a :~: b) -> Bool Source # (/=) :: (a :~: b) -> (a :~: b) -> Bool Source #
Ord (a :~: b) | Since: base-4.7.0.0

Instance details

Defined in GHC.Internal.Data.Type.Equality

Methods

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

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

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

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

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

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

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

HasDict (a ~ b) (a :~: b) |
Instance details Defined in Data.Constraint Methods evidence :: (a :~: b) -> Dict (a ~ b) Source #

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

#### Instances

Instances details

OrdC (Some :: (k -> Type) -> Type) Source # |
Instance details Defined in Data.Parameterized.ClassesC Methods compareC :: (forall (x :: k) (y :: k). 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 :: k) (y :: k). f x -> f y -> Maybe (x :~: y)) -> Some f -> Some f -> Bool Source #
FoldableF (Some :: (k -> Type) -> Type) Source # |

Instance details

Defined in Data.Parameterized.Some

Methods

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

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

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

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

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

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

FunctorF (Some :: (k -> Type) -> Type) Source # |
Instance details Defined in Data.Parameterized.Some Methods fmapF :: (forall (x :: k). f x -> g x) -> Some f -> Some g Source #
TraversableF (Some :: (k -> Type) -> Type) Source # |
Instance details Defined in Data.Parameterized.Some Methods traverseF :: Applicative m => (forall (s :: k). e s -> m (f s)) -> Some e -> m (Some f) Source #
ShowF f => Show (Some f) Source # |
Instance details Defined in Data.Parameterized.Some Methods showsPrec :: Int -> Some f -> ShowS Source # show :: Some f -> String Source # showList :: [Some f] -> ShowS Source #
TestEquality f => Eq (Some f) Source # |
Instance details Defined in Data.Parameterized.Some Methods (==) :: Some f -> Some f -> Bool Source # (/=) :: Some f -> Some f -> Bool Source #
OrdF f => Ord (Some f) Source # |
Instance details Defined in Data.Parameterized.Some Methods compare :: Some f -> Some f -> Ordering Source # (<) :: Some f -> Some f -> Bool Source # (<=) :: Some f -> Some f -> Bool Source # (>) :: Some f -> Some f -> Bool Source # (>=) :: Some f -> Some f -> Bool Source # max :: Some f -> Some f -> Some f Source # min :: Some f -> Some f -> Some f Source #
(HashableF f, TestEquality f) => Hashable (Some f) Source # |
Instance details Defined in Data.Parameterized.Some Methods hashWithSalt :: Int -> Some f -> Int Source # hash :: Some f -> Int Source #