Data.Kind.Extra

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

Documentation

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

A group of types that all Eval into the same type. This is an open and extensible alternative to defining an algebraic data type and using the promoted constructors. A goes hand-in-hand with IsA for better readability.

For 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 (MkField MkFieldFlag)) a

Defined in Data.Type.BitRecords.Builder.LazyByteStringBuilder

Associated Types

type ToBitStringBuilder (Proxy (MkField MkFieldFlag)) a :: Type

Methods

bitStringBuilderHoley :: Proxy (MkField MkFieldFlag) -> FunctionBuilder BitStringBuilder a (ToBitStringBuilder (Proxy (MkField MkFieldFlag)) a)

BitStringBuilderHoley (Proxy (MkField MkFieldI8)) a

Defined in Data.Type.BitRecords.Builder.LazyByteStringBuilder

Associated Types

type ToBitStringBuilder (Proxy (MkField MkFieldI8)) a :: Type

Methods

bitStringBuilderHoley :: Proxy (MkField MkFieldI8) -> FunctionBuilder BitStringBuilder a (ToBitStringBuilder (Proxy (MkField MkFieldI8)) a)

BitStringBuilderHoley (Proxy (MkField MkFieldI16)) a

Defined in Data.Type.BitRecords.Builder.LazyByteStringBuilder

Associated Types

type ToBitStringBuilder (Proxy (MkField MkFieldI16)) a :: Type

Methods

bitStringBuilderHoley :: Proxy (MkField MkFieldI16) -> FunctionBuilder BitStringBuilder a (ToBitStringBuilder (Proxy (MkField MkFieldI16)) a)

BitStringBuilderHoley (Proxy (MkField MkFieldI32)) a

Defined in Data.Type.BitRecords.Builder.LazyByteStringBuilder

Associated Types

type ToBitStringBuilder (Proxy (MkField MkFieldI32)) a :: Type

Methods

bitStringBuilderHoley :: Proxy (MkField MkFieldI32) -> FunctionBuilder BitStringBuilder a (ToBitStringBuilder (Proxy (MkField MkFieldI32)) a)

BitStringBuilderHoley (Proxy (MkField MkFieldI64)) a

Defined in Data.Type.BitRecords.Builder.LazyByteStringBuilder

Associated Types

type ToBitStringBuilder (Proxy (MkField MkFieldI64)) a :: Type

Methods

bitStringBuilderHoley :: Proxy (MkField MkFieldI64) -> FunctionBuilder BitStringBuilder a (ToBitStringBuilder (Proxy (MkField MkFieldI64)) a)

BitStringBuilderHoley (Proxy (MkField MkFieldU8)) a

Defined in Data.Type.BitRecords.Builder.LazyByteStringBuilder

Associated Types

type ToBitStringBuilder (Proxy (MkField MkFieldU8)) a :: Type

Methods

bitStringBuilderHoley :: Proxy (MkField MkFieldU8) -> FunctionBuilder BitStringBuilder a (ToBitStringBuilder (Proxy (MkField MkFieldU8)) a)

BitStringBuilderHoley (Proxy (MkField MkFieldU16)) a

Defined in Data.Type.BitRecords.Builder.LazyByteStringBuilder

Associated Types

type ToBitStringBuilder (Proxy (MkField MkFieldU16)) a :: Type

Methods

bitStringBuilderHoley :: Proxy (MkField MkFieldU16) -> FunctionBuilder BitStringBuilder a (ToBitStringBuilder (Proxy (MkField MkFieldU16)) a)

BitStringBuilderHoley (Proxy (MkField MkFieldU32)) a

Defined in Data.Type.BitRecords.Builder.LazyByteStringBuilder

Associated Types

type ToBitStringBuilder (Proxy (MkField MkFieldU32)) a :: Type

Methods

bitStringBuilderHoley :: Proxy (MkField MkFieldU32) -> FunctionBuilder BitStringBuilder a (ToBitStringBuilder (Proxy (MkField MkFieldU32)) a)

BitStringBuilderHoley (Proxy (MkField MkFieldU64)) a

Defined in Data.Type.BitRecords.Builder.LazyByteStringBuilder

Associated Types

type ToBitStringBuilder (Proxy (MkField MkFieldU64)) a :: Type

Methods

bitStringBuilderHoley :: Proxy (MkField MkFieldU64) -> FunctionBuilder BitStringBuilder a (ToBitStringBuilder (Proxy (MkField MkFieldU64)) a)

