Zulip Chat Archive

Stream: general

Topic: Changing the monad


view this post on Zulip Koundinya Vajjha (Feb 21 2019 at 22:34):

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?

view this post on Zulip Kevin Buzzard (Feb 21 2019 at 23:01):

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

view this post on Zulip Kevin Buzzard (Feb 21 2019 at 23:02):

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

view this post on Zulip Chris Hughes (Feb 21 2019 at 23:21):

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

view this post on Zulip Koundinya Vajjha (Feb 21 2019 at 23:23):

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

view this post on Zulip Koundinya Vajjha (Feb 21 2019 at 23:23):

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

view this post on Zulip Koundinya Vajjha (Feb 21 2019 at 23:23):

But maybe they are different.


Last updated: May 18 2021 at 17:44 UTC