Data.Kind.Extra

Kind-level utilities to guide and simplify programming at the type level

Documentation

data A :: forall foo. foo -> Type where

A symbolic type, i.e. a wrapper around a (poly kinded) type to be produced by Eval instances.

All data types, e.g. data Point2 x y :: Type can be made into /symbolic representations of other types, by adding a symbolic/ type parameter: data Point2 x y :: A Vec2 -> Type.

Complete example:

data PrettyPrinter c where
  RenderText :: Symbol -> PrettyPrinter Symbol
  WithColor :: Color -> PrettyPrinter c -> PrettyPrinter c

data Color = Black | White

data ColoredText :: Color -> Symbol -> IsA (PrettyPrinter Symbol)

type instance Eval (ColoredText c txt) = 'WithColor c ('RenderText txt)

Constructors

MkA :: A foo

Instances

BitStringBuilderHoley (Proxy (A Type (BitRecordField Bool * Bool 1 MkFieldFlag) -> Type) (MkField Bool * Bool 1 MkFieldFlag)) a

Associated Types

type ToBitStringBuilder (Proxy (A Type (BitRecordField Bool * Bool 1 MkFieldFlag) -> Type) (MkField Bool * Bool 1 MkFieldFlag)) a :: *

Methods

bitStringBuilderHoley :: Proxy (A Type (BitRecordField Bool * Bool 1 MkFieldFlag) -> Type) (MkField Bool * Bool 1 MkFieldFlag) -> Holey BitStringBuilder a (ToBitStringBuilder (Proxy (A Type (BitRecordField Bool * Bool 1 MkFieldFlag) -> Type) (MkField Bool * Bool 1 MkFieldFlag)) a)

BitStringBuilderHoley (Proxy (A Type (BitRecordField Int8 * SignedNat 8 MkFieldI8) -> Type) (MkField Int8 * SignedNat 8 MkFieldI8)) a

Associated Types

type ToBitStringBuilder (Proxy (A Type (BitRecordField Int8 * SignedNat 8 MkFieldI8) -> Type) (MkField Int8 * SignedNat 8 MkFieldI8)) a :: *

Methods

bitStringBuilderHoley :: Proxy (A Type (BitRecordField Int8 * SignedNat 8 MkFieldI8) -> Type) (MkField Int8 * SignedNat 8 MkFieldI8) -> Holey BitStringBuilder a (ToBitStringBuilder (Proxy (A Type (BitRecordField Int8 * SignedNat 8 MkFieldI8) -> Type) (MkField Int8 * SignedNat 8 MkFieldI8)) a)

BitStringBuilderHoley (Proxy (A Type (BitRecordField Int16 * SignedNat 16 MkFieldI16) -> Type) (MkField Int16 * SignedNat 16 MkFieldI16)) a

Associated Types

type ToBitStringBuilder (Proxy (A Type (BitRecordField Int16 * SignedNat 16 MkFieldI16) -> Type) (MkField Int16 * SignedNat 16 MkFieldI16)) a :: *

Methods

bitStringBuilderHoley :: Proxy (A Type (BitRecordField Int16 * SignedNat 16 MkFieldI16) -> Type) (MkField Int16 * SignedNat 16 MkFieldI16) -> Holey BitStringBuilder a (ToBitStringBuilder (Proxy (A Type (BitRecordField Int16 * SignedNat 16 MkFieldI16) -> Type) (MkField Int16 * SignedNat 16 MkFieldI16)) a)

BitStringBuilderHoley (Proxy (A Type (BitRecordField Int32 * SignedNat 32 MkFieldI32) -> Type) (MkField Int32 * SignedNat 32 MkFieldI32)) a

Associated Types

type ToBitStringBuilder (Proxy (A Type (BitRecordField Int32 * SignedNat 32 MkFieldI32) -> Type) (MkField Int32 * SignedNat 32 MkFieldI32)) a :: *

Methods

bitStringBuilderHoley :: Proxy (A Type (BitRecordField Int32 * SignedNat 32 MkFieldI32) -> Type) (MkField Int32 * SignedNat 32 MkFieldI32) -> Holey BitStringBuilder a (ToBitStringBuilder (Proxy (A Type (BitRecordField Int32 * SignedNat 32 MkFieldI32) -> Type) (MkField Int32 * SignedNat 32 MkFieldI32)) a)

BitStringBuilderHoley (Proxy (A Type (BitRecordField Int64 * SignedNat 64 MkFieldI64) -> Type) (MkField Int64 * SignedNat 64 MkFieldI64)) a

Associated Types

type ToBitStringBuilder (Proxy (A Type (BitRecordField Int64 * SignedNat 64 MkFieldI64) -> Type) (MkField Int64 * SignedNat 64 MkFieldI64)) a :: *

Methods

bitStringBuilderHoley :: Proxy (A Type (BitRecordField Int64 * SignedNat 64 MkFieldI64) -> Type) (MkField Int64 * SignedNat 64 MkFieldI64) -> Holey BitStringBuilder a (ToBitStringBuilder (Proxy (A Type (BitRecordField Int64 * SignedNat 64 MkFieldI64) -> Type) (MkField Int64 * SignedNat 64 MkFieldI64)) a)

BitStringBuilderHoley (Proxy (A Type (BitRecordField Word8 * Nat 8 MkFieldU8) -> Type) (MkField Word8 * Nat 8 MkFieldU8)) a

Associated Types

type ToBitStringBuilder (Proxy (A Type (BitRecordField Word8 * Nat 8 MkFieldU8) -> Type) (MkField Word8 * Nat 8 MkFieldU8)) a :: *

Methods

bitStringBuilderHoley :: Proxy (A Type (BitRecordField Word8 * Nat 8 MkFieldU8) -> Type) (MkField Word8 * Nat 8 MkFieldU8) -> Holey BitStringBuilder a (ToBitStringBuilder (Proxy (A Type (BitRecordField Word8 * Nat 8 MkFieldU8) -> Type) (MkField Word8 * Nat 8 MkFieldU8)) a)

BitStringBuilderHoley (Proxy (A Type (BitRecordField Word16 * Nat 16 MkFieldU16) -> Type) (MkField Word16 * Nat 16 MkFieldU16)) a

Associated Types

type ToBitStringBuilder (Proxy (A Type (BitRecordField Word16 * Nat 16 MkFieldU16) -> Type) (MkField Word16 * Nat 16 MkFieldU16)) a :: *