(KnownNat v, BitStringBuilderHoley (Proxy f) a, ToBitStringBuilder (Proxy f) a ~ (rt -> a), Num rt) => BitStringBuilderHoley (Proxy (f := v)) a

Defined in Data.Type.BitRecords.Builder.LazyByteStringBuilder

Associated Types

type ToBitStringBuilder (Proxy (f := v)) a :: Type

Methods

bitStringBuilderHoley :: Proxy (f := v) -> FunctionBuilder BitStringBuilder a (ToBitStringBuilder (Proxy (f := v)) a)

(KnownNat v, BitStringBuilderHoley (Proxy f) a, ToBitStringBuilder (Proxy f) a ~ (x -> a), Num x) => BitStringBuilderHoley (Proxy (f := NegativeNat v)) a

Defined in Data.Type.BitRecords.Builder.LazyByteStringBuilder

Associated Types

type ToBitStringBuilder (Proxy (f := NegativeNat v)) a :: Type

Methods

bitStringBuilderHoley :: Proxy (f := NegativeNat v) -> FunctionBuilder BitStringBuilder a (ToBitStringBuilder (Proxy (f := NegativeNat v)) a)

(KnownNat v, BitStringBuilderHoley (Proxy f) a, ToBitStringBuilder (Proxy f) a ~ (x -> a), Num x) => BitStringBuilderHoley (Proxy (f := PositiveNat v)) a

Defined in Data.Type.BitRecords.Builder.LazyByteStringBuilder

Associated Types

type ToBitStringBuilder (Proxy (f := PositiveNat v)) a :: Type

Methods

bitStringBuilderHoley :: Proxy (f := PositiveNat v) -> FunctionBuilder BitStringBuilder a (ToBitStringBuilder (Proxy (f := PositiveNat v)) a)

BitRecordFieldSize f ~ 1 => BitStringBuilderHoley (Proxy (f := False)) a

Defined in Data.Type.BitRecords.Builder.LazyByteStringBuilder

Associated Types

type ToBitStringBuilder (Proxy (f := False)) a :: Type

Methods

bitStringBuilderHoley :: Proxy (f := False) -> FunctionBuilder BitStringBuilder a (ToBitStringBuilder (Proxy (f := False)) a)

BitRecordFieldSize f ~ 1 => BitStringBuilderHoley (Proxy (f := True)) a

Defined in Data.Type.BitRecords.Builder.LazyByteStringBuilder

Associated Types

type ToBitStringBuilder (Proxy (f := True)) a :: Type

Methods

bitStringBuilderHoley :: Proxy (f := True) -> FunctionBuilder BitStringBuilder a (ToBitStringBuilder (Proxy (f := True)) a)

BitStringBuilderHoley (Proxy nested) a => BitStringBuilderHoley (Proxy (LabelF l nested)) a

Defined in Data.Type.BitRecords.Builder.LazyByteStringBuilder

Associated Types

type ToBitStringBuilder (Proxy (LabelF l nested)) a :: Type

Methods

bitStringBuilderHoley :: Proxy (LabelF l nested) -> FunctionBuilder BitStringBuilder a (ToBitStringBuilder (Proxy (LabelF l nested)) a)

KnownChunkSize s => BitStringBuilderHoley (Proxy (MkField (MkFieldBits :: BitField (B s) Nat s))) a

Defined in Data.Type.BitRecords.Builder.LazyByteStringBuilder

Associated Types

type ToBitStringBuilder (Proxy (MkField MkFieldBits)) a :: Type

Methods

bitStringBuilderHoley :: Proxy (MkField MkFieldBits) -> FunctionBuilder BitStringBuilder a (ToBitStringBuilder (Proxy (MkField MkFieldBits)) a)

KnownChunkSize size => BitStringBuilderHoley (Proxy (MkField (MkFieldCustom :: BitField (EnumValue e) e size))) r

Defined in Data.Type.BitRecords.Enum

Associated Types

type ToBitStringBuilder (Proxy (MkField MkFieldCustom)) r :: Type

Methods

bitStringBuilderHoley :: Proxy (MkField MkFieldCustom) -> FunctionBuilder BitStringBuilder r (ToBitStringBuilder (Proxy (MkField MkFieldCustom)) r)

(KnownNat (FromEnum e v), KnownChunkSize size) => BitStringBuilderHoley (Proxy (f := v)) r

Defined in Data.Type.BitRecords.Enum

