Lists as FAM's

Stream: new members

[lorã]

Hello!

I want to ask why Lists arnt instances of Monads or Applicatives anymore? i was trying to use the bind, but i saw that its deprecated. Thats some reason behind it? Also, i had to instanciate Lists as Applicatives in my own, but without lazy eval, shouldnt have only one choice?

instance : Applicative List where
  pure x := [x]
  seq fs u :=
    fs.flatMap (fun f => (u ()).map f)

I'm not sure if its 100% right.

Also, i would like to ask about the Unit -> f α in the seq.
(I'm really just trying to understand it, not to fight [i.e. sorry about my eng skills])

[Edward van de Meent]

for these instances, you need to import Mathlib.Data.List.Monad i think...

[lorã]

oh, im avoidint it because i dont know how to hide things yet

[Edward van de Meent]

lorã said:

Also, i had to instanciate Lists as Applicatives in my own, but without lazy eval, shouldnt have only one choice?

you can create another instance, it just might not allow you to create a LawfulApplicative instance, if i understand what you're asking

[Edward van de Meent]

also, even if there is just one choice, there might be different ways to phrase it leading to instances which are propositionally but not definitionally equal