Getting some results

[treeowl]

When you want more than one result, but not all of them, things can be a tad awkward. First off, there's no native function to do that! An obvious one might be

splitUpTo :: Int -> SeqT m a -> m ([a], m a)

to get up to n results in a list. Another might get fancier with length-indexed vectors

data Vec n a where
  Nil :: Vec Z a
  Cons :: a -> Vec n a -> Vec (S n) a

splitExact :: SNat n -> SeqT m a -> m (Maybe (Vec n a, m a))

Stuff like that.

[dagit]

Actually, this should probably be added to PR #28 LogicT has a observeManyT if I recall correctly. Would that do what you want?

[dagit]

I should add, it's not a big deal with our monad to write this yourself, but in LogicT the Identity version can avoid msplit which gives them a big performance boost.

[treeowl]

Yes, we should have that, but I want splitAt, not just take. Ideally, I think, one version that produces its result in m and one that does so in SeqT m, much as we have both toView and msplit.

[treeowl]

Sure, it's just a convenience.

[dagit]

Ah, I see. So this is analogous to Data.List.splitAt where you get the tail. Yeah, think that's a good API addition.