Associated Types

type ToBitStringBuilder (Proxy (f := v)) r :: Type

Methods

bitStringBuilderHoley :: Proxy (f := v) -> FunctionBuilder BitStringBuilder r (ToBitStringBuilder (Proxy (f := v)) r)

BitStringBuilderHoley (Proxy (Eval r)) a => BitStringBuilderHoley (Proxy r) a

Defined in Data.Type.BitRecords.Builder.LazyByteStringBuilder

Associated Types

type ToBitStringBuilder (Proxy r) a :: Type

Methods

bitStringBuilderHoley :: Proxy r -> FunctionBuilder BitStringBuilder a (ToBitStringBuilder (Proxy r) a)

type (Extract :: A (IsA foo :-> foo) -> Type) $~ (x :: IsA foo)

Defined in Data.Kind.Extra

type (Extract :: A (IsA foo :-> foo) -> Type) $~ (x :: IsA foo) = Eval x

type (f :^>>>: g :: A (IsA foo :-> bar2) -> Type) $~ (x :: IsA foo)

Defined in Data.Kind.Extra

type (f :^>>>: g :: A (IsA foo :-> bar2) -> Type) $~ (x :: IsA foo) = g $~ (f $~ Eval x)

type Eval (MaybeField (Nothing :: Maybe (IsA (BitRecordField t))) :: A BitRecord -> Type)

Defined in Data.Type.BitRecords.Core

type Eval (MaybeField (Nothing :: Maybe (IsA (BitRecordField t))) :: A BitRecord -> Type) = EmptyBitRecord

type Eval (MaybeField (Just fld) :: A BitRecord -> Type)

Defined in Data.Type.BitRecords.Core

type Eval (MaybeField (Just fld) :: A BitRecord -> Type) = BitRecordMember fld

type ToPretty (f :: IsA (BitRecordField t))

Defined in Data.Type.BitRecords.Core

type ToPretty (f :: IsA (BitRecordField t)) = PrettyField f

type ToBitStringBuilder (Proxy (MkField MkFieldFlag)) a

Defined in Data.Type.BitRecords.Builder.LazyByteStringBuilder

type ToBitStringBuilder (Proxy (MkField MkFieldFlag)) a = Bool -> a

type ToBitStringBuilder (Proxy (MkField MkFieldI8)) a

Defined in Data.Type.BitRecords.Builder.LazyByteStringBuilder

type ToBitStringBuilder (Proxy (MkField MkFieldI8)) a = Int8 -> a

type ToBitStringBuilder (Proxy (MkField MkFieldI16)) a

Defined in Data.Type.BitRecords.Builder.LazyByteStringBuilder

type ToBitStringBuilder (Proxy (MkField MkFieldI16)) a = Int16 -> a

type ToBitStringBuilder (Proxy (MkField MkFieldI32)) a

Defined in Data.Type.BitRecords.Builder.LazyByteStringBuilder

type ToBitStringBuilder (Proxy (MkField MkFieldI32)) a = Int32 -> a

type ToBitStringBuilder (Proxy (MkField MkFieldI64)) a

Defined in Data.Type.BitRecords.Builder.LazyByteStringBuilder

type ToBitStringBuilder (Proxy (MkField MkFieldI64)) a = Int64 -> a

type ToBitStringBuilder (Proxy (MkField MkFieldU8)) a

Defined in Data.Type.BitRecords.Builder.LazyByteStringBuilder

type ToBitStringBuilder (Proxy (MkField MkFieldU8)) a = Word8 -> a

type ToBitStringBuilder (Proxy (MkField MkFieldU16)) a

Defined in Data.Type.BitRecords.Builder.LazyByteStringBuilder

type ToBitStringBuilder (Proxy (MkField MkFieldU16)) a = Word16 -> a

type ToBitStringBuilder (Proxy (MkField MkFieldU32)) a

Defined in Data.Type.BitRecords.Builder.LazyByteStringBuilder

type ToBitStringBuilder (Proxy (MkField MkFieldU32)) a = Word32 -> a

type ToBitStringBuilder (Proxy (MkField MkFieldU64)) a

Defined in Data.Type.BitRecords.Builder.LazyByteStringBuilder

type ToBitStringBuilder (Proxy (MkField MkFieldU64)) a = Word64 -> a

type ToBitStringBuilder (Proxy (f := NegativeNat v)) a

Defined in Data.Type.BitRecords.Builder.LazyByteStringBuilder

