Algebra.Internal

Documentation

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

Methods

id :: cat a a

(.) :: cat b c -> cat a b -> cat a c

Preorder k ((:=:) k)

Methods

reflexivity :: Sing ((:=:) k) a -> eq a a

transitivity :: eq a b -> eq b c -> eq a c

Equality k ((:=:) k)

Methods

symmetry :: eq a b -> eq b a

TestEquality k ((:~:) k a)

Methods

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

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

Methods

minBound :: (k :~: a) b

maxBound :: (k :~: a) b

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

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)

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

withRefl :: (:~:) k a b -> ((~) k a b -> r) -> r

Solves equality constraint without explicit coercion. It has the same effect as gcastWith, but some hacks is done to reduce runtime overhead.

module Data.Proxy

toProxy :: a -> Proxy a

type Sized n a = Sized Vector n a

type Sized' n a = Sized Seq n a

coerceLength :: (n :~: m) -> Sized f n a -> Sized f m a

type SNat n = Sing n

sizedLength :: (ListLike (f a) a, Show (MonomorphicRep nat (Sing nat)), Integral (MonomorphicRep nat (Sing nat)), Monomorphicable nat (Sing nat), PeanoOrder nat) => Sized nat f n a -> Sing nat n

padVecs :: forall a n m. a -> Sized' n a -> Sized' m a -> (SNat (Max n m), Sized' (Max n m) a, Sized' (Max n m) a)

type family Flipped f a :: Nat -> Type where ...

Equations

Flipped f a = Flipped f a

pattern Flipped :: forall f n a. Sized f n a -> Flipped f a n

pattern OLt :: forall t. () => forall n1. (~) Bool ((:<) Nat n1 t) True => Sing Nat n1 -> Ordinal Nat t

sNatToInt :: SNat n -> Int

Orphan instances

Hashable a => Hashable (Seq a)

Methods

hashWithSalt :: Int -> Seq a -> Int

hash :: Seq a -> Int