Data.GenRec

Extensible records/row polymorphism are features not implemented in Haskell. Some other functional languages do it, like Purescript. GHC extensions allowing type level-programming allow us to encode them in Haskell.

Let us define records as a (partial) mapping from names (fields, wich are static) to values.

There are many implementations out there. This is yet another one, inspired in the HList library. It arose when programming the AspectAG library. Before, we depended on HList. Then we choose to implement a record library from scratch for two reasons:

• HList is experimental, it does not maintain a stable interface.
• We prefer a solution that fits better in our use case.

AspectAG is a library to encode type safe attribute grammars. Statically checked extensible records are used everywhere, knowing at compile time the structure of the grammar, and checking if it is well-formed.

Some example structures in AspectAG library are:

• Records: that's it, plane extensible records: Mappings from names to values.
• Attributions: mappings from attribute names to values. This is the same idea that the one for records, but we wanted to have different types for each structure, and for each label. This means that our labels must be polyinded.
• Children Records: That is a map from children to attibutions. It is a record of records.

One common way to implement a record is by using a GADT. For instance indexed by the list of pairs (label, value). We want labels polykinded, and values are usually of kind Type, what makes sense since Type is the kind of inhabited types, and records store values. However, in cases such as our children records, where we store attributions that are also represented by an indexed GADT, we would like to be able to reflect some of this structural information at the indexes of the record. This can be achieved if we are polymorphic in the kind of the types corresponding to the record fields.

Documentation

