Dropping fields in large-anon

[o1lo01ol1o]

When computing statistics over collections of anonymous records, it would be helpful to have a way to drop a field from a record without knowing the concrete row-type at compile time.

Say I wanted to compute group statistics: [Record I rs] -> (MonoidalMap k (Record (Mean 'Product' Count) rs'. If I know rs' then I can just specify what the row should be and use proejct. But, if i'd like to keep such a combinator around (I do), then I'd rather have::

groupBy' :: Field n -> (forall x. f x -> g x) -> Record f rs -> (f kn, Record g (DropField (n '=: kn) rs))
groupByField :: Field n -> (forall x. f x -> g x) -> t (Record f rs) -> MonoidalMap kn (Record g (DropField (n '=: kn) rs)

A cursory attempt at implementing DropField using first-class-families to filter the list yields a not unexpected occurrence of "the impossible":

<no location info>: error:
    panic! (the 'impossible' happened)
  GHC version 9.4.5:
        Unexpected KnownFields constraint with arguments:
Type
Eval
  (If
     (Eval
        (Not (TyEqImpl ("foo" ':= kv_akut[tau:0]) ("foo" ':= Text))))
     ((':) ("foo" ':= Text)
      <$> Filter
            (Not <=< TyEq ("foo" ':= kv_akut[tau:0]))
            '[ "bar" ':= Text, "date" ':= Day, "time" ':= Integer,
               ])
     (Filter
        (Not <=< TyEq ("foo" ':= kv_akut[tau:0]))
        '[ "bar" ':= Text, "date" ':= Day, "time" ':= Integer]))

What's the right way to implement it?

[edsko]

Hi Tim, nice to hear from you :) I'm not sure that what you're trying to do is possible (other than projecting out to a known record type again); I'm also not totally sure that it is not, but my intuition says no: large-anon is very much designed with the absence of any kind of induction principle (because type-level induction results in terrible compile time performance). So I guess the question here is: is there a design of your combinator that does not require you to specify the exact result type row?

[o1lo01ol1o]

Hi @edsko !

I had the opportunity to try a "quick" calculation that is usually the domain of libraries like Python's pandas (ie, aggregation and timeseries modeling on sets of tabular data) using large-anon. This ended up being mostly forms of map-reduce where you want to pull out the key, group, reduce and then either throw away the key or put it back in a field. You can't leave the key in the record because it can't be reduced in all cases.
I suppose I don't actually need to know the resulting row type provided I know that it does not contain a field. So in this case, it would suffice to be able to do delete :: (SubRow rs' rs, RowHasField n rs x) => Field n -> Record f rs -> Record f rs'

[edsko]

That function intuitively feels doable; would it be sufficient for you though? The SubRow constraint is satisfied for SubRow r r (it's not a "strict" subrow); so at the type-level you'd still not be guaranteed that the field does not exist. But perhaps that does not matter, necessarily?

[o1lo01ol1o]

I suspect it's good enough. What happens if insert #foo bar is called on a Record that already has Field 'foo' but we don't knot it from the type level?

[edsko]

It will simply override the existing field, so that should probably be fine?

[o1lo01ol1o]

If the value is gone in the term-level (and not adding GC pressure) and the user can't get hurt by not observing this fact at the type level then it should be fine.

[edsko]

Actually, considering this again, I was not thinking clearly enough. This type is not correct:

delete :: (SubRow rs' rs, RowHasField n rs x) => Field n -> Record f rs -> Record f rs'

because this claims that we can return a record for any choice of rs', as long as it is a sub-row of rs, but that clearly cannot be the case: then we could just pick rs itself (and then use composition with projection to get the more general type above); but that would result in a record which doesn't have the field anymore but yet the type claims that it does, which would then make get partial.

Conversely, we could say that it returns a Record f fs' for some rs' that happens to be a SubRow of rs, but in that case we can just pick rs' to be the empty record; that's not very useful either.

I guess we could have a function that returns a record for some rs' along with a function that can reconstruct a record of row rs if you provide that field again, but I'm not totally sure how useful that would be.

I knew there was a reason I hadn't implemented deletes yet 😬 If you have a specific proposal/implementation, I'd be happy to consider it, but I'm afraid I don't have spare capacity at the moment to think more about this now :(