Methods

bitStringBuilderHoley :: Proxy (A Type (BitRecordField Word16 * Nat 16 MkFieldU16) -> Type) (MkField Word16 * Nat 16 MkFieldU16) -> Holey BitStringBuilder a (ToBitStringBuilder (Proxy (A Type (BitRecordField Word16 * Nat 16 MkFieldU16) -> Type) (MkField Word16 * Nat 16 MkFieldU16)) a)

BitStringBuilderHoley (Proxy (A Type (BitRecordField Word32 * Nat 32 MkFieldU32) -> Type) (MkField Word32 * Nat 32 MkFieldU32)) a

Associated Types

type ToBitStringBuilder (Proxy (A Type (BitRecordField Word32 * Nat 32 MkFieldU32) -> Type) (MkField Word32 * Nat 32 MkFieldU32)) a :: *

Methods

bitStringBuilderHoley :: Proxy (A Type (BitRecordField Word32 * Nat 32 MkFieldU32) -> Type) (MkField Word32 * Nat 32 MkFieldU32) -> Holey BitStringBuilder a (ToBitStringBuilder (Proxy (A Type (BitRecordField Word32 * Nat 32 MkFieldU32) -> Type) (MkField Word32 * Nat 32 MkFieldU32)) a)

BitStringBuilderHoley (Proxy (A Type (BitRecordField Word64 * Nat 64 MkFieldU64) -> Type) (MkField Word64 * Nat 64 MkFieldU64)) a

Associated Types

type ToBitStringBuilder (Proxy (A Type (BitRecordField Word64 * Nat 64 MkFieldU64) -> Type) (MkField Word64 * Nat 64 MkFieldU64)) a :: *

Methods

bitStringBuilderHoley :: Proxy (A Type (BitRecordField Word64 * Nat 64 MkFieldU64) -> Type) (MkField Word64 * Nat 64 MkFieldU64) -> Holey BitStringBuilder a (ToBitStringBuilder (Proxy (A Type (BitRecordField Word64 * Nat 64 MkFieldU64) -> Type) (MkField Word64 * Nat 64 MkFieldU64)) a)

(KnownNat v, BitStringBuilderHoley (Proxy (IsA Type (BitRecordField rt * SignedNat size t)) f) a, (~) * (ToBitStringBuilder (Proxy (IsA Type (BitRecordField rt * SignedNat size t)) f) a) (x -> a), Num x) => BitStringBuilderHoley (Proxy (A Type (BitRecordField rt * SignedNat size t) -> Type) ((:=) rt size SignedNat t f (NegativeNat v))) a

Associated Types

type ToBitStringBuilder (Proxy (A Type (BitRecordField rt * SignedNat size t) -> Type) ((:=) rt size SignedNat t f (NegativeNat v))) a :: *

Methods

bitStringBuilderHoley :: Proxy (A Type (BitRecordField rt * SignedNat size t) -> Type) ((rt := size) SignedNat t f (NegativeNat v)) -> Holey BitStringBuilder a (ToBitStringBuilder (Proxy (A Type (BitRecordField rt * SignedNat size t) -> Type) ((rt := size) SignedNat t f (NegativeNat v))) a)

(KnownNat v, BitStringBuilderHoley (Proxy (IsA Type (BitRecordField rt * SignedNat size t)) f) a, (~) * (ToBitStringBuilder (Proxy (IsA Type (BitRecordField rt * SignedNat size t)) f) a) (x -> a), Num x) => BitStringBuilderHoley (Proxy (A Type (BitRecordField rt * SignedNat size t) -> Type) ((:=) rt size SignedNat t f (PositiveNat v))) a

Associated Types

type ToBitStringBuilder (Proxy (A Type (BitRecordField rt * SignedNat size t) -> Type) ((:=) rt size SignedNat t f (PositiveNat v))) a :: *

Methods

bitStringBuilderHoley :: Proxy (A Type (BitRecordField rt * SignedNat size t) -> Type) ((rt := size) SignedNat t f (PositiveNat v)) -> Holey BitStringBuilder a (ToBitStringBuilder (Proxy (A Type (BitRecordField rt * SignedNat size t) -> Type) ((rt := size) SignedNat t f (PositiveNat v))) a)

(KnownNat v, BitStringBuilderHoley (Proxy (IsA Type (BitRecordField rt * Nat len t)) f) a, (~) * (ToBitStringBuilder (Proxy (IsA Type (BitRecordField rt * Nat len t)) f) a) (rt -> a), Num rt) => BitStringBuilderHoley (Proxy (A Type (BitRecordField rt * Nat len t) -> Type) ((:=) rt len Nat t f v)) a

Associated Types

type ToBitStringBuilder (Proxy (A Type (BitRecordField rt * Nat len t) -> Type) ((:=) rt len Nat t f v)) a :: *

Methods

bitStringBuilderHoley :: Proxy (A Type (BitRecordField rt * Nat len t) -> Type) ((rt := len) Nat t f v) -> Holey BitStringBuilder a (ToBitStringBuilder (Proxy (A Type (BitRecordField rt * Nat len t) -> Type) ((rt := len) Nat t f v)) a)

(~) Nat (BitRecordFieldSize rt * Bool size t f) 1 => BitStringBuilderHoley (Proxy (A Type (BitRecordField rt * Bool size t) -> Type) ((:=) rt size Bool t f False)) a

Associated Types

type ToBitStringBuilder (Proxy (A Type (BitRecordField rt * Bool size t) -> Type) ((:=) rt size Bool t f False)) a :: *

Methods

bitStringBuilderHoley :: Proxy (A Type (BitRecordField rt * Bool size t) -> Type) ((rt := size) Bool t f False) -> Holey BitStringBuilder a (ToBitStringBuilder (Proxy (A Type (BitRecordField rt * Bool size t) -> Type) ((rt := size) Bool t f False)) a)

(~) Nat (BitRecordFieldSize rt * Bool size t f) 1 => BitStringBuilderHoley (Proxy (A Type (BitRecordField rt * Bool size t) -> Type) ((:=) rt size Bool t f True)) a

Associated Types

type ToBitStringBuilder (Proxy (A Type (BitRecordField rt * Bool size t) -> Type) ((:=) rt size Bool t f True)) a :: *

Methods