type ToBitStringBuilder (Proxy (f := NegativeNat v)) a = a

type ToBitStringBuilder (Proxy (f := PositiveNat v)) a

Defined in Data.Type.BitRecords.Builder.LazyByteStringBuilder

type ToBitStringBuilder (Proxy (f := PositiveNat v)) a = a

type ToBitStringBuilder (Proxy (f := v)) a

Defined in Data.Type.BitRecords.Builder.LazyByteStringBuilder

type ToBitStringBuilder (Proxy (f := v)) a = a

type ToBitStringBuilder (Proxy (f := False)) a

Defined in Data.Type.BitRecords.Builder.LazyByteStringBuilder

type ToBitStringBuilder (Proxy (f := False)) a = a

type ToBitStringBuilder (Proxy (f := True)) a

Defined in Data.Type.BitRecords.Builder.LazyByteStringBuilder

type ToBitStringBuilder (Proxy (f := True)) a = a

type ToBitStringBuilder (Proxy (LabelF l nested)) a

Defined in Data.Type.BitRecords.Builder.LazyByteStringBuilder

type ToBitStringBuilder (Proxy (LabelF l nested)) a = ToBitStringBuilder (Proxy nested) a

type ToBitStringBuilder (Proxy (MkField (MkFieldBits :: BitField (B s) Nat s))) a

Defined in Data.Type.BitRecords.Builder.LazyByteStringBuilder

type ToBitStringBuilder (Proxy (MkField (MkFieldBits :: BitField (B s) Nat s))) a = B s -> a

type ToBitStringBuilder (Proxy (MkField (MkFieldCustom :: BitField (EnumValue e) e size))) r

Defined in Data.Type.BitRecords.Enum

type ToBitStringBuilder (Proxy (MkField (MkFieldCustom :: BitField (EnumValue e) e size))) r = EnumValue e -> r

type ToBitStringBuilder (Proxy (f := v)) r

Defined in Data.Type.BitRecords.Enum

type ToBitStringBuilder (Proxy (f := v)) r = r

type ToBitStringBuilder (Proxy r) a

Defined in Data.Type.BitRecords.Builder.LazyByteStringBuilder

type ToBitStringBuilder (Proxy r) a = ToBitStringBuilder (Proxy (Eval r)) a

type (Fun1 f :: A (foo :-> IsA b) -> Type) $~ (x :: foo)

Defined in Data.Kind.Extra

type (Fun1 f :: A (foo :-> IsA b) -> Type) $~ (x :: foo) = f x

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

Defined in Data.Kind.Extra

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

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

Defined in Data.Kind.Extra

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

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

Defined in Data.Kind.Extra

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

type (f :>>>^: g :: A (foo :-> IsA o) -> Type) $~ (x :: foo)

Defined in Data.Kind.Extra

type (f :>>>^: g :: A (foo :-> IsA o) -> Type) $~ (x :: foo) = Return (g $~ (f $~ x))

type (Optional fallback f :: A (Maybe s :-> IsA t) -> Type) $~ (Nothing :: Maybe s)

Defined in Data.Kind.Extra

type (Optional fallback f :: A (Maybe s :-> IsA t) -> Type) $~ (Nothing :: Maybe s) = fallback

type (Optional fallback f :: A (Maybe foo :-> IsA t) -> Type) $~ (Just s :: Maybe foo)

Defined in Data.Kind.Extra

type (Optional fallback f :: A (Maybe foo :-> IsA t) -> Type) $~ (Just s :: Maybe foo) = f $~ s

type (f :^>>>^: g :: A (IsA foo :-> IsA o) -> Type) $~ (x :: IsA foo)

Defined in Data.Kind.Extra

type (f :^>>>^: g :: A (IsA foo :-> IsA o) -> Type) $~ (x :: IsA foo) = Return (g $~ (f $~ Eval x))

type SizeFieldValue (MkField t :: A (BitRecordField t) -> Type)

Defined in Data.Type.BitRecords.Sized

type SizeFieldValue (MkField t :: A (BitRecordField t) -> Type) = size

type SizeFieldValue (f := v :: A (BitRecordField t) -> Type)

Defined in Data.Type.BitRecords.Sized

type SizeFieldValue (f := v :: A (BitRecordField t) -> Type) = SizeFieldValue v

type SizeFieldValue (LabelF l f :: A (BitRecordField t) -> Type)

