Refactoring With Equational Reasoning

While working on a project today, a particular pattern kept coming up:

g :: Wallet -> Taco

f :: Reader Wallet Taco
f = do
  val <- ask
  return $ g val

I suspected a refactoring to a more succinct applicative-style existed. I tinkered with types¹ for a bit until I arrived at:

f :: Reader Wallet Taco
f = g <$> ask

This works, and I scratched my head for part of the day as to the why of this. I dug a bit into the laws relating Monad, Functor, and Applicative and found the bits I needed. In the end, I was able to use equational reasoning to show how I got from the do-style implementation to the applicative-style one. That process is shown below.

Some Scratch Paper

-- laws/assumptions:
  fmap f g = g >>= return . f -- (1)
  fmap = (<$>)  -- (2)
  do {g <- f; return g;} = f >>= (\g -> return g)

By browsing through the Typeclassopedia, I was able to find laws (1) and (2) above.

The last “law” is a do-style desugaring. That transformation is described in the Haskell Standard.

A note about (1) and (2): they are not enforced by the Haskell type system. It’s up to us to enforce them by convention and property tests. As long as the laws are upheld by a particular data type, the refactoring I’m writing about works.²

Where Are We Going?

Here’s a review of the starting point and the goal:

-- start: indented, as usually seen
do
  y <- ask
  return (x + y)

-- start: in one line, convenient for what follows
do {y <- ask; return (x + y);}

-- end: succinct
(x+) <$> ask

There’s a subtle benefit (?) to this refactoring, aside from the succinctness. The refactored version uses a weaker set of constraints, e.g., Functor rather than Monad. I admit I don’t fully understand the implications of this benefit. Possibly more on this later.

Equational Reasoning Put to Work

Below’s a chain of transformations consisting of valid Haskell code that take us from start to end. As noted above, they depend on (1) and (2) being true, which are not enforced by the type system.

-- start
start :: Int -> Reader Int Int
start x = do {y <- ask; return (x + y);}

-- end
end :: Int -> Reader Int Int
end x = (x+) <$> ask

-- proof: every step type checks
start' x = do {y <- ask; return (x + y);}
s1 x = ask >>= (\y -> return (x + y))    -- do-notation desugaring
s2 x = ask >>= (\y -> return ((x+) y))   -- currying, sections
s3 x = ask >>= (\y -> (return . (x+)) y) -- compose, preserving types
s4 x = ask >>= (return . (x+))           -- eta reduction
s5 x = fmap (x+) ask                     -- first law
s6 x = (<$>) (x+) ask                    -- second law
end x = (x+) <$> ask                     -- infix operator sugar

Conclusions

This was a fun exercise for me. Technicalities aside, I have a personal preference for applicative style. I learned a great deal about working with applicatives while practicing with Haskell parser code, namely, log parsing with attoparsec. I’ve found a similar flavor of this particular refactoring to be handy in that domain. Here’s an example I’ve hosted in a gist.

Also, this was my first attempt at carrying out a proof of sorts by relying on the Haskell type system. The parts of the code I was not able to prove correct were the laws we depended on (1) and (2). In practice, this is usually fine as the conventions around these laws are pretty strong. Yet, tt makes me just a bit more curious about Idris and others.

–