bitStringBuilderHoley :: Proxy (A Type (BitRecordField rt * Bool size t) -> Type) ((rt := size) Bool t f True) -> Holey BitStringBuilder a (ToBitStringBuilder (Proxy (A Type (BitRecordField rt * Bool size t) -> Type) ((rt := size) Bool t f True)) a)

BitStringBuilderHoley (Proxy (IsA Type (BitRecordField rt k st len t)) nested) a => BitStringBuilderHoley (Proxy (A Type (BitRecordField rt k st len t) -> Type) (LabelF rt k st len t l nested)) a

Associated Types

type ToBitStringBuilder (Proxy (A Type (BitRecordField rt k st len t) -> Type) (LabelF rt k st len t l nested)) a :: *

Methods

bitStringBuilderHoley :: Proxy (A Type (BitRecordField rt k st len t) -> Type) (LabelF rt k st len t l nested) -> Holey BitStringBuilder a (ToBitStringBuilder (Proxy (A Type (BitRecordField rt k st len t) -> Type) (LabelF rt k st len t l nested)) a)

KnownChunkSize s => BitStringBuilderHoley (Proxy (A Type (BitRecordField (B s) * Nat s (MkFieldBits s)) -> Type) (MkField (B s) * Nat s (MkFieldBits s))) a

Associated Types

type ToBitStringBuilder (Proxy (A Type (BitRecordField (B s) * Nat s (MkFieldBits s)) -> Type) (MkField (B s) * Nat s (MkFieldBits s))) a :: *

Methods

bitStringBuilderHoley :: Proxy (A Type (BitRecordField (B s) * Nat s (MkFieldBits s)) -> Type) (MkField (B s) * Nat s (MkFieldBits s)) -> Holey BitStringBuilder a (ToBitStringBuilder (Proxy (A Type (BitRecordField (B s) * Nat s (MkFieldBits s)) -> Type) (MkField (B s) * Nat s (MkFieldBits s))) a)

KnownChunkSize size => BitStringBuilderHoley (Proxy (A Type (BitRecordField (EnumValue e) * e size (MkFieldCustom * (EnumValue e) e size)) -> Type) (MkField (EnumValue e) * e size (MkFieldCustom * (EnumValue e) e size))) r

Associated Types

type ToBitStringBuilder (Proxy (A Type (BitRecordField (EnumValue e) * e size (MkFieldCustom * (EnumValue e) e size)) -> Type) (MkField (EnumValue e) * e size (MkFieldCustom * (EnumValue e) e size))) r :: *

Methods

bitStringBuilderHoley :: Proxy (A Type (BitRecordField (EnumValue e) * e size (MkFieldCustom * (EnumValue e) e size)) -> Type) (MkField (EnumValue e) * e size (MkFieldCustom * (EnumValue e) e size)) -> Holey BitStringBuilder r (ToBitStringBuilder (Proxy (A Type (BitRecordField (EnumValue e) * e size (MkFieldCustom * (EnumValue e) e size)) -> Type) (MkField (EnumValue e) * e size (MkFieldCustom * (EnumValue e) e size))) r)

(KnownNat (FromEnum e v), KnownChunkSize size) => BitStringBuilderHoley (Proxy (A Type (BitRecordField (EnumValue e) * e size (MkFieldCustom * (EnumValue e) e size)) -> Type) ((:=) (EnumValue e) size e (MkFieldCustom * (EnumValue e) e size) f v)) r

Associated Types

type ToBitStringBuilder (Proxy (A Type (BitRecordField (EnumValue e) * e size (MkFieldCustom * (EnumValue e) e size)) -> Type) ((:=) (EnumValue e) size e (MkFieldCustom * (EnumValue e) e size) f v)) r :: *

Methods

bitStringBuilderHoley :: Proxy (A Type (BitRecordField (EnumValue e) * e size (MkFieldCustom * (EnumValue e) e size)) -> Type) ((EnumValue e := size) e (MkFieldCustom * (EnumValue e) e size) f v) -> Holey BitStringBuilder r (ToBitStringBuilder (Proxy (A Type (BitRecordField (EnumValue e) * e size (MkFieldCustom * (EnumValue e) e size)) -> Type) ((EnumValue e := size) e (MkFieldCustom * (EnumValue e) e size) f v)) r)

BitStringBuilderHoley (Proxy BitRecord (Eval BitRecord r)) a => BitStringBuilderHoley (Proxy (IsA * BitRecord) r) a

Associated Types

type ToBitStringBuilder (Proxy (IsA * BitRecord) r) a :: *

Methods

bitStringBuilderHoley :: Proxy (IsA * BitRecord) r -> Holey BitStringBuilder a (ToBitStringBuilder (Proxy (IsA * BitRecord) r) a)

type ($~) foo (IsA k b) (Fun1 k b foo f) x

type ($~) foo (IsA k b) (Fun1 k b foo f) x = f x

type ($~) foo (IsA * ((:->) Type * a (IsA k b))) (Fun2 k b a foo f) x

type ($~) foo (IsA * ((:->) Type * a (IsA k b))) (Fun2 k b a foo f) x = Fun1 k b a (f x)

type ($~) foo (IsA * ((:->) Type * a (IsA * ((:->) Type * b (IsA k c))))) (Fun3 k c b a foo f) x

type ($~) foo (IsA * ((:->) Type * a (IsA * ((:->) Type * b (IsA k c))))) (Fun3 k c b a foo f) x = Fun2 k c b a (f x)

type ($~) foo (IsA * ((:->) Type * a (IsA * ((:->) Type * b (IsA * ((:->) Type * c (IsAn k d))))))) (Fun4 k d c b a foo f) x

type ($~) foo (IsA * ((:->) Type * a (IsA * ((:->) Type * b (IsA * ((:->) Type * c (IsAn k d))))))) (Fun4 k d c b a foo f) x = Fun3 k d c b a (f x)

type ($~) foo (IsA * o) ((:>>>^:) * o * foo * bar f g) x

type ($~) foo (IsA * o) ((:>>>^:) * o * foo * bar f g) x = Return o (($~) bar o g (($~) foo bar f x))

type Eval BitRecord (MaybeField rt k st len t (Nothing (IsA Type (BitRecordField rt k st len t))))

type Eval BitRecord (MaybeField rt k st len t (Nothing (IsA Type (BitRecordField rt k st len t)))) = EmptyBitRecord

