poly-rec-0.7.0.0: Polykinded extensible records
Copyright(c) Juan García Garland
Marcos Viera 2019-2020
LicenseGPL
Maintainerjpgarcia@fing.edu.uy
Stabilityexperimental
PortabilityPOSIX
Safe HaskellSafe-Inferred
LanguageHaskell2010

Data.GenRec

Description

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.

Synopsis

Documentation

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

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

Instances details
(Show v, KnownSymbol l, Show (Record ('(l', v') ': r))) => Show (Record ('(l, v) ': ('(l', v') ': r))) Source # 
Instance details

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)]) Source # 
Instance details

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)])) Source # 
Instance details

Defined in Data.GenRec.RecInstances.Record

Methods

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

show :: Record '[] -> String #

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

type UnWrap (Rec c r) Source # 
Instance details

Defined in Data.GenRec

type UnWrap (Rec c r) = r

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

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 Source #

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

Instances

Instances details
type WrapField Reco (v :: Type) Source #

field type

Instance details

Defined in Data.GenRec.RecInstances.Record

type WrapField Reco (v :: Type) = v

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

The inverse of WrapField

Instances

Instances details
type UnWrap (Rec c r) Source # 
Instance details

Defined in Data.GenRec

type UnWrap (Rec c r) = r

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

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 Source #

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 Source #

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 Source #

.*. the pretty cons, hiding require

class OrdType k Source #

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

Instances details
OrdType Nat Source # 
Instance details

Defined in Data.GenRec.RecInstances.Record

Associated Types

type Cmp a b :: Ordering Source #

OrdType Symbol Source # 
Instance details

Defined in Data.GenRec

Associated Types

type Cmp a b :: Ordering Source #

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

Instances

Instances details
type Cmp (m :: Nat) (n :: Nat) Source # 
Instance details

Defined in Data.GenRec.RecInstances.Record

type Cmp (m :: Nat) (n :: Nat) = CmpNat m n
type Cmp (a :: Symbol) (b :: Symbol) Source # 
Instance details

Defined in Data.GenRec

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

type family ShowRec c :: Symbol Source #

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

Instances

Instances details
type ShowRec Reco Source #

Type level show utilities

Instance details

Defined in Data.GenRec.RecInstances.Record

type ShowRec Reco = "Record"

type family ShowField c :: Symbol Source #

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

Instances

Instances details
type ShowField Reco Source # 
Instance details

Defined in Data.GenRec.RecInstances.Record

type ShowField Reco = "field named "

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

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

Datatype for lookup (wrapper)

Constructors

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

Instances

Instances details
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 Source #

error instance (looking up an empty record)

Instance details

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 Source #

wrapper instance

Instance details

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')])) Source # 
Instance details

Defined in Data.GenRec

type ReqR (OpLookup c l ('[] :: [(k, k')])) = ()
type ReqR (OpLookup c l ('(l', v) ': r)) Source # 
Instance details

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) Source #

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 Source #

extension operator (wrapper)

Constructors

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

Instances

Instances details
Require (OpExtend c l v ('[] :: [(k, k')])) ctx Source #

extending an empty record

Instance details

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 Source #

wrapper instance

Instance details

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')])) Source # 
Instance details

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)) Source # 
Instance details

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 Source #

update operator (wrapper)

Constructors

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

Instances

Instances details
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 Source #

error instance

Instance details

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 Source #

wrapper instance

Instance details

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')])) Source # 
Instance details

Defined in Data.GenRec

type ReqR (OpUpdate c l v ('[] :: [(k, k')])) = Rec c ('[] :: [(Any :: Type, Any :: Type)])
type ReqR (OpUpdate c l v ('(l', v') ': r)) Source # 
Instance details

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) Source #

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'')]) Source #

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