3 ms·
Can you expand on that?
by cannam 8y ago
Can you expand on that?
- kqr 8y agoI wish I could. Honestly! It's just that while I have experienced it firsthand, I have not spent enough time thinking about it and tinkering with it to be able to succinctly and accurately put into words what it is about. Some loose thoughts that may or may not make sense: - In Haskell, effectful computations (such as prints, variable updates, and so on) are first-class values (like integers, strings, and so on). This is the big idea. - When effectful computations are first-class values, you can store them in data structures like lists. You can associate them with keys in maps. You can even stick them in priority queues. - When effectful computations are first-class values, you can pass them around as arguments, or send them off as return values. - When effectful computations are first-class values, you can transform their results, you can chain them together and you can create branches in them. - When effectful computations are first-class values, you can perform them, then perform then again, then perform them 12 times, then discard them. Or discard them first and never perform them. - When effectful computations are first-class values, you have decoupled "describing the action" from "executing the action". You can handle the effectful computation without being afraid of performing the effect. - When description is decoupled from execution, you can abstract over the flow of control. You can have a loop that doesn't always increment its counter, because the incrementing operation is specified in a list somewhere instead. - Abstracting over the flow of control can be about as confusing as it is dynamic and powerful. It can also be the most clear and obvious solution to some problems. - Effectful computations as first-class values is a little like functions as first-class values: when you have tried it, you've found it's so convenient that you'd like to have it everywhere. (It's also a little like first-class functions in the sense that you can emulate first-class effects with first-class functions, but it easily becomes unwieldy.) - Effectful computations as first-class values is even a little like Lisp metaprogramming. In Lisp, the flow of control can be rewired dynamically, because the code itself is a Lisp data structure. In Haskell, the flow of control can be rewired dynamically, because statements don't have to be executed the second you see them. - The do notation, when used the traditional way, pulls a curtain over how effectful computations are first-class values. Computations in do notation are (to a first approximation) executed as soon as they are seen, because do notation was designed to intentionally hide the ways in which Haskell is a more powerful imperative language. Sorry if that made things even more confusing than it cleared up. ---- Here's the most basic concrete example I can think of: repeated = do { putStrLn "Hello"; putStrLn "Hello"; } Huh, the same action is performed two times. I guess I should put it in a variable. somewhatDRY = do { let greet = putStrLn "Hello"; -- not executed when put into variable greet; -- executed once here greet; -- and again here } Oh, the user wanted to specify how many greetings to print. countGreetings number = do { let greetings = -- infinite list of prints, repeat (putStrLn "Hello"); -- none of which is executed let enough = -- we take the first few prints, take number greetings; -- still without executing any sequenceA_ enough; -- now we execute just the first ones } Huh, I guess I don't even need the do notation anymore. countGreetings number = let greetings = repeat (putStrLn "Hello") enough = take number greetings in sequenceA_ enough ---- In these examples I used sequenceA_, which is a plain library function that takes a list of effectful computations and returns a single effectful computation. The effect of the returned computation is the same as if all the effectful computations in the list was called one after the other. I mention it's a plain library function because you wouldn't be able to define such a function – not even in the standard library – if effectful computations weren't first-class values... ---- I wrote a comment in the example saying "now we execute just the first ones". That's a lie, actually. Because like any effectful computation, also the return value of countGreetings is a first-class value. Meaning we could assign the return value of countGreetings to a variable, or stick it in a list, and so on, and nothing would be executed. In order to avoid uncomfortable déjà vu, I'll In order to avoid uncomfortable déjà vu, I'll just leave off here and conclude that when effectful computations are first-class values, there is, in a sense, two phases when the code is run. First there's an evaluation phase, where effectful computations are constructed and passed around. Then there's an execution phase, which actually executes these effects. If your effectful computation isn't hit by the execution phase, it will never be executed – no matter how many times the evaluation phase goes over it.
- cannam 8y agoThank you! This is a really nice comment that gives plenty to think about. It's delightful that, two days later, you actually have expanded in compelling detail on what initially looked to be something of a throwaway remark. I think that Idris tries to make the evaluation/execution distinction a bit more apparent. In particular, when you enter something effectful at the REPL, only the evaluation happens automatically and the result is printed in an internal form. This is confusing at first, but you can see that there's something tantalisingly interesting going on.
- kqr 8y agoNo problem whatsoever! I only wish I could have done it better. I do like the way the Idris REPL does that, from your description. Didn't know that. How do you run it for effects?
- cannam 8y agoUsing the :exec REPL command. Idris> putStrLn "Hello, world!" io_bind (prim_write "Hello, world!\n") (\__bindx => io_pure ()) : IO () Idris> :exec putStrLn "Hello, world!" Hello, world!