type Eval BitRecord (MaybeField rt k st len t (Just (IsA Type (BitRecordField rt k st len t)) fld))

type Eval BitRecord (MaybeField rt k st len t (Just (IsA Type (BitRecordField rt k st len t)) fld)) = BitRecordMember rt k st len t fld

type ($~) (Maybe s) (IsA k t) (Optional s k t fallback f) (Nothing s)

type ($~) (Maybe s) (IsA k t) (Optional s k t fallback f) (Nothing s) = fallback

type ($~) (Maybe foo) (IsA k t) (Optional foo k t fallback f) (Just foo s)

type ($~) (Maybe foo) (IsA k t) (Optional foo k t fallback f) (Just foo s) = ($~) foo (IsA k t) f s

type ToPretty (IsA Type (BitRecordField rt Type st size t)) f

type ToPretty (IsA Type (BitRecordField rt Type st size t)) f = PrettyField rt st size t f

type ToBitStringBuilder (Proxy (A Type (BitRecordField Bool * Bool 1 MkFieldFlag) -> Type) (MkField Bool * Bool 1 MkFieldFlag)) a

type ToBitStringBuilder (Proxy (A Type (BitRecordField Bool * Bool 1 MkFieldFlag) -> Type) (MkField Bool * Bool 1 MkFieldFlag)) a = Bool -> a

type ToBitStringBuilder (Proxy (A Type (BitRecordField Int8 * SignedNat 8 MkFieldI8) -> Type) (MkField Int8 * SignedNat 8 MkFieldI8)) a

type ToBitStringBuilder (Proxy (A Type (BitRecordField Int8 * SignedNat 8 MkFieldI8) -> Type) (MkField Int8 * SignedNat 8 MkFieldI8)) a = Int8 -> a

type ToBitStringBuilder (Proxy (A Type (BitRecordField Int16 * SignedNat 16 MkFieldI16) -> Type) (MkField Int16 * SignedNat 16 MkFieldI16)) a

type ToBitStringBuilder (Proxy (A Type (BitRecordField Int16 * SignedNat 16 MkFieldI16) -> Type) (MkField Int16 * SignedNat 16 MkFieldI16)) a = Int16 -> a

type ToBitStringBuilder (Proxy (A Type (BitRecordField Int32 * SignedNat 32 MkFieldI32) -> Type) (MkField Int32 * SignedNat 32 MkFieldI32)) a

type ToBitStringBuilder (Proxy (A Type (BitRecordField Int32 * SignedNat 32 MkFieldI32) -> Type) (MkField Int32 * SignedNat 32 MkFieldI32)) a = Int32 -> a

type ToBitStringBuilder (Proxy (A Type (BitRecordField Int64 * SignedNat 64 MkFieldI64) -> Type) (MkField Int64 * SignedNat 64 MkFieldI64)) a

type ToBitStringBuilder (Proxy (A Type (BitRecordField Int64 * SignedNat 64 MkFieldI64) -> Type) (MkField Int64 * SignedNat 64 MkFieldI64)) a = Int64 -> a

type ToBitStringBuilder (Proxy (A Type (BitRecordField Word8 * Nat 8 MkFieldU8) -> Type) (MkField Word8 * Nat 8 MkFieldU8)) a

type ToBitStringBuilder (Proxy (A Type (BitRecordField Word8 * Nat 8 MkFieldU8) -> Type) (MkField Word8 * Nat 8 MkFieldU8)) a = Word8 -> a

type ToBitStringBuilder (Proxy (A Type (BitRecordField Word16 * Nat 16 MkFieldU16) -> Type) (MkField Word16 * Nat 16 MkFieldU16)) a

type ToBitStringBuilder (Proxy (A Type (BitRecordField Word16 * Nat 16 MkFieldU16) -> Type) (MkField Word16 * Nat 16 MkFieldU16)) a = Word16 -> a

type ToBitStringBuilder (Proxy (A Type (BitRecordField Word32 * Nat 32 MkFieldU32) -> Type) (MkField Word32 * Nat 32 MkFieldU32)) a

type ToBitStringBuilder (Proxy (A Type (BitRecordField Word32 * Nat 32 MkFieldU32) -> Type) (MkField Word32 * Nat 32 MkFieldU32)) a = Word32 -> a

type ToBitStringBuilder (Proxy (A Type (BitRecordField Word64 * Nat 64 MkFieldU64) -> Type) (MkField Word64 * Nat 64 MkFieldU64)) a

type ToBitStringBuilder (Proxy (A Type (BitRecordField Word64 * Nat 64 MkFieldU64) -> Type) (MkField Word64 * Nat 64 MkFieldU64)) a = Word64 -> a

type ToBitStringBuilder (Proxy (A Type (BitRecordField rt * SignedNat size t) -> Type) ((:=) rt size SignedNat t f (NegativeNat v))) a

type ToBitStringBuilder (Proxy (A Type (BitRecordField rt * SignedNat size t) -> Type) ((:=) rt size SignedNat t f (NegativeNat v))) a = a

type ToBitStringBuilder (Proxy (A Type (BitRecordField rt * SignedNat size t) -> Type) ((:=) rt size SignedNat t f (PositiveNat v))) a

type ToBitStringBuilder (Proxy (A Type (BitRecordField rt * SignedNat size t) -> Type) ((:=) rt size SignedNat t f (PositiveNat v))) a = a

type ToBitStringBuilder (Proxy (A Type (BitRecordField rt * Nat len t) -> Type) ((:=) rt len Nat t f v)) a

type ToBitStringBuilder (Proxy (A Type (BitRecordField rt * Nat len t) -> Type) ((:=) rt len Nat t f v)) a = a

type ToBitStringBuilder (Proxy (A Type (BitRecordField rt * Bool size t) -> Type) ((:=) rt size Bool t f False)) a

type ToBitStringBuilder (Proxy (A Type (BitRecordField rt * Bool size t) -> Type) ((:=) rt size Bool t f False)) a = a

type ToBitStringBuilder (Proxy (A Type (BitRecordField rt * Bool size t) -> Type) ((:=) rt size Bool t f True)) a

type ToBitStringBuilder (Proxy (A Type (BitRecordField rt * Bool size t) -> Type) ((:=) rt size Bool t f True)) a = a

