Safe Haskell	Safe-Inferred
Language	GHC2021

Plutarch.DataRepr.Internal.HList.Utils

Synopsis

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

Documentation

newtype Labeled sym 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 :: Elem a (a ': as)
There :: Elem a as -> Elem a (b ': as)

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

Indexing type-level lists

Equations

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

type family IndexLabel name as where ... Source #

Indexing list of labeled pairs by label

Equations

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

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

Return the single item from a singleton list

Equations

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

Drop first n fields of a list

Equations

Drop 0 xs = xs
Drop n (_ ': xs) = Drop (n - 1) xs