data Rec (c :: k) (r :: [(k', k'')]) :: Type where

Record data structure for generic records (Internal). The c index indicates the kind of record (for each record instance, the user should define an index). The r index represents the mapping from labels to values. Labels are of kind k`. Values are still polykinded (k'`) since rich information can be statically represented here (for instance, when a record of records, or a record of Vectors is represented). k` must implement the Cmp family, although it is not visible here for simplicity. Records are built putting fields ordered according to the Cmp result of its labels. This constructors are not intended to be used to build records, (ConsRec is the problematic one). Use the smart constructors emptyRecord and .*. instead. We export the constructors to pattern match on them. Although there are solutions to hide Constructors while supporting pattern matching, we kept it simple

Constructors

EmptyRec

Fields

• :: Rec c '[]

  empty record

ConsRec

Fields

• :: TagField c l v
• -> Rec c r
• -> Rec c ('(l, v) ': r)

  ConsRec takes a tagged field (TagField) and a record, to build a new record. Recall that fields should be ordered.

Instances

(Show v, KnownSymbol l, Show (Record ('(l', v') ': r))) => Show (Record ('(l, v) ': ('(l', v') ': r)))

Defined in Data.GenRec.RecInstances.Record

Methods

showsPrec :: Int -> Record ('(l, v) ': ('(l', v') ': r)) -> ShowS

show :: Record ('(l, v) ': ('(l', v') ': r)) -> String

showList :: [Record ('(l, v) ': ('(l', v') ': r))] -> ShowS

(Show v, KnownSymbol l) => Show (Record '['(l, v)])

Defined in Data.GenRec.RecInstances.Record

Methods

showsPrec :: Int -> Record '['(l, v)] -> ShowS

show :: Record '['(l, v)] -> String

showList :: [Record '['(l, v)]] -> ShowS

Show (Record ('[] :: [(Symbol, Type)]))

Defined in Data.GenRec.RecInstances.Record

Methods

showsPrec :: Int -> Record '[] -> ShowS

show :: Record '[] -> String

showList :: [Record '[]] -> ShowS

type UnWrap (Rec c r)

Defined in Data.GenRec

type UnWrap (Rec c r) = r

data TagField (c :: k) (l :: k') (v :: k'') where

TagField

Constructors

TagField

Fields

• :: Label c
• -> Label l
• -> WrapField c v
• -> TagField c l v

  TagField tags a value v with record and label information. v is polykinded, for instance we could be tagging some kind of record, because then we would build a matrix. In that case k' could be something as `[(kindforlabels, Type)]`. But TagField contains inhabited values, it tags values of a type of kind Type. In this example perhaps some value of type `Rec Something [(kindforlabels, Type)]`. That is the role of the WrapField family. Given c, the kind of record, and v, ir computes the wrapper.

type family WrapField (c :: k') (v :: k) :: Type

Given a type of record and its index, it computes the type of record inhabitants

Instances

type WrapField Reco (v :: Type)

field type

Defined in Data.GenRec.RecInstances.Record

type WrapField Reco (v :: Type) = v

type family UnWrap (t :: Type) :: [(k, k')]

The inverse of WrapField

Instances

type UnWrap (Rec c r)

Defined in Data.GenRec

type UnWrap (Rec c r) = r

untagField :: TagField c l v -> WrapField c v

This is the destructor of TagField. Note the use of WrapField here.

(.=.) :: forall k' k k'' (l :: k') (c :: k) (v :: k''). Label l -> WrapField c v -> TagField c l v infix 4

TagField operator, note that c will be ambiguous if not annotated.

(#) :: forall c l r ctx v. RequireR (OpLookupCall c l r) ctx v => Rec c r -> Label l -> v

Pretty lookup

(.*.) :: forall k k' c (l :: k) (v :: k') (r :: [(k, k')]). Require (OpExtend c l v r) '['Text ""] => TagField c l v -> Rec c r -> ReqR (OpExtend c l v r) infixr 2

.*. the pretty cons, hiding require

class OrdType k

comparisson of Labels, this family is polykinded, each record-like structure must implement this family for its labels type family Cmp (a :: k) (b :: k) :: Ordering

Instance for Symbols type instance Cmp (a :: Symbol) (b :: Symbol) = CmpSymbol a b

Instances

OrdType Nat

Defined in Data.GenRec.RecInstances.Record

Associated Types

type Cmp a b :: Ordering

OrdType Symbol

Defined in Data.GenRec

Associated Types

type Cmp a b :: Ordering

type family Cmp (a :: k) (b :: k) :: Ordering

Instances

type Cmp (m :: Nat) (n :: Nat)

Defined in Data.GenRec.RecInstances.Record

type Cmp (m :: Nat) (n :: Nat) = CmpNat m n

type Cmp (a :: Symbol) (b :: Symbol)

Defined in Data.GenRec

type Cmp (a :: Symbol) (b :: Symbol) = CmpSymbol a b

type family ShowRec c :: Symbol

Function to show the name of records (Record, Mapping, etc):

Instances

type ShowRec Reco

Type level show utilities

Defined in Data.GenRec.RecInstances.Record

type ShowRec Reco = "Record"

type family ShowField c :: Symbol

Function to show the field of the record ("field named", "children", "tag:", etc)

Instances

type ShowField Reco

Defined in Data.GenRec.RecInstances.Record

type ShowField Reco = "field named "

type family ShowLabel (l :: k) :: Symbol

data OpLookup (c :: Type) (l :: k) (r :: [(k, k')]) :: Type where

Datatype for lookup (wrapper)

Constructors

OpLookup :: Label l -> Rec c r -> OpLookup c l r

Instances

Require (OpError (('Text "field not Found on " :<>: 'Text (ShowRec c)) :$$: ((('Text "looking up the " :<>: 'Text (ShowField c)) :<>: 'Text " ") :<>: 'Text (ShowLabel l)))) ctx => Require (OpLookup c l ('[] :: [(k, k')])) ctx

error instance (looking up an empty record)

Defined in Data.GenRec

Associated Types

type ReqR (OpLookup c l '[])

Methods

req :: Proxy ctx -> OpLookup c l '[] -> ReqR (OpLookup c l '[])

Require (OpLookup' (Cmp l l') c l ('(l', v) ': r)) ctx => Require (OpLookup c l ('(l', v) ': r)) ctx

wrapper instance

Defined in Data.GenRec

Associated Types

type ReqR (OpLookup c l ('(l', v) ': r))

Methods

req :: Proxy ctx -> OpLookup c l ('(l', v) ': r) -> ReqR (OpLookup c l ('(l', v) ': r))

type ReqR (OpLookup c l ('[] :: [(k, k')]))

Defined in Data.GenRec

type ReqR (OpLookup c l ('[] :: [(k, k')])) = ()

type ReqR (OpLookup c l ('(l', v) ': r))

Defined in Data.GenRec

type ReqR (OpLookup c l ('(l', v) ': r))

lookup :: forall k' c (r :: [(Type, k')]) (ctx :: [ErrorMessage]). Require (OpLookup c c r) ctx => Label c -> Rec c r -> ReqR (OpLookup c c r)

The lookup function. Given a Label and a Record, it returns the field at that position. It raises a custom type error if there is no field labelled with l.

data OpExtend (c :: Type) (l :: k) (v :: k') (r :: [(k, k')]) :: Type where

extension operator (wrapper)

Constructors

OpExtend :: Label l -> WrapField c v -> Rec c r -> OpExtend c l v r

Instances

Require (OpExtend c l v ('[] :: [(k, k')])) ctx

extending an empty record

Defined in Data.GenRec

Associated Types

type ReqR (OpExtend c l v '[])

Methods

req :: Proxy ctx -> OpExtend c l v '[] -> ReqR (OpExtend c l v '[])

Require (OpExtend' (Cmp l l') c l v ('(l', v') ': r)) ctx => Require (OpExtend c l v ('(l', v') ': r)) ctx

wrapper instance

Defined in Data.GenRec

Associated Types

type ReqR (OpExtend c l v ('(l', v') ': r))

Methods

req :: Proxy ctx -> OpExtend c l v ('(l', v') ': r) -> ReqR (OpExtend c l v ('(l', v') ': r))

type ReqR (OpExtend c l v ('[] :: [(k, k')]))

Defined in Data.GenRec

type ReqR (OpExtend c l v ('[] :: [(k, k')])) = Rec c '['(l, v)]

type ReqR (OpExtend c l v ('(l', v') ': r))

Defined in Data.GenRec

type ReqR (OpExtend c l v ('(l', v') ': r))

data OpUpdate (c :: Type) (l :: k) (v :: k') (r :: [(k, k')]) :: Type where

update operator (wrapper)

Constructors

OpUpdate :: Label l -> WrapField c v -> Rec c r -> OpUpdate c l v r

Instances

Require (OpError (('Text "field not Found on " :<>: 'Text (ShowRec c)) :$$: (('Text "updating the " :<>: 'Text (ShowField c)) :<>: ShowTE l))) ctx => Require (OpUpdate c l v ('[] :: [(k', k'')])) ctx

error instance

Defined in Data.GenRec

Associated Types

type ReqR (OpUpdate c l v '[])

Methods

req :: Proxy ctx -> OpUpdate c l v '[] -> ReqR (OpUpdate c l v '[])

Require (OpUpdate' (Cmp l l') c l v ('(l', v') ': r)) ctx => Require (OpUpdate c l v ('(l', v') ': r)) ctx

wrapper instance

Defined in Data.GenRec

Associated Types

type ReqR (OpUpdate c l v ('(l', v') ': r))

Methods

req :: Proxy ctx -> OpUpdate c l v ('(l', v') ': r) -> ReqR (OpUpdate c l v ('(l', v') ': r))

type ReqR (OpUpdate c l v ('[] :: [(k', k'')]))

Defined in Data.GenRec

type ReqR (OpUpdate c l v ('[] :: [(k', k'')])) = Rec c ('[] :: [(k', k'')])

type ReqR (OpUpdate c l v ('(l', v') ': r))

Defined in Data.GenRec

type ReqR (OpUpdate c l v ('(l', v') ': r))

update :: forall k c (l :: k) v (r :: [(k, Type)]) (ctx :: [ErrorMessage]). (Require (OpUpdate c l v r) ctx, WrapField c v ~ v) => Label l -> v -> Rec c r -> ReqR (OpUpdate c l v r)

The update function. Given a Label and value, and a Record containing this label, it updates the value. It could change its type. It raises a custom type error if there is no field labelled with l.

emptyGenRec :: forall k k' k'' (c :: k). Rec c ('[] :: [(k', k'')])

The empty Record. Note that it is polymorphic on the kind of record c.

module Data.GenRec.Label