5 ms·

Equational reasoning

82 points by svenkatesh 13y ago

ColinWright 13y ago
An excellent article, well worth the read. I would make one comment: In Haskell, when you see a single equals sign it means that the left-hand and right-hand side are substitutable for each other both ways. For example, if you see: x = 5 That means that wherever you see an x in your program, you can substitute it with a 5, and, vice versa, anywhere you see a 5 in your program you can substitute it with an x. This is missing a key term: "in scope." Apart from that, I'm going to re-read this several times. Thank you.
- sfvisser 13y ago
  > This is missing a key term: "in scope." True, of course. Sometimes I wish Haskell would have made shadowing variables into a compile error. Shadowing is the number one reason that substitution doesn't always work like you expect. (everyone please use -Wall) However, substitution also doesn't work sometimes because the types aren't polymorphic enough. Let bindings are monomorphic by default nowadays which can give some surprising results.
  - quchen 13y ago
    I guess shadowing produces warnings instead of errors is because sometimes it can be a good thing: you can use it to create the illusion of mutability. In GHC's source I've seen a couple of longer functions (say ~50 lines) that re-use names in let/bind "statements" to get around going from x to x'''; the "x" simply kept shadowing its previous value.
    - judk 13y ago
      Not just prettier, but it is more correct to shadow if your intent is to make the original x unavailable. It would be cleaner/safer if the language had a keyword like 'shadowlet'.
      - velis_vel 13y ago
        I've also done stuff like x <- m1; f x; x <- m 2; f x; in a do-block, and it's not clear to me how to write 'shadowfrom' (or however you pronounce '<-' in that context).
        judk 13y ago
        Maybe this would be cool: x! <- m 2 Sort of like a strictness annotation. In think it would be a compatible language change, since only identifiers can currently appear left of a <-
  - judk 13y ago
    It is isn't just shadowing. f1 = let x = 1 in x f2 = let x = 2 in x It would be insane to ban that in the name of "equational reasoning".
MaxGabriel 13y ago
Does an underscore at the end of the method signify anything in Haskell (eg replicateM_)?
- bstamour 13y ago
  Typically with monadic code, a function with an underscore at the end of its name discards it's effect. For example, the function mapM maps a function over a list, i.e. mapM :: Monad m => (a -> m b) -> [a] -> m [b] it returns the result of the computation. But sometimes you want to iterate over a list but discard the result (say you're printing elements.) mapM_ discards the result: mapM_ :: Monad m => (a -> m b) -> [a] -> m () where () denotes a kind of "null type". So if you want to store the results in a new list, you use mapM, but if you don't, and just want the "effects", you use mapM_. Here's an example of each, using the IO monad. If I have a list of numbers, and I want to iterate through each one and prompt the user for a multiplier, I would write the code like this: main = do let numbers = [1.. 10] numbers' <- forM numbers $ \n -> do putStrLn "Enter a multiplier" a <- getLine return $ n * (read a :: Int) where forM is just mapM with the arguments reversed to look more like a for-loop. Here I want the results of the computation, so I use forM. If, however I want to just print the numbers out, I'd use forM_ main = do let numbers = [1.. 10] forM_ numbers $ \n -> do putStrLn (show n)
  - MaxGabriel 13y ago
    Great explanation, thank you.
  - judk 13y ago
    To be clear (for readers, I know parent knows this), the return values of the effects are discarded. (The first sentence maybe should say "discard its results", not "discard it's effects"). The point is to make the (side-)effects happen (since non-strictness means the effects have to be forced, by calling `(>>=)` or similar) but not use the return value (which is how computations are usually forced in Haskell) And also, the effects happen in the order determined by the function forM_ or whoever, instead of in a hard-to-impossible-to-predict order of the pure non-monadic/non-effect computations defined by equations of function applications. (The M in fooM is for Monad, indicating that bind (f <<= x) is used instead of simple function application (f x) that is used in the "cousin" function foo. But that is just naming convention.)

82 points by svenkatesh 13y ago

An excellent article, well worth the read. I would make one comment: In Haskell, when you see a single equals sign it means that the left-hand and right-hand side are substitutable for each other both ways. For example, if you see: x = 5 That means that wherever you see an x in your program, you can substitute it with a 5, and, vice versa, anywhere you see a 5 in your program you can substitute it with an x. This is missing a key term: "in scope." Apart from that, I'm going to re-read this several times. Thank you.

sfvisser 13y ago
> This is missing a key term: "in scope." True, of course. Sometimes I wish Haskell would have made shadowing variables into a compile error. Shadowing is the number one reason that substitution doesn't always work like you expect. (everyone please use -Wall) However, substitution also doesn't work sometimes because the types aren't polymorphic enough. Let bindings are monomorphic by default nowadays which can give some surprising results.
- quchen 13y ago
  I guess shadowing produces warnings instead of errors is because sometimes it can be a good thing: you can use it to create the illusion of mutability. In GHC's source I've seen a couple of longer functions (say ~50 lines) that re-use names in let/bind "statements" to get around going from x to x'''; the "x" simply kept shadowing its previous value.
  - judk 13y ago
    Not just prettier, but it is more correct to shadow if your intent is to make the original x unavailable. It would be cleaner/safer if the language had a keyword like 'shadowlet'.
    - velis_vel 13y ago
      I've also done stuff like x <- m1; f x; x <- m 2; f x; in a do-block, and it's not clear to me how to write 'shadowfrom' (or however you pronounce '<-' in that context).
      - judk 13y ago
        Maybe this would be cool: x! <- m 2 Sort of like a strictness annotation. In think it would be a compatible language change, since only identifiers can currently appear left of a <-
