Changing the monad

Stream: general

[Koundinya Vajjha]

I have a termns : list name, and a function foo : name -> tactic string. What I want is a term of type list (list string). Naturally, I want to use some sort of map to apply foo to every element of ns, but that gives me the wrong type. What do I do to get rid of the tactic monad?

[Kevin Buzzard]

Isn't it in general impossible to get out of a monad?

[Kevin Buzzard]

The tactic could fail; then there's no possibility for getting out

[Chris Hughes]

list.mmap might help. You'll end up with a tactic (list (list string))

[Koundinya Vajjha]

Yes I guess so. I figured it out - at any rate. Thanks!

[Koundinya Vajjha]

I thought that this was what the monad transformers were about.

[Koundinya Vajjha]

But maybe they are different.