Defined in Data.Type.BitRecords.Sized

type SizeFieldValue (LabelF l f :: A (BitRecordField t) -> Type) = SizeFieldValue f

type IsA (foo :: k) = (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 :: k) = (IsA oo :: Type)

An alias to IsA

type Return f = Pure f

data Pure (f :: o) :: IsAn o

A type foo, IsA foo.

Instances

type Eval (Pure f :: A foo -> Type)

Defined in Data.Kind.Extra

type Eval (Pure f :: A foo -> Type) = 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 (OptionalRecord (Nothing :: Maybe BitRecord))

Defined in Data.Type.BitRecords.Core

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

type Eval (OptionalRecord (Just t) :: A BitRecord -> Type)

Defined in Data.Type.BitRecords.Core

type Eval (OptionalRecord (Just t) :: A BitRecord -> Type) = t

type Eval (StaticExpandableContent record :: A BitRecord -> Type)

Defined in Data.ByteString.Mp4.Boxes.Expandable

type Eval (StaticExpandableContent record :: A BitRecord -> Type) = ExpandableSize (ShiftR StaticExpandableContentMaxBits (BitRecordSize record) 3) :+: record

type Eval (Pure f :: A foo -> Type)

Defined in Data.Kind.Extra

type Eval (Pure f :: A foo -> Type) = f

type Eval (RecArray r n :: A BitRecord -> Type)

Defined in Data.Type.BitRecords.Core

type Eval (RecArray r n :: A BitRecord -> Type) = RecArrayToBitRecord r n

type Eval (l :^+ r :: A BitRecord -> Type)

Defined in Data.Type.BitRecords.Core

type Eval (l :^+ r :: A BitRecord -> Type) = Append (Eval l) r

type Eval (l :+^ r :: A BitRecord -> Type)

Defined in Data.Type.BitRecords.Core

type Eval (l :+^ r :: A BitRecord -> Type) = Append l (Eval r)

type Eval (BitRecordOfList f xs :: A BitRecord -> Type)

Defined in Data.Type.BitRecords.Core

type Eval (BitRecordOfList f xs :: A BitRecord -> Type) = FoldMap BitRecordAppendFun EmptyBitRecord f xs

type Eval (GASpecificConfig fl cd ext :: A AudioSubConfig -> Type)

Defined in Data.ByteString.Mp4.Boxes.AudioSpecificConfig

type Eval (GASpecificConfig fl cd ext :: A AudioSubConfig -> Type) = (TypeError (Text "AudioSubConfig is abstract!") :: AudioSubConfig)

type Eval (Sized sf r :: A BitRecord -> Type)

Defined in Data.Type.BitRecords.Sized

type Eval (Sized sf r :: A BitRecord -> Type) = (("size" @: sf) := SizeFieldValue r) .+: r

type Eval (x :>>=: f :: A foo2 -> Type)

Defined in Data.Kind.Extra

type Eval (x :>>=: f :: A foo2 -> Type) = Eval (f $~ Eval x)

type Eval (RecordField f :: A BitRecord -> Type)

Defined in Data.Type.BitRecords.Core

type Eval (RecordField f :: A BitRecord -> Type) = BitRecordMember f

type Eval (MaybeField (Nothing :: Maybe (IsA (BitRecordField t))) :: A BitRecord -> Type)

Defined in Data.Type.BitRecords.Core

type Eval (MaybeField (Nothing :: Maybe (IsA (BitRecordField t))) :: A BitRecord -> Type) = EmptyBitRecord

type Eval (MaybeField (Just fld) :: A BitRecord -> Type)

Defined in Data.Type.BitRecords.Core

type Eval (MaybeField (Just fld) :: A BitRecord -> Type) = BitRecordMember fld

type Eval (SizedField sf r :: A BitRecord -> Type)

Defined in Data.Type.BitRecords.Sized

type Eval (SizedField sf r :: A BitRecord -> Type) = (("size" @: sf) := SizeFieldValue r) .+. r

type Eval (EnumParam label ei :: A (EnumOf enum) -> Type)

Defined in Data.Type.BitRecords.Enum

type Eval (EnumParam label ei :: A (EnumOf enum) -> Type) = MkEnumOf ei (RuntimeFieldValue label :: A (FieldValue label enum) -> Type) EmptyBitRecord

type Eval (EnumParamAlt label (FixedEnum enum size) :: A (EnumOf enum) -> Type)

Defined in Data.Type.BitRecords.Enum

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