- judk 13y ago
  It is isn't just shadowing. f1 = let x = 1 in x f2 = let x = 2 in x It would be insane to ban that in the name of "equational reasoning".

MaxGabriel 13y ago

Does an underscore at the end of the method signify anything in Haskell (eg replicateM_)?

bstamour 13y ago
Typically with monadic code, a function with an underscore at the end of its name discards it's effect. For example, the function mapM maps a function over a list, i.e. mapM :: Monad m => (a -> m b) -> [a] -> m [b] it returns the result of the computation. But sometimes you want to iterate over a list but discard the result (say you're printing elements.) mapM_ discards the result: mapM_ :: Monad m => (a -> m b) -> [a] -> m () where () denotes a kind of "null type". So if you want to store the results in a new list, you use mapM, but if you don't, and just want the "effects", you use mapM_. Here's an example of each, using the IO monad. If I have a list of numbers, and I want to iterate through each one and prompt the user for a multiplier, I would write the code like this: main = do let numbers = [1.. 10] numbers' <- forM numbers $ \n -> do putStrLn "Enter a multiplier" a <- getLine return $ n * (read a :: Int) where forM is just mapM with the arguments reversed to look more like a for-loop. Here I want the results of the computation, so I use forM. If, however I want to just print the numbers out, I'd use forM_ main = do let numbers = [1.. 10] forM_ numbers $ \n -> do putStrLn (show n)
- MaxGabriel 13y ago
  Great explanation, thank you.
- judk 13y ago
  To be clear (for readers, I know parent knows this), the return values of the effects are discarded. (The first sentence maybe should say "discard its results", not "discard it's effects"). The point is to make the (side-)effects happen (since non-strictness means the effects have to be forced, by calling `(>>=)` or similar) but not use the return value (which is how computations are usually forced in Haskell) And also, the effects happen in the order determined by the function forM_ or whoever, instead of in a hard-to-impossible-to-predict order of the pure non-monadic/non-effect computations defined by equations of function applications. (The M in fooM is for Monad, indicating that bind (f <<= x) is used instead of simple function application (f x) that is used in the "cousin" function foo. But that is just naming convention.)