quantification-0.5.0: Rage against the quantification

Safe HaskellNone
LanguageHaskell2010

Topaz.Types

Documentation

data Elem (rs :: [k]) (r :: k) where Source #

Constructors

ElemHere :: Elem (r ': rs) r 
ElemThere :: Elem rs r -> Elem (s ': rs) r 

data Rec :: (k -> Type) -> [k] -> Type where Source #

Constructors

RecNil :: Rec f '[] 
RecCons :: f r -> Rec f rs -> Rec f (r ': rs) 
Instances
TestCoercion f => TestCoercion (Rec f :: [k] -> Type) Source # 
Instance details

Defined in Topaz.Types

Methods

testCoercion :: Rec f a -> Rec f b -> Maybe (Coercion a b) #

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

Defined in Topaz.Types

Methods

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

MonoidForeach f => MonoidForeach (Rec f :: [k] -> Type) Source # 
Instance details

Defined in Topaz.Types

Methods

emptyForeach :: Sing a -> Rec f a Source #

BinaryForeach f => BinaryForeach (Rec f :: [k] -> Type) Source # 
Instance details

Defined in Topaz.Types

Methods

putForeach :: Sing a -> Rec f a -> Put Source #

getForeach :: Sing a -> Get (Rec f a) Source #

StorableForeach f => StorableForeach (Rec f :: [k] -> Type) Source # 
Instance details

Defined in Topaz.Types

Methods

peekForeach :: Sing a -> Ptr (Rec f a) -> IO (Rec f a) Source #

pokeForeach :: Sing a -> Ptr (Rec f a) -> Rec f a -> IO () Source #

sizeOfForeach :: Proxy (Rec f) -> Sing a -> Int Source #

SemigroupForall f => SemigroupForall (Rec f :: [k] -> Type) Source # 
Instance details

Defined in Topaz.Types

Methods

appendForall :: Rec f a -> Rec f a -> Rec f a Source #

SemigroupForeach f => SemigroupForeach (Rec f :: [k] -> Type) Source # 
Instance details

Defined in Topaz.Types

Methods

appendForeach :: Sing a -> Rec f a -> Rec f a -> Rec f a Source #

FromJSONExists f => FromJSONExists (Rec f :: [k] -> Type) Source # 
Instance details

Defined in Topaz.Types

FromJSONForeach f => FromJSONForeach (Rec f :: [k] -> Type) Source # 
Instance details

Defined in Topaz.Types

Methods

parseJSONForeach :: Sing a -> Value -> Parser (Rec f a) Source #

ToJSONForall f => ToJSONForall (Rec f :: [k] -> Type) Source # 
Instance details

Defined in Topaz.Types

Methods

toJSONForall :: Rec f a -> Value Source #

HashableForall f => HashableForall (Rec f :: [k] -> Type) Source # 
Instance details

Defined in Topaz.Types

Methods

hashWithSaltForall :: Int -> Rec f a -> Int Source #

ShowForeach f => ShowForeach (Rec f :: [k] -> Type) Source # 
Instance details

Defined in Topaz.Types

Methods

showsPrecForeach :: Sing a -> Int -> Rec f a -> ShowS Source #

ShowForall f => ShowForall (Rec f :: [k] -> Type) Source # 
Instance details

Defined in Topaz.Types

Methods

showsPrecForall :: Int -> Rec f a -> ShowS Source #

OrdForeach f => OrdForeach (Rec f :: [k] -> Type) Source # 
Instance details

Defined in Topaz.Types

Methods

compareForeach :: Sing a -> Rec f a -> Rec f a -> Ordering Source #

EqForallPoly f => EqForallPoly (Rec f :: [k] -> Type) Source # 
Instance details

Defined in Topaz.Types

Methods

eqForallPoly :: Rec f a -> Rec f b -> WitnessedEquality a b Source #

OrdForall f => OrdForall (Rec f :: [k] -> Type) Source # 
Instance details

Defined in Topaz.Types

Methods

compareForall :: Rec f a -> Rec f a -> Ordering Source #

EqForeach f => EqForeach (Rec f :: [k] -> Type) Source # 
Instance details

Defined in Topaz.Types

Methods

eqForeach :: Sing a -> Rec f a -> Rec f a -> Bool Source #

EqForall f => EqForall (Rec f :: [k] -> Type) Source # 
Instance details

Defined in Topaz.Types

Methods

eqForall :: Rec f a -> Rec f a -> Bool Source #

EqForall f => Eq (Rec f as) Source # 
Instance details

Defined in Topaz.Types

Methods

(==) :: Rec f as -> Rec f as -> Bool #

(/=) :: Rec f as -> Rec f as -> Bool #

OrdForall f => Ord (Rec f as) Source # 
Instance details

Defined in Topaz.Types

Methods

compare :: Rec f as -> Rec f as -> Ordering #

(<) :: Rec f as -> Rec f as -> Bool #

(<=) :: Rec f as -> Rec f as -> Bool #

(>) :: Rec f as -> Rec f as -> Bool #

(>=) :: Rec f as -> Rec f as -> Bool #

max :: Rec f as -> Rec f as -> Rec f as #

min :: Rec f as -> Rec f as -> Rec f as #

ShowForall f => Show (Rec f as) Source # 
Instance details

Defined in Topaz.Types

Methods

showsPrec :: Int -> Rec f as -> ShowS #

show :: Rec f as -> String #

showList :: [Rec f as] -> ShowS #

SemigroupForall f => Semigroup (Rec f as) Source # 
Instance details

Defined in Topaz.Types

Methods

(<>) :: Rec f as -> Rec f as -> Rec f as #

sconcat :: NonEmpty (Rec f as) -> Rec f as #

stimes :: Integral b => b -> Rec f as -> Rec f as #

HashableForall f => Hashable (Rec f as) Source # 
Instance details

Defined in Topaz.Types

Methods

hashWithSalt :: Int -> Rec f as -> Int #

hash :: Rec f as -> Int #

ToJSONForall f => ToJSON (Rec f as) Source # 
Instance details

Defined in Topaz.Types

Methods

toJSON :: Rec f as -> Value #

toEncoding :: Rec f as -> Encoding #

toJSONList :: [Rec f as] -> Value #

toEncodingList :: [Rec f as] -> Encoding #

(FromJSONForeach f, Reify as) => FromJSON (Rec f as) Source # 
Instance details

Defined in Topaz.Types

Methods

parseJSON :: Value -> Parser (Rec f as) #

parseJSONList :: Value -> Parser [Rec f as] #

(StorableForeach f, Reify as) => Storable (Rec f as) Source # 
Instance details

Defined in Topaz.Types

Methods

sizeOf :: Rec f as -> Int #

alignment :: Rec f as -> Int #

peekElemOff :: Ptr (Rec f as) -> Int -> IO (Rec f as) #

pokeElemOff :: Ptr (Rec f as) -> Int -> Rec f as -> IO () #

peekByteOff :: Ptr b -> Int -> IO (Rec f as) #

pokeByteOff :: Ptr b -> Int -> Rec f as -> IO () #

peek :: Ptr (Rec f as) -> IO (Rec f as) #

poke :: Ptr (Rec f as) -> Rec f as -> IO () #

data NestRec :: (k -> Type) -> Nest k -> Type where Source #

Constructors

NestRec :: Rec f rs -> Rec (NestRec f) ns -> NestRec f (Nest ns rs) 

newtype Fix f Source #

Constructors

Fix (f (Fix f)) 
Instances
Semigroup1 f => Semigroup (Fix f) Source # 
Instance details

Defined in Topaz.Types

Methods

(<>) :: Fix f -> Fix f -> Fix f #

sconcat :: NonEmpty (Fix f) -> Fix f #

stimes :: Integral b => b -> Fix f -> Fix f #

Monoid1 f => Monoid (Fix f) Source # 
Instance details

Defined in Topaz.Types

Methods

mempty :: Fix f #

mappend :: Fix f -> Fix f -> Fix f #

mconcat :: [Fix f] -> Fix f #

newtype HFix h a Source #

Constructors

HFix (h (HFix h) a) 
Instances
TestEqualityHetero h => TestEquality (HFix h :: k -> *) Source # 
Instance details

Defined in Topaz.Types

Methods

testEquality :: HFix h a -> HFix h b -> Maybe (a :~: b) #

EqHetero h => EqForall (HFix h :: k -> *) Source # 
Instance details

Defined in Topaz.Types

Methods

eqForall :: HFix h a -> HFix h a -> Bool Source #

EqHetero h => Eq (HFix h a) Source # 
Instance details

Defined in Topaz.Types

Methods

(==) :: HFix h a -> HFix h a -> Bool #

(/=) :: HFix h a -> HFix h a -> Bool #

data Nest a Source #

Constructors

Nest [Nest a] [a] 

class EqHetero h where Source #

Minimal complete definition

eqHetero

Methods

eqHetero :: (forall x. f x -> f x -> Bool) -> h f a -> h f a -> Bool Source #

class TestEqualityHetero h where Source #

Minimal complete definition

testEqualityHetero

Methods

testEqualityHetero :: (forall x y. f x -> f y -> Maybe (x :~: y)) -> h f a -> h f b -> Maybe (a :~: b) Source #

data Nat Source #

Constructors

Succ Nat 
Zero 
Instances
type Sing Source # 
Instance details

Defined in Topaz.Types

type Sing = SingNat

data SingNat :: Nat -> Type where Source #

Constructors

SingZero :: SingNat Zero 
SingSucc :: SingNat n -> SingNat (Succ n) 

data Vector :: Nat -> Type -> Type where Source #

Constructors

VectorNil :: Vector Zero a 
VectorCons :: a -> Vector n a -> Vector (Succ n) a 
Instances
Eq a => Eq (Vector n a) Source # 
Instance details

Defined in Topaz.Types

Methods

(==) :: Vector n a -> Vector n a -> Bool #

(/=) :: Vector n a -> Vector n a -> Bool #

type family (as :: [k]) ++ (bs :: [k]) :: [k] where ... infixr 5 Source #

Equations

'[] ++ bs = bs 
(a ': as) ++ bs = a ': (as ++ bs)