type Eval (EnumParamAlt label (ExtEnum enum size extInd extField) :: A (EnumOf enum) -> Type)

Defined in Data.Type.BitRecords.Enum

type Eval (EnumParamAlt label (ExtEnum enum size extInd extField) :: A (EnumOf enum) -> Type) = MkEnumOf (ExtEnum enum size extInd extField) (StaticFieldValue label extInd) (BitRecordMember (extField :~ (RuntimeFieldValue label :: A (FieldValue label st) -> Type)))

type Eval (SetEnum l ei value :: A (EnumOf enum) -> Type)

Defined in Data.Type.BitRecords.Enum

type Eval (SetEnum l ei value :: A (EnumOf enum) -> Type) = MkEnumOf ei (StaticFieldValue l value) EmptyBitRecord

type Eval (SetEnumAlt l (FixedEnum enum size) value :: A (EnumOf enum) -> Type)

Defined in Data.Type.BitRecords.Enum

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

type Eval (SetEnumAlt l (ExtEnum enum size extInd extField) value :: A (EnumOf enum) -> Type)

Defined in Data.Type.BitRecords.Enum

type Eval (SetEnumAlt l (ExtEnum enum size extInd extField) value :: A (EnumOf enum) -> Type) = MkEnumOf (ExtEnum enum size extInd extField) (StaticFieldValue l extInd) (BitRecordMember (extField := value))

type Eval Mp4SyncLayerDescriptor

In the holy scripture, ISO-14496-14 section 3.1.2, it is written that there shall be restrictions on the elementary stream descriptor, in there it says: Thou shall use only two as the value for the predefined field in the blessed SLDescriptor. Not one, this is a value not big enough, nor three, this value is too much. The righteous one ever only uses two. Only a fool will use 256.

Defined in Data.ByteString.Mp4.Boxes.SyncLayerConfigDescriptor

type Eval Mp4SyncLayerDescriptor = (MkDescriptor (BitRecordMember (("predefined" @: FieldU8) := 2)) :: Descriptor SLConfigDescr)

type Eval (ProfileLevelIndicationIndexDescriptor val :: A (Descriptor ProfileLevelIndicationIndexDescr) -> Type)

Defined in Data.ByteString.Mp4.Boxes.DecoderConfigDescriptor

type Eval (ProfileLevelIndicationIndexDescriptor val :: A (Descriptor ProfileLevelIndicationIndexDescr) -> Type) = (MkDescriptor (BitRecordMember (FieldU8 :~ val)) :: Descriptor ProfileLevelIndicationIndexDescr)

type Eval (DecoderConfigDescriptor ot st di ps :: A (Descriptor DecoderConfigDescr) -> Type)

Defined in Data.ByteString.Mp4.Boxes.DecoderConfigDescriptor

type Eval (DecoderConfigDescriptor ot st di ps :: A (Descriptor DecoderConfigDescr) -> Type) = (MkDescriptor (DecoderConfigDescriptorBody ot st di ps) :: Descriptor DecoderConfigDescr)

type Eval (AudioConfigAacMinimal aoId subCfg freq channels :: A (DecoderSpecificInfo AudioIso14496_3 AudioStream) -> Type)

Defined in Data.ByteString.Mp4.Boxes.AudioSpecificConfig

type Eval (AudioConfigAacMinimal aoId subCfg freq channels :: A (DecoderSpecificInfo AudioIso14496_3 AudioStream) -> Type) = (MkDecoderSpecificInfo (AudioConfigCommon aoId freq channels (BitRecordOfAudioSubConfig subCfg)) :: DecoderSpecificInfo AudioIso14496_3 AudioStream)

type Eval (AudioConfigSbrExplicitHierachical aoId subCfg freq channels extFreq :: A (DecoderSpecificInfo AudioIso14496_3 AudioStream) -> Type)

Defined in Data.ByteString.Mp4.Boxes.AudioSpecificConfig

type Eval (AudioConfigSbrExplicitHierachical aoId subCfg freq channels extFreq :: A (DecoderSpecificInfo AudioIso14496_3 AudioStream) -> Type) = (MkDecoderSpecificInfo (AudioConfigCommon Sbr freq channels ((BitRecordOfEnum extFreq :+: AudioObjectTypeRec aoId) :+: BitRecordOfAudioSubConfig subCfg)) :: DecoderSpecificInfo AudioIso14496_3 AudioStream)

