Safe Haskell	None
Language	GHC2021

Plutarch.DataRepr.Internal.HList

Contents

HRec and Label types
Field indexing functions
Type families
Internal utils

Synopsis

data HRec (as :: [(Symbol, Type)]) where
- HNil :: HRec ('[] :: [(Symbol, Type)])
- HCons :: forall (name :: Symbol) a (as1 :: [(Symbol, Type)]). Labeled name a -> HRec as1 -> HRec ('(name, a) ': as1)
newtype HRecGeneric (as :: [(Symbol, Type)]) = HRecGeneric (HRec as)
newtype Labeled (sym :: Symbol) a = Labeled {
- unLabeled :: a
}
hrecField' :: forall (name :: Symbol) a (as :: [(Symbol, Type)]). ElemOf name a as => HRec as -> a
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 ...
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)
class IndexLabel name as ~ a => ElemOf (name :: Symbol) a (as :: [(Symbol, Type)]) | as name -> a where
- elemOf :: Elem '(name, a) as

HRec and Label types

data HRec (as :: [(Symbol, Type)]) where Source #

Constructors

HNil :: HRec ('[] :: [(Symbol, Type)])
HCons :: forall (name :: Symbol) a (as1 :: [(Symbol, Type)]). Labeled name a -> HRec as1 -> HRec ('(name, a) ': as1)

Instances

Instances details

(IndexLabel name as ~ a, ElemOf name a as, Term s (PAsData b) ~ a, PFromDataable b c) => HasField (name :: Symbol) (HRec as) (Term s c) Source #
Instance details Defined in Plutarch.DataRepr.Internal.HList Methods getField :: HRec as -> Term s c Source #

newtype HRecGeneric (as :: [(Symbol, Type)]) Source #

Constructors

HRecGeneric (HRec as)

Instances

Instances details

(IndexLabel name as ~ a, ElemOf name a as) => HasField (name :: Symbol) (HRecGeneric as) a Source #
Instance details Defined in Plutarch.DataRepr.Internal.HList Methods getField :: HRecGeneric as -> a Source #

newtype Labeled (sym :: Symbol) a Source #

Constructors

Labeled
Fields unLabeled :: a

Field indexing functions

hrecField' :: forall (name :: Symbol) a (as :: [(Symbol, Type)]). ElemOf name a as => HRec as -> a Source #

Index a HList with a field in a provided list of fields.

>>> xs = HRec @["x", "y", "z"] (HCons 1 (HCons 2 (HCons 3 HNil)))
>>> hrecField @"y" @["x", "y", "z"] xs
>>> 2

Type families

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

Internal utils

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)

class IndexLabel name as ~ a => ElemOf (name :: Symbol) a (as :: [(Symbol, Type)]) | as name -> a where Source #

Construct an Elem via Nat.

This class could instead be a more direct version of indexHList, but perhaps the Elem encoding will be useful.

Methods

elemOf :: Elem '(name, a) as Source #

Construct the Elem corresponding to a Nat index.

Example:

>>> natElem @_ @0
Here

>>> natElem @_ @3
There (There (There Here))

Instances

Instances details

ElemOf name a ('(name, a) ': as) Source #
Instance details Defined in Plutarch.DataRepr.Internal.HList Methods elemOf :: Elem '(name, a) ('(name, a) ': as) Source #
(IndexLabel name (b ': as) ~ a, ElemOf name a as) => ElemOf name a (b ': as) Source #
Instance details Defined in Plutarch.DataRepr.Internal.HList Methods elemOf :: Elem '(name, a) (b ': as) Source #