type ToBitStringBuilder (Proxy (A Type (BitRecordField rt k st len t) -> Type) (LabelF rt k st len t l nested)) a

type ToBitStringBuilder (Proxy (A Type (BitRecordField rt k st len t) -> Type) (LabelF rt k st len t l nested)) a = ToBitStringBuilder (Proxy (IsA Type (BitRecordField rt k st len t)) nested) a

type ToBitStringBuilder (Proxy (A Type (BitRecordField (B s) * Nat s (MkFieldBits s)) -> Type) (MkField (B s) * Nat s (MkFieldBits s))) a

type ToBitStringBuilder (Proxy (A Type (BitRecordField (B s) * Nat s (MkFieldBits s)) -> Type) (MkField (B s) * Nat s (MkFieldBits s))) a = B s -> a

type ToBitStringBuilder (Proxy (A Type (BitRecordField (EnumValue e) * e size (MkFieldCustom * (EnumValue e) e size)) -> Type) (MkField (EnumValue e) * e size (MkFieldCustom * (EnumValue e) e size))) r

type ToBitStringBuilder (Proxy (A Type (BitRecordField (EnumValue e) * e size (MkFieldCustom * (EnumValue e) e size)) -> Type) (MkField (EnumValue e) * e size (MkFieldCustom * (EnumValue e) e size))) r = EnumValue e -> r

type ToBitStringBuilder (Proxy (A Type (BitRecordField (EnumValue e) * e size (MkFieldCustom * (EnumValue e) e size)) -> Type) ((:=) (EnumValue e) size e (MkFieldCustom * (EnumValue e) e size) f v)) r

type ToBitStringBuilder (Proxy (A Type (BitRecordField (EnumValue e) * e size (MkFieldCustom * (EnumValue e) e size)) -> Type) ((:=) (EnumValue e) size e (MkFieldCustom * (EnumValue e) e size) f v)) r = r

type ToBitStringBuilder (Proxy (IsA * BitRecord) r) a

type ToBitStringBuilder (Proxy (IsA * BitRecord) r) a = ToBitStringBuilder (Proxy BitRecord (Eval BitRecord r)) a

type ($~) (IsA * foo) foo (Extract * foo) x

type ($~) (IsA * foo) foo (Extract * foo) x = Eval foo x

type ($~) (IsA * foo) bar1 ((:^>>>:) * bar1 * foo * bar f g) x

type ($~) (IsA * foo) bar1 ((:^>>>:) * bar1 * foo * bar f g) x = ($~) bar bar1 g (($~) foo bar f (Eval foo x))

type ($~) (IsA * foo) (IsA * o) ((:^>>>^:) * o * foo * bar f g) x

type ($~) (IsA * foo) (IsA * o) ((:^>>>^:) * o * foo * bar f g) x = Return o (($~) bar o g (($~) foo bar f (Eval foo x)))

type SizeFieldValue (A Type (BitRecordField rt k st size t) -> Type) (MkField rt k st size t)

type SizeFieldValue (A Type (BitRecordField rt k st size t) -> Type) (MkField rt k st size t) = size

type SizeFieldValue (A Type (BitRecordField rt * k size t) -> Type) ((:=) rt size k t f v)

type SizeFieldValue (A Type (BitRecordField rt * k size t) -> Type) ((:=) rt size k t f v) = SizeFieldValue k v

type SizeFieldValue (A Type (BitRecordField rt k st len t) -> Type) (LabelF rt k st len t l f)

type SizeFieldValue (A Type (BitRecordField rt k st len t) -> Type) (LabelF rt k st len t l f) = SizeFieldValue (IsA Type (BitRecordField rt k st len t)) f

type IsA foo = (A foo -> Type :: Type)

Type alias for A such that data Point2 x y :: A Vec2 -> Type becomes data Point2 x y :: IsA Vec2

type IsAn oo = (IsA oo :: Type)

An alias to IsA

type Return f = Pure f

data Pure f :: IsAn o

A type foo, IsA foo.

Instances

type Eval foo (Pure foo f)

type Eval foo (Pure foo f) = f

type family Eval (t :: A foo -> Type) :: foo

An open type family to turn symbolic type representations created with A or IsA into the actual types.

Instances

type Eval BitRecord (OptionalRecord (Nothing BitRecord))

type Eval BitRecord (OptionalRecord (Nothing BitRecord)) = EmptyBitRecord

type Eval BitRecord (OptionalRecord (Just BitRecord t))

type Eval BitRecord (OptionalRecord (Just BitRecord t)) = t

type Eval BitRecord (StaticExpandableContent record)

type Eval BitRecord (StaticExpandableContent record) = (:+:) (ExpandableSize (ShiftR StaticExpandableContentMaxBits (BitRecordSize record) 3)) record

type Eval foo (Pure foo f)

type Eval foo (Pure foo f) = f

type Eval BitRecord (RecArray r n)

type Eval BitRecord (RecArray r n) = RecArrayToBitRecord r n

type Eval BitRecord ((:^+) l r)

type Eval BitRecord ((:^+) l r) = Append (Eval BitRecord l) r

type Eval BitRecord ((:+^) l r)

type Eval BitRecord ((:+^) l r) = Append l (Eval BitRecord r)

type Eval BitRecord (BitRecordOfList foo f xs)

type Eval BitRecord (BitRecordOfList foo f xs) = FoldMap foo BitRecord BitRecordAppendFun EmptyBitRecord f xs

type Eval AudioSubConfig (GASpecificConfig fl cd ext)

type Eval AudioSubConfig (GASpecificConfig fl cd ext) = TypeError AudioSubConfig (Text "AudioSubConfig is abstract!")

type Eval BitRecord (Sized rt len t1 sf r)

type Eval BitRecord (Sized rt len t1 sf r) = (.+:) rt * Nat len t1 ((:=) rt len Nat t1 ((@:) rt * Nat len t1 "size" sf) (SizeFieldValue BitRecord r)) r

type Eval foo1 ((:>>=:) * foo1 * foo x f)

type Eval foo1 ((:>>=:) * foo1 * foo x f) = Eval foo1 (($~) foo (IsA * foo1) f (Eval foo x))

type Eval BitRecord (RecordField rt k st len t f)

type Eval BitRecord (RecordField rt k st len t f) = BitRecordMember rt k st len t f

type Eval BitRecord (MaybeField rt k st len t (Nothing (IsA Type (BitRecordField rt k st len t))))

