@typeswitch @mcc that will in fact work, but i thought the do notation version might be less cryptic.
0 Boosts
0 Likes
@mcc @typeswitch i had hoped you'd come to do x <- xs; y <- ys; pure (x,y)
@dysfun @typeswitch but then there's some entirely other thing, somewhere else, that I have to do to put this in List Monad, right? Is it enough to assign the result to a `List a` and that puts it into List Context? Geez this is just Perl
@mcc @dysfun @typeswitch > Geez this is just Perl
yes. that's what makes it good 😉 lmao (at least, that's what I most like about Haskell, Idris and Perl)
@dysfun @typeswitch i'm going to be honest you said that and i spent 20 minutes looking at https://idris2.readthedocs.io/en/latest/tutorial/interfaces.html#monads-and-do-notation and trying to understand what on *earth* you could have possibly meant. to me "do" is a mysterious magic thing that has special cased behavior for <- and newline. So "do and two lists" could mean do a;b; it could mean… i don't know, a lot of things. do is not a higher-order function of three arguments, such like I could have used the type to derive what order I write things in.
Interfaces — Idris 2.0 Documentation