type Eval (ESDescriptor esId depEsId url ocrEsId streamPrio decConfig slConfig :: A (Descriptor ES_Descr) -> Type)

Defined in Data.ByteString.Mp4.Boxes.ElementaryStreamDescriptor

type Eval (ESDescriptor esId depEsId url ocrEsId streamPrio decConfig slConfig :: A (Descriptor ES_Descr) -> Type) = (MkDescriptor ((((((("esId" @: FieldU16) :~ esId) .+: (("depEsIdFlag" @: FlagJust depEsId) .+: (("urlFlag" @: FlagJust url) .+: (("ocrEsIdFlag" @: FlagJust ocrEsId) .+: ((("streamPriority" @: Field 5) :~ streamPrio) .+: (("depEsId" @: FieldU16) :+? depEsId)))))) :+: Eval (OptionalRecordOf (Fun1 (RecordField :: IsA (BitRecordField (MkFieldCustom :: BitField ASizedString ASizedString len)) -> A BitRecord -> Type)) url)) :+: (("ocrEsId" @: FieldU16) :+? ocrEsId)) :+: ((BitRecordOfDescriptor :: A (Descriptor DecoderConfigDescr :-> BitRecord) -> Type) $~ Eval decConfig)) :+: ((BitRecordOfDescriptor :: A (Descriptor SLConfigDescr :-> BitRecord) -> Type) $~ Eval slConfig)) :: Descriptor ES_Descr)

data foo :-> bar

A symbolic type-level function.

Instances

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

Defined in Data.Kind.Extra

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

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

Defined in Data.Kind.Extra

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

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

Defined in Data.Kind.Extra

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

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

Identity

Instances

type (Id :: A (bar :-> bar) -> Type) $~ (x :: bar)

Defined in Data.Kind.Extra

type (Id :: A (bar :-> bar) -> Type) $~ (x :: bar) = x

type Apply f x = f $~ x

An alias for $~

type (^*^) (f :: IsA (foo :-> bar)) (x :: IsA foo) = 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 (BitRecordAppendFun_ l :: A (BitRecord :-> BitRecord) -> Type) $~ (r :: BitRecord)

Defined in Data.Type.BitRecords.Core

type (BitRecordAppendFun_ l :: A (BitRecord :-> BitRecord) -> Type) $~ (r :: BitRecord) = Append l r

type (Id :: A (bar :-> bar) -> Type) $~ (x :: bar)

Defined in Data.Kind.Extra

type (Id :: A (bar :-> bar) -> Type) $~ (x :: bar) = x

type (f :>>>: g :: A (foo :-> bar2) -> Type) $~ (x :: foo)

Defined in Data.Kind.Extra

type (f :>>>: g :: A (foo :-> bar2) -> Type) $~ (x :: foo) = g $~ (f $~ x)

type (Extract :: A (IsA foo :-> foo) -> Type) $~ (x :: IsA foo)

Defined in Data.Kind.Extra

type (Extract :: A (IsA foo :-> foo) -> Type) $~ (x :: IsA foo) = Eval x

type (BitRecordOfDescriptor :: A (Descriptor tag :-> BitRecord) -> Type) $~ (MkDescriptor body :: Descriptor tag)

Defined in Data.ByteString.Mp4.Boxes.BaseDescriptor

type (BitRecordOfDescriptor :: A (Descriptor tag :-> BitRecord) -> Type) $~ (MkDescriptor body :: Descriptor tag) = (FieldU8 := tagInd) .+: Eval (StaticExpandableContent body)

type (f :^>>>: g :: A (IsA foo :-> bar2) -> Type) $~ (x :: IsA foo)

Defined in Data.Kind.Extra

type (f :^>>>: g :: A (IsA foo :-> bar2) -> Type) $~ (x :: IsA foo) = g $~ (f $~ Eval x)

type (Fun1 f :: A (foo :-> IsA b) -> Type) $~ (x :: foo)

Defined in Data.Kind.Extra

type (Fun1 f :: A (foo :-> IsA b) -> Type) $~ (x :: foo) = f x

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

Defined in Data.Kind.Extra

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

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

Defined in Data.Kind.Extra

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

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

Defined in Data.Kind.Extra

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

type (f :>>>^: g :: A (foo :-> IsA o) -> Type) $~ (x :: foo)

Defined in Data.Kind.Extra

type (f :>>>^: g :: A (foo :-> IsA o) -> Type) $~ (x :: foo) = Return (g $~ (f $~ x))

