Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Advanced interface (with a functor argument)
See Data.Record.Anon.Simple for the simple interface. You will probably also want to import Data.Record.Anon.
Intended for qualified import.
import Data.Record.Anon import Data.Record.Anon.Advanced (Record) import qualified Data.Record.Anon.Advanced as Anon
Synopsis
- data Record (f :: k -> Type) (r :: Row k)
- empty :: Record f '[]
- insert :: Field n -> f a -> Record f r -> Record f ((n := a) ': r)
- insertA :: Applicative m => Field n -> m (f a) -> m (Record f r) -> m (Record f ((n := a) ': r))
- applyPending :: Record f r -> Record f r
- get :: RowHasField n r a => Field n -> Record f r -> f a
- set :: RowHasField n r a => Field n -> f a -> Record f r -> Record f r
- project :: SubRow r r' => Record f r -> Record f r'
- inject :: SubRow r r' => Record f r' -> Record f r -> Record f r
- lens :: SubRow r r' => Record f r -> (Record f r', Record f r' -> Record f r)
- merge :: Record f r -> Record f r' -> Record f (Merge r r')
- map :: (forall x. f x -> g x) -> Record f r -> Record g r
- cmap :: AllFields r c => Proxy c -> (forall x. c x => f x -> g x) -> Record f r -> Record g r
- pure :: KnownFields r => (forall x. f x) -> Record f r
- cpure :: AllFields r c => Proxy c -> (forall x. c x => f x) -> Record f r
- ap :: Record (f -.-> g) r -> Record f r -> Record g r
- collapse :: Record (K a) r -> [a]
- toList :: KnownFields r => Record (K a) r -> [(String, a)]
- mapM :: Applicative m => (forall x. f x -> m (g x)) -> Record f r -> m (Record g r)
- cmapM :: (Applicative m, AllFields r c) => Proxy c -> (forall x. c x => f x -> m (g x)) -> Record f r -> m (Record g r)
- sequenceA :: Applicative m => Record (m :.: f) r -> m (Record f r)
- sequenceA' :: Applicative m => Record m r -> m (Record I r)
- distribute :: (Functor m, KnownFields r) => m (Record f r) -> Record (m :.: f) r
- distribute' :: (Functor m, KnownFields r) => m (Record I r) -> Record m r
- zip :: Record f r -> Record g r -> Record (Product f g) r
- zipWith :: (forall x. f x -> g x -> h x) -> Record f r -> Record g r -> Record h r
- zipWithM :: Applicative m => (forall x. f x -> g x -> m (h x)) -> Record f r -> Record g r -> m (Record h r)
- czipWith :: AllFields r c => Proxy c -> (forall x. c x => f x -> g x -> h x) -> Record f r -> Record g r -> Record h r
- czipWithM :: (Applicative m, AllFields r c) => Proxy c -> (forall x. c x => f x -> g x -> m (h x)) -> Record f r -> Record g r -> m (Record h r)
- reifyAllFields :: AllFields r c => proxy c -> Record (Dict c) r
- reflectAllFields :: Record (Dict c) r -> Reflected (AllFields r c)
- reifyKnownFields :: KnownFields r => proxy r -> Record (K String) r
- reflectKnownFields :: Record (K String) r -> Reflected (KnownFields r)
- data InRow (r :: Row k) (a :: k) where
- InRow :: forall k (n :: Symbol) (r :: Row k) (a :: k). (KnownSymbol n, RowHasField n r a) => Proxy n -> InRow r a
- reifySubRow :: (KnownFields r', SubRow r r') => Record (InRow r) r'
- reflectSubRow :: Record (InRow r) r' -> Reflected (SubRow r r')
- data SomeRecord (f :: k -> Type) where
- SomeRecord :: forall k (r :: Row k) (f :: k -> Type). KnownFields r => Record (Product (InRow r) f) r -> SomeRecord f
- someRecord :: [(String, Some f)] -> SomeRecord f
- letRecordT :: forall r f. (forall r'. Let r' r => Proxy r' -> Record f r) -> Record f r
- letInsertAs :: forall r r' f n a. Proxy r -> Field n -> f a -> Record f r' -> (forall r''. Let r'' ((n := a) ': r') => Record f r'' -> Record f r) -> Record f r
- castEqual :: Equal a b => a -> b
Documentation
data Record (f :: k -> Type) (r :: Row k) Source #
Anonymous record
Instances
Construction
insertA :: Applicative m => Field n -> m (f a) -> m (Record f r) -> m (Record f ((n := a) ': r)) Source #
Applicative insert
This is a simple wrapper around insert
, but can be quite useful when
constructing records. Consider code like
>>>
:{
example :: Applicative m => m a -> m b -> m (a, b) example ma mb = (,) <$> ma <*> mb :}
We cannot really extend this to the world of named records, but we can do something comparable using anonymous records:
>>>
:{
example :: Applicative m => m (f a) -> m (f b) -> m (Record f [ "a" := a, "b" := b ]) example ma mb = insertA #a ma $ insertA #b mb $ Prelude.pure empty :}
As for regular insert
, this example too can instead be written using
ANON_F
and sequenceA
(or sequenceA'
).
example ma mb = sequenceA $ ANON_F { a = Comp ma , b = Comp mb }
applyPending :: Record f r -> Record f r Source #
Apply all pending changes to the record
Updates to a record are stored in a hashtable. As this hashtable grows,
record field access and update will become more expensive. Applying the
updates, resulting in a flat vector, is an O(n)
operation. This will happen
automatically whenever another O(n)
operation is applied (for example,
mapping a function over the record). However, occassionally it is useful to
explicitly apply these changes, for example after constructing a record or
updating a lot of fields.
Field access
get :: RowHasField n r a => Field n -> Record f r -> f a Source #
Get field from the record
This is just a wrapper around getField
.
>>>
:{
example :: Record Maybe [ "a" := Bool, "b" := Int ] -> Maybe Bool example r = get #a r :}
If using record-dot-preprocessor
, you can also write this example as
example r = r.a
If the field does not exist, you will get a type error about an unsolvable
RowHasField
constraint:
>>>
:{
absentField :: Record Maybe [ "a" := Bool, "b" := Int ] -> Maybe Char absentField r = get #c r :} ... ...No instance for (RowHasField "c"... ...
Type mismatches will result in regular type errors:
>>>
:{
wrongType :: Record Maybe [ "a" := Bool, "b" := Int ] -> Maybe Char wrongType r = get #a r :} ... ...Couldn't match...Char...Bool... ...
When part of the record is not known, it might not be possible to resolve a
HasField
constraint until later. For example, in
>>>
:{
unknownField :: Record Maybe [ x := Bool, "b" := Int ] -> Maybe Int unknownField r = get #b r :} ... ...No instance for (RowHasField "b"... ...
(Note that x
here is a variable, not a string.) It is important that the
constraint remains unsolved in this example, because if x == "b"
, the first
field would shadow the second, and the result type should be Maybe Bool
instead of Maybe Int
.
set :: RowHasField n r a => Field n -> f a -> Record f r -> Record f r Source #
Update field in the record
This is just a wrapper around setField
.
>>>
:{
example :: Record Maybe [ "a" := Bool, "b" := Int ] -> Record Maybe [ "a" := Bool, "b" := Int ] example r = set #a (Just False) r :}
If using record-dot-preprocessor
, can also write this example as
example r = r{a = Just False}
Changing rows
project :: SubRow r r' => Record f r -> Record f r' Source #
Project from one record to another
Both the source record and the target record must be fully known.
The target record can omit fields from the source record, as well as rearrange them:
>>>
:{
example :: Record f [ "a" := Char, "b" := Int, "c" := Bool ] -> Record f [ "c" := Bool, "a" := Char ] example = project :}
Of course, it is not possible to add fields:
>>>
:{
example :: Record f [ "c" := Bool, "a" := Char ] -> Record f [ "a" := Char, "b" := Int, "c" := Bool ] example = project :} ... ...No instance for (SubRow... ...
Type inference will work through projections: field types are unified based on their name:
>>>
:{
example :: Record f [ "a" := Char, "b" := Int, "c" := Bool ] -> Record f [ "c" := _, "a" := Char ] example = project :} ... ...Found type wildcard...Bool... ...
inject :: SubRow r r' => Record f r' -> Record f r -> Record f r Source #
Inject smaller record into larger record
This is just the lens
setter.
merge :: Record f r -> Record f r' -> Record f (Merge r r') Source #
Merge two records
The Merge
type family does not reduce:
>>>
:{
example :: Record Maybe (Merge '[ "a" := Bool ] '[]) example = merge (insert #a (Just True) empty) empty :}
If you want to flatten the row after merging, you can use project
:
>>>
:{
example :: Record Maybe '[ "a" := Bool ] example = project $ merge (insert #a (Just True) empty) empty :}
HasField
constraints can be resolved for merged records, subject to the
same condition discussed in get
: all fields in the record must be fully
known:
>>>
:{
example :: Record f (Merge '[ "a" := Bool ] '[ "b" := Char ]) -> f Char example r = get #b r :}
If parts in the record are unknown we get type error:
>>>
:{
example :: Record I (Merge r '[ "b" := Char ]) -> I Char example r = get #b r :} ... ...No instance for (RowHasField "b"... ...
Combinators
" Functor "
cmap :: AllFields r c => Proxy c -> (forall x. c x => f x -> g x) -> Record f r -> Record g r Source #
Constrained form of map
" Applicable "
cpure :: AllFields r c => Proxy c -> (forall x. c x => f x) -> Record f r Source #
Constrained form of pure
" Foldable "
toList :: KnownFields r => Record (K a) r -> [(String, a)] Source #
Like collapse
, but also include field names
" Traversable "
mapM :: Applicative m => (forall x. f x -> m (g x)) -> Record f r -> m (Record g r) Source #
Analogue to mapM
cmapM :: (Applicative m, AllFields r c) => Proxy c -> (forall x. c x => f x -> m (g x)) -> Record f r -> m (Record g r) Source #
Constrained form of cmap
sequenceA' :: Applicative m => Record m r -> m (Record I r) Source #
Simplified form of sequenceA
distribute :: (Functor m, KnownFields r) => m (Record f r) -> Record (m :.: f) r Source #
Distribute
This is a higher kinded version of distribute
from
https://hackage.haskell.org/package/distributive, and inverse to
sequenceA
.
Be careful with this function: if f
allows effects, then those effects will
be duplicated whenever any field of the resulting record is accessed. Using
this with f == Vector
or f == Maybe
is fine, but you almost certainly
don't want to use it with f == IO
, for example.
distribute' :: (Functor m, KnownFields r) => m (Record I r) -> Record m r Source #
Simplified form of distribute
.
Zipping
zipWith :: (forall x. f x -> g x -> h x) -> Record f r -> Record g r -> Record h r Source #
Analogue of zipWith
zipWithM :: Applicative m => (forall x. f x -> g x -> m (h x)) -> Record f r -> Record g r -> m (Record h r) Source #
Analogue of zipWithM
czipWith :: AllFields r c => Proxy c -> (forall x. c x => f x -> g x -> h x) -> Record f r -> Record g r -> Record h r Source #
Constrained form of zipWith
czipWithM :: (Applicative m, AllFields r c) => Proxy c -> (forall x. c x => f x -> g x -> m (h x)) -> Record f r -> Record g r -> m (Record h r) Source #
Constrained form of zipWithM
Constraint reification and reflection
reifyAllFields :: AllFields r c => proxy c -> Record (Dict c) r Source #
Record of dictionaries
This reifies an AllFields
constraint as a record.
Inverse to reflectKnownFields
.
reflectAllFields :: Record (Dict c) r -> Reflected (AllFields r c) Source #
Establish AllFields
from a record of dictionaries
Inverse to reifyKnownFields
.
reifyKnownFields :: KnownFields r => proxy r -> Record (K String) r Source #
reflectKnownFields :: Record (K String) r -> Reflected (KnownFields r) Source #
Establish KnownFields
from a record of field names
Inverse to reifyAllFields
.
data InRow (r :: Row k) (a :: k) where Source #
InRow r a
is evidence that there exists some n
s.t. (n := a)
in r
.
InRow :: forall k (n :: Symbol) (r :: Row k) (a :: k). (KnownSymbol n, RowHasField n r a) => Proxy n -> InRow r a |
reifySubRow :: (KnownFields r', SubRow r r') => Record (InRow r) r' Source #
Record over r'
with evidence that every field is in r
.
This reifies a SubRow
constraint.
Inverse to reflectSubRow
.
reflectSubRow :: Record (InRow r) r' -> Reflected (SubRow r r') Source #
Establish SubRow
from a record of evidence.
Inverse to reifySubRow
.
Existential records
data SomeRecord (f :: k -> Type) where Source #
Discovered row variable
See someRecord
for detailed discussion.
SomeRecord :: forall k (r :: Row k) (f :: k -> Type). KnownFields r => Record (Product (InRow r) f) r -> SomeRecord f |
someRecord :: [(String, Some f)] -> SomeRecord f Source #
Construct record with existentially quantified row variable
Existentially quantified records arise for example when parsing JSON values
as records. Pattern matching on the result of someRecord
brings into scope
an existentially quantified row variable r
, along with a record over r
;
every field in record contains the value specified, as well as evidence that
that that field is indeed an element of r
.
For such a record to be useful, you will probably want to prove additional
constraints AllFields r c
; you can do this using reflectAllFields
,
provided that you carefully pick your f
such that you can define a function
fieldSatisfiesC :: forall c. f x -> Dict c x
for every c
you want to prove.
It is also possible to do a runtime check to see if the existential row r
can be projected to some concrete known row r'
. To do this, construct a
record of evidence with type
Record (InRow r) r'
and then call reflectSubRow
. To construct this record of evidence you will
need to do a runtime type check to verify that the types of the fields in
concrete row match the types of the corresponding fields in the inferred row
(the inferred row may contain fields that are not present in the concrete
row, of course). An obvious candidate for doing this is
Typeable
, but for specific applications (with specific
subsets of types of interest) other choices may be possible also.
The large-anon
test suite contains examples of doing both of these things;
see Test.Infra.DynRecord.Simple
(or Test.Infra.DynRecord.Advanced
for
rows over kind other than Type
) for examples of proving additional
constraints, and Test.Infra.Discovery
for an example of how you could do a
projection check.
Experimental integration with typelet
The typelet
plugin provides support for type sharing. These functions
can be used to construct records that result in ghc core that is truly
linear in size.
letRecordT :: forall r f. (forall r'. Let r' r => Proxy r' -> Record f r) -> Record f r Source #
Introduce type variable for a row
This can be used in conjunction with letInsertAs
:
>>>
:{
example :: Record I '[ "a" := Int, "b" := Char, "c" := Bool ] example = letRecordT $ \p -> castEqual $ letInsertAs p #c (I True) empty $ \xs02 -> letInsertAs p #b (I 'X' ) xs02 $ \xs01 -> letInsertAs p #a (I 1 ) xs01 $ \xs00 -> castEqual xs00 :}
:: forall r r' f n a. Proxy r | Type of the record we are constructing |
-> Field n | New field to be inserted |
-> f a | Value of the new field |
-> Record f r' | Record constructed so far |
-> (forall r''. Let r'' ((n := a) ': r') => Record f r'' -> Record f r) | Assign type variable to new partial record, and continue |
-> Record f r |
Insert field into a record and introduce type variable for the result