Safe Haskell	None
Language	GHC2021

Plutarch.DataRepr.Internal.HList.Utils

Synopsis

newtype Labeled (sym :: Symbol) a = Labeled {
- unLabeled :: a
}
data Elem (a :: k) (as :: [k]) where
- Here :: forall {k} (a :: k) (as1 :: [k]). Elem a (a ': as1)
- There :: forall {k} (a :: k) (as1 :: [k]) (b :: k). Elem a as1 -> Elem a (b ': as1)
type family IndexList (n :: Nat) (l :: [k]) :: k where ...
type family IndexLabel (name :: Symbol) (as :: [(Symbol, Type)]) where ...
type family SingleItem (as :: [k]) :: k where ...
type family Drop (n :: Nat) (as :: [k]) :: [k] where ...

Documentation

newtype Labeled (sym :: Symbol) a Source #

Constructors

Labeled
Fields unLabeled :: a

data Elem (a :: k) (as :: [k]) where Source #

GADT proof-witness of HList membership, usable as an index

Constructors

Here :: forall {k} (a :: k) (as1 :: [k]). Elem a (a ': as1)
There :: forall {k} (a :: k) (as1 :: [k]) (b :: k). Elem a as1 -> Elem a (b ': as1)

type family IndexList (n :: Nat) (l :: [k]) :: k where ... Source #

Indexing type-level lists

Equations

IndexList _1 ('[] :: [k]) = TypeError ('Text "IndexList: index out of bounds") :: k
IndexList 0 (x ': _1 :: [k]) = x
IndexList n (_1 ': xs :: [k]) = IndexList (n - 1) xs

type family IndexLabel (name :: Symbol) (as :: [(Symbol, Type)]) where ... Source #

Indexing list of labeled pairs by label

Equations

IndexLabel name ('[] :: [(Symbol, Type)]) = TypeError ((('Text "Invalid field name `" ':<>: 'Text name) ':<>: 'Text "`") ':$$: 'Text "Consider adding it to `pletFields` list") :: Type
IndexLabel name ('(name, a) ': _1) = a
IndexLabel name (_1 ': as) = IndexLabel name as

type family SingleItem (as :: [k]) :: k where ... Source #

Return the single item from a singleton list

Equations

SingleItem ('[a] :: [k]) = a

type family Drop (n :: Nat) (as :: [k]) :: [k] where ... Source #

Drop first n fields of a list

Equations

Drop 0 (xs :: [k]) = xs
Drop n (_1 ': xs :: [k]) = Drop (n - 1) xs