type (Optional fallback f :: A (Maybe s :-> IsA t) -> Type) $~ (Nothing :: Maybe s)

Defined in Data.Kind.Extra

type (Optional fallback f :: A (Maybe s :-> IsA t) -> Type) $~ (Nothing :: Maybe s) = fallback

type (Optional fallback f :: A (Maybe foo :-> IsA t) -> Type) $~ (Just s :: Maybe foo)

Defined in Data.Kind.Extra

type (Optional fallback f :: A (Maybe foo :-> IsA t) -> Type) $~ (Just s :: Maybe foo) = f $~ s

type (DescriptorOfDecoderSpecificInfo :: A (DecoderSpecificInfo ot st :-> Descriptor DecSpecificInfo) -> Type) $~ (MkDecoderSpecificInfo body :: DecoderSpecificInfo ot st)

Defined in Data.ByteString.Mp4.Boxes.DecoderSpecificInfo

type (DescriptorOfDecoderSpecificInfo :: A (DecoderSpecificInfo ot st :-> Descriptor DecSpecificInfo) -> Type) $~ (MkDecoderSpecificInfo body :: DecoderSpecificInfo ot st) = (MkDescriptor body :: Descriptor DecSpecificInfo)

type (f :^>>>^: g :: A (IsA foo :-> IsA o) -> Type) $~ (x :: IsA foo)

Defined in Data.Kind.Extra

type (f :^>>>^: g :: A (IsA foo :-> IsA o) -> Type) $~ (x :: IsA foo) = Return (g $~ (f $~ Eval x))

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

Eval and ApplyCompose functions

Instances

type Eval (x :>>=: f :: A foo2 -> Type)

Defined in Data.Kind.Extra

type Eval (x :>>=: f :: A foo2 -> Type) = Eval (f $~ Eval x)

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

Compose functions

Instances

type (f :>>>: g :: A (foo :-> bar2) -> Type) $~ (x :: foo)

Defined in Data.Kind.Extra

type (f :>>>: g :: A (foo :-> bar2) -> Type) $~ (x :: foo) = g $~ (f $~ x)

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

Eval Input & Compose

Instances

type (f :^>>>: g :: A (IsA foo :-> bar2) -> Type) $~ (x :: IsA foo)

Defined in Data.Kind.Extra

type (f :^>>>: g :: A (IsA foo :-> bar2) -> Type) $~ (x :: IsA foo) = g $~ (f $~ Eval x)

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

Compose and Return

Instances

type (f :>>>^: g :: A (foo :-> IsA o) -> Type) $~ (x :: foo)

Defined in Data.Kind.Extra

type (f :>>>^: g :: A (foo :-> IsA o) -> Type) $~ (x :: foo) = Return (g $~ (f $~ x))

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

Eval compose and return

Instances

type (f :^>>>^: g :: A (IsA foo :-> IsA o) -> Type) $~ (x :: IsA foo)

Defined in Data.Kind.Extra

type (f :^>>>^: g :: A (IsA foo :-> IsA o) -> Type) $~ (x :: IsA foo) = Return (g $~ (f $~ Eval x))

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

A function that applies Eval

Instances

type (Extract :: A (IsA foo :-> foo) -> Type) $~ (x :: IsA foo)

Defined in Data.Kind.Extra

type (Extract :: A (IsA foo :-> foo) -> Type) $~ (x :: IsA foo) = Eval 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 (Optional fallback f :: A (Maybe s :-> IsA t) -> Type) $~ (Nothing :: Maybe s)

Defined in Data.Kind.Extra

type (Optional fallback f :: A (Maybe s :-> IsA t) -> Type) $~ (Nothing :: Maybe s) = fallback

type (Optional fallback f :: A (Maybe foo :-> IsA t) -> Type) $~ (Just s :: Maybe foo)

Defined in Data.Kind.Extra

type (Optional fallback f :: A (Maybe foo :-> IsA t) -> Type) $~ (Just s :: Maybe foo) = 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 (Fun1 f :: A (foo :-> IsA b) -> Type) $~ (x :: foo)

Defined in Data.Kind.Extra

type (Fun1 f :: A (foo :-> IsA b) -> Type) $~ (x :: foo) = f x

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

Instances

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

Defined in Data.Kind.Extra

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

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

Instances

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

Defined in Data.Kind.Extra

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

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

Instances

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

Defined in Data.Kind.Extra

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