Copyright	(c) Juan García Garland Marcos Viera 2019-2020
License	GPL
Maintainer	jpgarcia@fing.edu.uy
Stability	experimental
Portability	POSIX
Safe Haskell	Safe-Inferred
Language	Haskell2010

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

data Rec (c :: k) (r :: [(k', k'')]) :: Type where
- EmptyRec :: Rec c '[]
- ConsRec :: TagField c l v -> Rec c r -> Rec c ('(l, v) ': r)
data TagField (c :: k) (l :: k') (v :: k'') where
- TagField :: Label c -> Label l -> WrapField c v -> TagField c l v
type family WrapField (c :: k') (v :: k) :: Type
type family UnWrap (t :: Type) :: [(k, k')]
untagField :: TagField c l v -> WrapField c v
(.=.) :: forall k' k k'' (l :: k') (c :: k) (v :: k''). Label l -> WrapField c v -> TagField c l v
(#) :: forall c l r ctx v. RequireR (OpLookupCall c l r) ctx v => Rec c r -> Label l -> v
(.*.) :: 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)
class OrdType k
type family Cmp (a :: k) (b :: k) :: Ordering
type family ShowRec c :: Symbol
type family ShowField c :: Symbol
type family ShowLabel (l :: k) :: Symbol
data OpLookup (c :: Type) (l :: k) (r :: [(k, k')]) :: Type where
- OpLookup :: Label l -> Rec c r -> OpLookup c l 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)
data OpExtend (c :: Type) (l :: k) (v :: k') (r :: [(k, k')]) :: Type where
- OpExtend :: Label l -> WrapField c v -> Rec c r -> OpExtend c l v r
data OpUpdate (c :: Type) (l :: k) (v :: k') (r :: [(k, k')]) :: Type where
- OpUpdate :: Label l -> WrapField c v -> Rec c r -> OpUpdate c 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)
emptyGenRec :: forall k k' k'' (c :: k). Rec c ('[] :: [(k', k'')])
module Data.GenRec.Label

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 #

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 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.

module Data.GenRec.Label