Monadic operations inside List.takeWhile

Stream: Is there code for X?

[Jeremy Salwen]

I am relatively new to functional programming, so maybe there is a trick here I am missing, but it seems like there is no way to use monadic functions as the condition in List.takeWhile?

I wrote the following function that works for me instead.

def List.takeWhileM {m : Type → Type} [Monad m]  {α} (p : α → m Bool) : List α → m (List α)
| [] => pure []
| (x :: xs) => do
  if ← p x then
    do let ys ← takeWhileM p xs
       pure (x :: ys)
  else
    pure []

But I was wondering if there is a standard way of doing this?

[Scott Morrison]

It seems to not exist yet (there is ListM.takeWhileM for monadic lazy lists). You could PR it!

[Scott Morrison]

You could inline the let.

[Scott Morrison]

And I think for consistency with other APIs you would have p : α → m (ULift Bool), so m can be universe polymorphic.

[Jeremy Salwen]

Scott Morrison said:

It seems to not exist yet (there is ListM.takeWhileM for monadic lazy lists). You could PR it!

To std, or mathlib?

[Mario Carneiro]

the std version would probably not be universe polymorphic if that means adding a ulift

[Eric Wieser]

Does std not have access to ulift?

[Mario Carneiro]

no, it's just a more awkward interface and I think that core usually doesn't do universe parametricity unless it is zero cost