type Eval BitRecord (MaybeField rt k st len t (Nothing (IsA Type (BitRecordField rt k st len t)))) = EmptyBitRecord

type Eval BitRecord (MaybeField rt k st len t (Just (IsA Type (BitRecordField rt k st len t)) fld))

type Eval BitRecord (MaybeField rt k st len t (Just (IsA Type (BitRecordField rt k st len t)) fld)) = BitRecordMember rt k st len t fld

type Eval BitRecord (SizedField rt k st len t2 rt1 len1 t1 sf r)

type Eval BitRecord (SizedField rt k st len t2 rt1 len1 t1 sf r) = (.+.) rt k st len t2 rt1 * Nat len1 t1 ((:=) rt1 len1 Nat t1 ((@:) rt1 * Nat len1 t1 "size" sf) (SizeFieldValue (IsA Type (BitRecordField rt k st len t2)) r)) r

type Eval (EnumOf enum) (EnumParamAlt enum size label (FixedEnum enum size))

type Eval (EnumOf enum) (EnumParamAlt enum size label (FixedEnum enum size)) = TypeError (EnumOf enum) ((:<>:) (Text "Cannot assign an extension value to the FixedEnum ") (ShowType Type enum))

type Eval (EnumOf enum) (EnumParamAlt enum size label (ExtEnum rt k st len t enum size extInd extField))

type Eval (EnumOf enum) (EnumParamAlt enum size label (ExtEnum rt k st len t enum size extInd extField)) = MkEnumOf enum size label (ExtEnum rt k st len t enum size extInd extField) (StaticFieldValue enum label extInd) (BitRecordMember rt k st len t ((:~) label rt k st len t extField (RuntimeFieldValue k st label)))

type Eval (EnumOf enum) (EnumParam enum size label ei)

type Eval (EnumOf enum) (EnumParam enum size label ei) = MkEnumOf enum size label ei (RuntimeFieldValue Type enum label) EmptyBitRecord

type Eval (EnumOf enum) (SetEnum enum size l ei value)

type Eval (EnumOf enum) (SetEnum enum size l ei value) = MkEnumOf enum size l ei (StaticFieldValue enum l value) EmptyBitRecord

type Eval (EnumOf enum) (SetEnumAlt k enum size l (FixedEnum enum size) value)

type Eval (EnumOf enum) (SetEnumAlt k enum size l (FixedEnum enum size) value) = TypeError (EnumOf enum) ((:<>:) (Text "Cannot assign an 'extended' value to the 'FixedEnum' ") (ShowType Type enum))

type Eval (EnumOf enum) (SetEnumAlt st enum size l (ExtEnum rt * st len t enum size extInd extField) value)

type Eval (EnumOf enum) (SetEnumAlt st enum size l (ExtEnum rt * st len t enum size extInd extField) value) = MkEnumOf enum size l (ExtEnum rt * st len t enum size extInd extField) (StaticFieldValue enum l extInd) (BitRecordMember rt * st len t ((:=) rt len st t extField value))

type Eval (Descriptor 6 SLConfigDescr) Mp4SyncLayerDescriptor

type Eval (Descriptor 6 SLConfigDescr) Mp4SyncLayerDescriptor = MkDescriptor 6 SLConfigDescr (BitRecordMember Word8 * Nat 8 MkFieldU8 ((:=) Word8 8 Nat MkFieldU8 ((@:) Word8 * Nat 8 MkFieldU8 "predefined" FieldU8) 2))

type Eval (Descriptor 20 ProfileLevelIndicationIndexDescr) (ProfileLevelIndicationIndexDescriptor val)

type Eval (Descriptor 20 ProfileLevelIndicationIndexDescr) (ProfileLevelIndicationIndexDescriptor val) = MkDescriptor 20 ProfileLevelIndicationIndexDescr (BitRecordMember Word8 * Nat 8 MkFieldU8 ((:~) "profileLevelIndicationIndex" Word8 * Nat 8 MkFieldU8 FieldU8 val))

type Eval (Descriptor 4 DecoderConfigDescr) (DecoderConfigDescriptor ot st di ps)

type Eval (Descriptor 4 DecoderConfigDescr) (DecoderConfigDescriptor ot st di ps) = MkDescriptor 4 DecoderConfigDescr (DecoderConfigDescriptorBody ot st di ps)

type Eval (DecoderSpecificInfo AudioIso14496_3 AudioStream) (AudioConfigAacMinimal aoId subCfg freq channels)

type Eval (DecoderSpecificInfo AudioIso14496_3 AudioStream) (AudioConfigAacMinimal aoId subCfg freq channels) = MkDecoderSpecificInfo AudioIso14496_3 AudioStream (AudioConfigCommon ChannelConfigTable SamplingFreqTable aoId freq channels (BitRecordOfAudioSubConfig subCfg))

type Eval (DecoderSpecificInfo AudioIso14496_3 AudioStream) (AudioConfigSbrExplicitHierachical aoId subCfg freq channels extFreq)

type Eval (DecoderSpecificInfo AudioIso14496_3 AudioStream) (AudioConfigSbrExplicitHierachical aoId subCfg freq channels extFreq) = MkDecoderSpecificInfo AudioIso14496_3 AudioStream (AudioConfigCommon ChannelConfigTable SamplingFreqTable Sbr freq channels ((:+:) ((:+:) (BitRecordOfEnum SamplingFreqTable extFreq) (AudioObjectTypeRec aoId)) (BitRecordOfAudioSubConfig subCfg)))

type Eval (Descriptor 3 ES_Descr) (ESDescriptor len esId depEsId url ocrEsId streamPrio decConfig slConfig)

