Equational reasoning | Hacker News Reader

Equational reasoning

haskellforall.com

82 pointssvenkatesh13 comments

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.

> 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.

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.

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'.

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).

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 <-

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".

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

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)

Great explanation, thank you.

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.)

() is not null, it's the type that has only one value (think of it like Bool that's always True). Null (or C-void, which it is also often compared to) on the other hand stands for a lack of information and is more of a makeshift placeholder.

The semantics of (), a.k.a. unit, are effectively the same to those of null, and it can be useful to think of it that way. Both null and unit stand for lack of information and are placeholders. The difference is in the implementation details.

http://en.wikipedia.org/wiki/Unit_type

Reply on news.ycombinator.com