An experimental module for splitting a borrow of a record gradually and partially. To be used when you need to access more than one fields of a borrowed record, and borrow-out each field as you go. If you can just pattern match on the record borrow once, consider using Data.Record.Linear.Borrow.Experimental.PatternMatch.

The API is subject to future change.

Overview

(.#) is handy when you need only one field of a borrowed record, but not applicable when you need to access more than one fields. For that purpose, we provide SplitRecord machinery and associated combinators (-#), (+#), and (!#) for splitting a borrow of a record into borrows of its fields.

In such cases, however, we must ensure that each field of a record borrow is split out at most once. Here, SplitRecord a bk α fs comes int play: it is representationally same as Borrow bk α a, but only the fields in fs remains unsplit. That is, a field is borrowed by splitting combinator only if it remains in fs type parameter, and the field is removed from fs after splitting.

A record type can be converted into a SplitRecord by splitRecord function, which requires SplittableRecord instance for the record type. This can be derived generically by deriving Generic and then SplittableRecord for the record type, as follows:

{-# LANGUAGE TemplateHaskell, DataKinds, TypeFamilies, LinearTypes #-}
import Generics.Linear.TH (deriveGeneric)

data MyRecord = MyRecord {field :: Ref Int, otherField :: Vector String}

deriveGeneric ''MyRecord

deriving anyclass instance SplittableRecord MyRecord

Once we have SplittableRecord instance derived, we can now split a record borrow partially, step-by-step using (-#), (+#), and (!#) combinators. Through out this documentation, suppose we have the following record borrow in scope:

recordBor :: Mut α MyRecord

splitRec ::
  SplitRecord MyRecord Mut α
      '[ '("field", '( 'One, Ref Int)), '("otherField", '( 'One, Vector String))]
splitRec = splitRecord recordBor

Borrows-out a linear field

When you want to borrow-out a single linear field from the record, you can use (-#) combinator, as follows:

fieldBor :: Mut α (Ref Int)
restBor :: SplitRecord MyRecord Mut α '[ '(otherField, '( 'One, Vector String)))]
(fieldBor, restSplit) = splitRec -# #field

Here, the borrow to the field of splitRec is borrowed out as fieldBor, and the remaining borrow is represented by restSplit, where only otherField remain unsplit. We can no longer borrow-out field from restSplit by the type constraints.

Consuming a split record

When you no longer need to borrow any field of a split record, you can just consume a split record, or call (!#) to borrow out a single field from the split record and discard the rest of the record borrow, as follows:

otherFieldBor :: Mut α (Vector String)
otherFieldBor = restSplit !# #otherField

(!#) is analogous to (.#), but it acts on SplitRecord instead of borrow of a record.