parsonsmatt / prairie

First Class Record Fields in Haskell
BSD 3-Clause "New" or "Revised" License
17 stars 4 forks source link

Class method for monadic tabulation #15

Open mixphix opened 5 months ago

mixphix commented 5 months ago

The method tabulateRecordA is great for building a record from a structure of Applicative actions. But when the action is a Monad we have even more freedom: we can choose to delay the "glue" operation, whereas this is impossible in the general Applicative case.

decompose ::
  forall m f rec.
  (Record rec, Monad m, Applicative f) =>
  (Field rec ~> Compose m f) -> m (Field rec ~> f)
decompose r = do
  f0 <- r field0
  f1 <- r field1
  ...
  pure @m (\case fieldN -> fN) -- still untabulated!

Generating this function at compile-time would give users more control when creating records with actions. For example

cmdUser :: forall ty. Field User ty -> Compose IO Maybe ty
cmdUser = \case
  UserName -> Compose $ listToMaybe . words <$> getLine
  UserAge -> Compose $ readMaybe @Int <$> getLine

Then decompose cmdUser :: IO (forall ty. Field User ty -> Maybe ty) will first do all the IO actions to construct the record, before giving back the generic, untabulated accessor function. For Applicatives like Monoid m => Const m, this gives a way to refer to the specific Monoid element obtained for each field after performing the IO actions, but before combining them all into Const m rec during the tabulation.

This would require ImpredicativeTypes.

parsonsmatt commented 5 months ago

That is very interesting. I wonder if it is an expression of a more general form.

Let's assume newtype T f r = T (forall ty. Field r ty -> f r), just to condense things.

I think this does not require a Monad, Applicative ought to do fine. And - actually - I don't think you even need Applicative on the inner type to construct.

decompose :: (Applicative f, Record rec) => T (Compose f g) rec  -> f (T g rec)
decompose (T k) = liftAN mk (getCompose $ k field0) (getCompose $ k field1) ... (getCompose $ k fieldN)
  where
    mk f0 f1 f2 f3 ... fN = T \case
      -- etc...
      FieldN -> fN

If we abstract Compose f g and getCompose, then I think we have:

transmogrify
     :: (Applicative g, Record rec) 
    => (forall x. f x -> g (h x)) 
    -> T f rec  -> g (T h rec)
transmogrify run (T k) = liftAN mk (run $ k field0) (run $ k field1) ... (run $ k fieldN)
  where
    mk f0 f1 f2 f3 ... fN = T \case
      -- etc...
      FieldN -> fN

decompose :: (Applicative f, Record rec) => T (Compose f g) rec -> f (T g rec)
decompose = transmogrify getCompose 

Additionally - it is the newtype that makes Compose necessary at all.

decompose
    :: forall f g rec. (Applicative f, Record rec)
    => (forall ty. Field rec ty -> f (g ty))
    -> f (forall ty. Field rec ty -> g ty)
decompose k =
    (\g0 g1 -> \case
        Field0 -> g0
        Field1 -> g1
    ) <$> k Field0 <*> k Field1
mixphix commented 5 months ago

The newtype makes Compose necessary, but also obscures the polymorphism just enough to make the implementation work. Consider:

it "sequenceRecordA" $ do
    Cases user' <- do
        sequenceRecordA @User @IO @Maybe $ Cases \case
            UserName -> Compose do
                print 10 >> pure (Just "")
            UserAge -> Compose do
                print 20 >> pure Nothing
    user' UserName `shouldBe` Just ""
    user' UserAge `shouldBe` Nothing

Without the newtype (in this example Cases), GHC errors at user' <- about illegal polymorphic type variables and again at UserAge when failing to match String with Int due to the previous application to UserName. But with it, we can apply the user' function to any of its fields without complaint: user' really does have the type forall ty. Field User ty -> f ty.

I took the liberty of drafting the TH generation for sequenceRecordA here.

parsonsmatt commented 5 months ago

The extra fun thing about the newtype wrapper is that you can give it an instance HasField and use OverloadedRecordDot to index into it 😄

As much as I hate to admit it, bike shedding the name of the newtype is probably our barrier to getting this merged.