type Eval (Descriptor 3 ES_Descr) (ESDescriptor len esId depEsId url ocrEsId streamPrio decConfig slConfig) = MkDescriptor 3 ES_Descr ((:+:) ((:+:) ((:+:) ((:+:) ((.+:) Word16 * Nat 16 MkFieldU16 ((:~) "esId" Word16 * Nat 16 MkFieldU16 ((@:) Word16 * Nat 16 MkFieldU16 "esId" FieldU16) esId) ((.+:) Bool * Bool 1 MkFieldFlag ((@:) Bool * Bool 1 MkFieldFlag "depEsIdFlag" (FlagJust (IsA Type (FieldValue * "depEsId" Nat)) depEsId)) ((.+:) Bool * Bool 1 MkFieldFlag ((@:) Bool * Bool 1 MkFieldFlag "urlFlag" (FlagJust (IsA Type (BitRecordField ASizedString * ASizedString len (MkFieldCustom * ASizedString ASizedString len))) url)) ((.+:) Bool * Bool 1 MkFieldFlag ((@:) Bool * Bool 1 MkFieldFlag "ocrEsIdFlag" (FlagJust (IsA Type (FieldValue * "ocrEsId" Nat)) ocrEsId)) ((.+:) (B 5) * Nat 5 (MkFieldBits 5) ((:~) "streamPrio" (B 5) * Nat 5 (MkFieldBits 5) ((@:) (B 5) * Nat 5 (MkFieldBits 5) "streamPriority" (Field 5)) streamPrio) ((:+?) "depEsId" Word16 * Nat 16 MkFieldU16 ((@:) Word16 * Nat 16 MkFieldU16 "depEsId" FieldU16) depEsId)))))) (Eval BitRecord (OptionalRecordOf (IsA Type (BitRecordField ASizedString * ASizedString len (MkFieldCustom * ASizedString ASizedString len))) (Fun1 * BitRecord (IsA Type (BitRecordField ASizedString * ASizedString len (MkFieldCustom * ASizedString ASizedString len))) (RecordField ASizedString * ASizedString len (MkFieldCustom * ASizedString ASizedString len))) url))) ((:+?) "ocrEsId" Word16 * Nat 16 MkFieldU16 ((@:) Word16 * Nat 16 MkFieldU16 "ocrEsId" FieldU16) ocrEsId)) (($~) (Descriptor 4 DecoderConfigDescr) BitRecord (BitRecordOfDescriptor 4 DecoderConfigDescr) (Eval (Descriptor 4 DecoderConfigDescr) decConfig))) (($~) (Descriptor 6 SLConfigDescr) BitRecord (BitRecordOfDescriptor 6 SLConfigDescr) (Eval (Descriptor 6 SLConfigDescr) slConfig)))

data foo :-> bar

A symbolic type-level function.

Instances

type ($~) foo (IsA * ((:->) Type * a (IsA k b))) (Fun2 k b a foo f) x

type ($~) foo (IsA * ((:->) Type * a (IsA k b))) (Fun2 k b a foo f) x = Fun1 k b a (f x)

type ($~) foo (IsA * ((:->) Type * a (IsA * ((:->) Type * b (IsA k c))))) (Fun3 k c b a foo f) x

type ($~) foo (IsA * ((:->) Type * a (IsA * ((:->) Type * b (IsA k c))))) (Fun3 k c b a foo f) x = Fun2 k c b a (f x)

type ($~) foo (IsA * ((:->) Type * a (IsA * ((:->) Type * b (IsA * ((:->) Type * c (IsAn k d))))))) (Fun4 k d c b a foo f) x

type ($~) foo (IsA * ((:->) Type * a (IsA * ((:->) Type * b (IsA * ((:->) Type * c (IsAn k d))))))) (Fun4 k d c b a foo f) x = Fun3 k d c b a (f x)

data Id :: IsA (foo :-> foo)

Identity

Instances

type ($~) bar bar (Id * bar) x

type ($~) bar bar (Id * bar) x = x

type Apply f x = f $~ x

An alias for $~

type (^*^) f x = f $~ Eval x infixl 0

Symbolic function application

type family (f :: IsA (foo :-> bar)) $~ (x :: foo) :: bar infixl 0

An open family of functions from foo to bar

Instances

type ($~) BitRecord BitRecord (BitRecordAppendFun_ l) r

type ($~) BitRecord BitRecord (BitRecordAppendFun_ l) r = Append l r

type ($~) bar bar (Id * bar) x

type ($~) bar bar (Id * bar) x = x

type ($~) foo bar1 ((:>>>:) * bar1 * foo * bar f g) x

type ($~) foo bar1 ((:>>>:) * bar1 * foo * bar f g) x = ($~) bar bar1 g (($~) foo bar f x)

type ($~) foo (IsA k b) (Fun1 k b foo f) x

type ($~) foo (IsA k b) (Fun1 k b foo f) x = f x

type ($~) foo (IsA * ((:->) Type * a (IsA k b))) (Fun2 k b a foo f) x

type ($~) foo (IsA * ((:->) Type * a (IsA k b))) (Fun2 k b a foo f) x = Fun1 k b a (f x)

type ($~) foo (IsA * ((:->) Type * a (IsA * ((:->) Type * b (IsA k c))))) (Fun3 k c b a foo f) x

type ($~) foo (IsA * ((:->) Type * a (IsA * ((:->) Type * b (IsA k c))))) (Fun3 k c b a foo f) x = Fun2 k c b a (f x)

type ($~) foo (IsA * ((:->) Type * a (IsA * ((:->) Type * b (IsA * ((:->) Type * c (IsAn k d))))))) (Fun4 k d c b a foo f) x

type ($~) foo (IsA * ((:->) Type * a (IsA * ((:->) Type * b (IsA * ((:->) Type * c (IsAn k d))))))) (Fun4 k d c b a foo f) x = Fun3 k d c b a (f x)

type ($~) foo (IsA * o) ((:>>>^:) * o * foo * bar f g) x

type ($~) foo (IsA * o) ((:>>>^:) * o * foo * bar f g) x = Return o (($~) bar o g (($~) foo bar f x))

type ($~) (Maybe s) (IsA k t) (Optional s k t fallback f) (Nothing s)

type ($~) (Maybe s) (IsA k t) (Optional s k t fallback f) (Nothing s) = fallback

type ($~) (Maybe foo) (IsA k t) (Optional foo k t fallback f) (Just foo s)

type ($~) (Maybe foo) (IsA k t) (Optional foo k t fallback f) (Just foo s) = ($~) foo (IsA k t) f s

type ($~) (IsA * foo) foo (Extract * foo) x

type ($~) (IsA * foo) foo (Extract * foo) x = Eval foo x

type ($~) (Descriptor tagInd tag) BitRecord (BitRecordOfDescriptor tagInd tag) (MkDescriptor tagInd tag body)

type ($~) (Descriptor tagInd tag) BitRecord (BitRecordOfDescriptor tagInd tag) (MkDescriptor tagInd tag body) = (.+:) Word8 * Nat 8 MkFieldU8 ((:=) Word8 8 Nat MkFieldU8 FieldU8 tagInd) (Eval BitRecord (StaticExpandableContent body))

type ($~) (IsA * foo) bar1 ((:^>>>:) * bar1 * foo * bar f g) x

type ($~) (IsA * foo) bar1 ((:^>>>:) * bar1 * foo * bar f g) x = ($~) bar bar1 g (($~) foo bar f (Eval foo x))

type ($~) (DecoderSpecificInfo ot st) (Descriptor 5 DecSpecificInfo) (DescriptorOfDecoderSpecificInfo ot st) (MkDecoderSpecificInfo ot st body)

type ($~) (DecoderSpecificInfo ot st) (Descriptor 5 DecSpecificInfo) (DescriptorOfDecoderSpecificInfo ot st) (MkDecoderSpecificInfo ot st body) = MkDescriptor 5 DecSpecificInfo body

type ($~) (IsA * foo) (IsA * o) ((:^>>>^:) * o * foo * bar f g) x

type ($~) (IsA * foo) (IsA * o) ((:^>>>^:) * o * foo * bar f g) x = Return o (($~) bar o g (($~) foo bar f (Eval foo x)))

data (:>>=:) :: IsA foo -> IsA (foo :-> IsA bar) -> IsA bar infixl 1

Eval and ApplyCompose functions

Instances

type Eval foo1 ((:>>=:) * foo1 * foo x f)

type Eval foo1 ((:>>=:) * foo1 * foo x f) = Eval foo1 (($~) foo (IsA * foo1) f (Eval foo x))

data (:>>>:) :: IsA (good :-> better) -> IsA (better :-> best) -> IsA (good :-> best) infixl 1

Compose functions

Instances

type ($~) foo bar1 ((:>>>:) * bar1 * foo * bar f g) x

type ($~) foo bar1 ((:>>>:) * bar1 * foo * bar f g) x = ($~) bar bar1 g (($~) foo bar f x)

data (:^>>>:) :: IsA (good :-> better) -> IsA (better :-> best) -> IsA (IsA good :-> best) infixl 1

Eval Input & Compose

Instances

type ($~) (IsA * foo) bar1 ((:^>>>:) * bar1 * foo * bar f g) x

type ($~) (IsA * foo) bar1 ((:^>>>:) * bar1 * foo * bar f g) x = ($~) bar bar1 g (($~) foo bar f (Eval foo x))

data (:>>>^:) :: IsA (good :-> better) -> IsA (better :-> best) -> IsA (good :-> IsA best) infixl 1

Compose and Return

Instances

type ($~) foo (IsA * o) ((:>>>^:) * o * foo * bar f g) x

type ($~) foo (IsA * o) ((:>>>^:) * o * foo * bar f g) x = Return o (($~) bar o g (($~) foo bar f x))

data (:^>>>^:) :: IsA (good :-> better) -> IsA (better :-> best) -> IsA (IsA good :-> IsA best) infixl 1

Eval compose and return

Instances

type ($~) (IsA * foo) (IsA * o) ((:^>>>^:) * o * foo * bar f g) x

type ($~) (IsA * foo) (IsA * o) ((:^>>>^:) * o * foo * bar f g) x = Return o (($~) bar o g (($~) foo bar f (Eval foo x)))

data Extract :: IsA (IsA x :-> x)

A function that applies Eval

Instances

type ($~) (IsA * foo) foo (Extract * foo) x

type ($~) (IsA * foo) foo (Extract * foo) x = Eval foo x

data Optional :: IsA t -> IsA (s :-> IsA t) -> IsA (Maybe s :-> IsA t)

Either use the value from Just or return a fallback value(types(kinds))

Instances

type ($~) (Maybe s) (IsA k t) (Optional s k t fallback f) (Nothing s)

type ($~) (Maybe s) (IsA k t) (Optional s k t fallback f) (Nothing s) = fallback

type ($~) (Maybe foo) (IsA k t) (Optional foo k t fallback f) (Just foo s)

type ($~) (Maybe foo) (IsA k t) (Optional foo k t fallback f) (Just foo s) = ($~) foo (IsA k t) f s

type family FoldMap (append :: IsA (bar :-> IsA (bar :-> bar))) (zero :: bar) (f :: IsA (foo :-> bar)) (xs :: [(foo :: Type)]) :: (bar :: Type) where ...

Map over the elements of a list and fold the result.

Equations

FoldMap append zero f '[] = zero

FoldMap append zero f (x ': xs) = (append $~ (f $~ x)) $~ FoldMap append zero f xs

data Fun1 :: (a -> IsA b) -> IsA (a :-> IsA b)

Like TyCon1 from Data.Singletons

Instances

type ($~) foo (IsA k b) (Fun1 k b foo f) x

type ($~) foo (IsA k b) (Fun1 k b foo f) x = f x

data Fun2 :: (a -> b -> IsA c) -> IsA (a :-> IsA (b :-> IsA c))

Instances

type ($~) foo (IsA * ((:->) Type * a (IsA k b))) (Fun2 k b a foo f) x

type ($~) foo (IsA * ((:->) Type * a (IsA k b))) (Fun2 k b a foo f) x = Fun1 k b a (f x)

data Fun3 :: (a -> b -> c -> IsA d) -> IsA (a :-> IsA (b :-> IsA (c :-> IsA d)))

Instances

type ($~) foo (IsA * ((:->) Type * a (IsA * ((:->) Type * b (IsA k c))))) (Fun3 k c b a foo f) x

type ($~) foo (IsA * ((:->) Type * a (IsA * ((:->) Type * b (IsA k c))))) (Fun3 k c b a foo f) x = Fun2 k c b a (f x)

data Fun4 :: (a -> b -> c -> d -> IsAn e) -> IsA (a :-> IsA (b :-> IsA (c :-> IsA (d :-> IsAn e))))

Instances

type ($~) foo (IsA * ((:->) Type * a (IsA * ((:->) Type * b (IsA * ((:->) Type * c (IsAn k d))))))) (Fun4 k d c b a foo f) x

type ($~) foo (IsA * ((:->) Type * a (IsA * ((:->) Type * b (IsA * ((:->) Type * c (IsAn k d))))))) (Fun4 k d c b a foo f) x = Fun3 k d c b a (f x)