← The refactoring catalogue · 1 of 35

Extract / Inline Method is the pair everyone learns first. Extract: find a region of a method body that does one nameable thing, move it into a new method, and replace the region with a call. Inline: take a call and replace it with the body of the method it names. Fowler’s 1999 catalogue gave Extract that name [1]; the second edition renamed it Extract Function, lists Inline Function as its inverse, and rewrote the mechanics for a language without classes [2]. The lineage is older. Griswold’s 1991 thesis treated restructuring as meaning-preserving manipulation of a program dependence graph, with a tool holding the semantics fixed while the programmer moved code about [4]. Opdyke’s 1992 thesis gave the first full treatment of “refactoring” for the object-oriented setting, and stated each operation as a transformation with explicit preconditions under which behaviour is preserved [3].

Motivation

The two directions answer different code smells, and the direction you choose records a judgement about the code. Extract when the same shape of work recurs in more than one place and the duplication would otherwise drift out of sync, each copy fixed separately; or when a method has grown so long that its single responsibility is no longer visible. Naming the region gives the recurring or the long shape a signature and a boundary of its own — it can be reused, tested and varied, and the reader no longer holds the whole method in their head.

Inline when the indirection costs more than it names. A method that exists only because some future boundary might need it is speculative generality: abstraction tax paid today for flexibility nobody uses. And a seam whose callers are coupled through its implementation rather than its contract hides nothing — the name adds a hop, not meaning. Inlining removes the hop and lets the body breathe into the caller, where the constants and structure the name kept apart become visible again.

Both languages here let a method nest inside the method that uses it, and that adds a third, finer judgement: where exactly the boundary falls. When you extract into a nested method, the values the region still sees from the enclosing scope simply stay in scope — they are captured, not passed — and only the values it needs from further out become the actual parameters. Choosing the scope of the extraction is therefore a judgement about which values should remain accessible and which should be made explicit, and the same region can be rendered with all of its dependencies in scope, or with some, or with none. The worst of the three looks like the same program with an extra name; the best gives the step function a boundary as sharp as a top-level one.

The move

Fowler’s mechanics are short: create a method named for what the region does, copy the region into it, pass the locals the region reads as parameters, return the locals it writes or refuse, replace the region with the call, test [1], [2]. “Refuse” is where the preconditions live. In an imperative language a region of statements is not a value; it is a sequence of effects on a mutable environment. The extracted method must see the same environment the region saw, hand back every change the rest of the method depends on, and run exactly as often, in the same position, as the region ran. A region that assigns two locals, or whose reads are interleaved with writes to the same fields elsewhere, cannot be lifted without changing the program. Fowler’s advice to reduce temps first pushes the code toward the case where extraction is safe; Opdyke’s precondition list makes the same demand formally [3]. Every automated refactoring tool since, including Stocker’s Scala refactoring library behind the Scala IDE [15], must perform exactly this analysis.

To and from

Extract / Inline method: one equation read in two directions. Left: f x = … e …. Right: g v = e and f x = … g v …. The free variables of e are the parameters v — except where the definition stays nested, in which case v is just what lies outside that nested scope. The arrow to the right is extract (fold, lambda-lift); the arrow to the left is inline (unfold, beta). before after f x = … e … g v = e f x = … g v … e: the region to extract free variables of e: v v: the parameters of g extract (define and fold / lambda-lift) inline (unfold and β-reduce / denest) v are the free variables of e; they become the parameters of g
The koan. One equation, read in two directions: extract (define and fold; lambda-lift, or simply nest the definition) to the right, inline (unfold and β-reduce; denest) to the left. The free variables of the region e become the parameters of a top-level definition — nested, they stay in the enclosing scope instead, and only what lies further out is passed.

The catalogue lists each refactoring in both directions because the two moves are one equation read left to right and right to left. For a definition f with parameters x₁ … xₙ and body e, f a₁ … aₙ equals e with each xᵢ replaced by aᵢ, provided no aᵢ is captured by a binder inside e. Read from application to body it is Inline: unfold, substitute, and if the arguments were variables the result is what stood there before. Read from body to application it is Extract: choose the region e, take its free variables as the xᵢ, and fold.

The directions serve different ends. Extract is for naming, so a reader sees what the region means rather than how; for reuse, so a second occurrence becomes a second call; and for generalisation, because once the free variables are parameters any of them can be varied and a specific expression becomes a function over a family. Inline is for specialisation, because unfolding at a call site with known arguments exposes constants and structure that further rewrites can act on, and for removing indirection that no longer earns its name. Burstall and Darlington’s system gets almost all of its power from alternating the two: unfold to expose a pattern, apply a law, fold to recover a recursion with a better shape [5]. A compiler’s simplifier works the unfolding half at scale [9]. The programmer works at a larger grain with a different objective, but the moves are the same moves.

Three examples

Each example is the same program twice, Before and After, in Scala 3 and in Haskell. The entry point keeps its name and its type, the extraction is the only difference, and a hedgehog property generates inputs and demands that both versions agree on every one of them. The sources below are included verbatim from the files the tests run against.

1 · Order total: the textbook move

A subtotal, a percentage discount, a percentage tax. The region amount × pct / 100 appears twice with different free variables, so it becomes percent(pct, amount); the line sum has no free variables beyond the list, so it becomes subtotal(items). Nothing in the region closes over anything the new functions cannot be handed as an argument.

Extracting subtotal and percent from total. Before: total(o) computes the line sum, the discount and the tax inline; the line sum and the two "amount times pct over 100" expressions are marked as regions. After: total(o) calls subtotal(items) with o.items, and percent(pct, amount) twice, with (o.discountPct, net) and (o.taxPct, discounted). before after total(o) = val subtotal = o.items.map(l => l.unitPrice * l.quantity).sum val discounted = subtotal - subtotal * o.discountPct / 100 discounted + discounted * o.taxPct / 100 total(o) = val net = subtotal(o.items) val discounted = net - percent(o.discountPct, net) discounted + percent(o.taxPct, discounted) subtotal(items) percent(pct, amount) 1 2 2 1 2 o.items o.discountPct, net o.taxPct, discounted

Before · Scala

// Total of an order: the lines summed, less a percentage discount, plus tax.
object Before:
  case class Line(unitPrice: Int, quantity: Int)
  case class Order(items: List[Line], discountPct: Int, taxPct: Int)

  def total(o: Order): Int =
    val subtotal   = o.items.map(l => l.unitPrice * l.quantity).sum
    val discounted = subtotal - subtotal * o.discountPct / 100
    discounted + discounted * o.taxPct / 100

Before · Haskell

-- Total of an order: the lines summed, less a percentage discount, plus tax.
module Before where

data Line  = Line  { unitPrice :: Int, quantity :: Int }
data Order = Order { items :: [Line], discountPct :: Int, taxPct :: Int }

total :: Order -> Int
total o = discounted + discounted * taxPct o `div` 100
  where
    subtotal   = sum [unitPrice l * quantity l | l <- items o]
    discounted = subtotal - subtotal * discountPct o `div` 100

After · Scala

// Total of an order: the lines summed, less a percentage discount, plus tax.
object After:
  case class Line(unitPrice: Int, quantity: Int)
  case class Order(items: List[Line], discountPct: Int, taxPct: Int)

  def total(o: Order): Int =
    val net        = subtotal(o.items)
    val discounted = net - percent(o.discountPct, net)
    discounted + percent(o.taxPct, discounted)

  def subtotal(items: List[Line]): Int =
    items.map(l => l.unitPrice * l.quantity).sum

  def percent(pct: Int, amount: Int): Int =
    amount * pct / 100

After · Haskell

-- Total of an order: the lines summed, less a percentage discount, plus tax.
module After where

data Line  = Line  { unitPrice :: Int, quantity :: Int }
data Order = Order { items :: [Line], discountPct :: Int, taxPct :: Int }

total :: Order -> Int
total o = discounted + percent (taxPct o) discounted
  where
    net        = subtotal (items o)
    discounted = net - percent (discountPct o) net

subtotal :: [Line] -> Int
subtotal ls = sum [unitPrice l * quantity l | l <- ls]

percent :: Int -> Int -> Int
percent pct amount = amount * pct `div` 100

Note what did not change: net is still bound once, so subtotal is still computed once. Extracting a function and then calling it twice would have been a second, different refactoring.

The property: Before.total == After.total on generated orders

Spec · Scala

//> using scala 3.3.4
//> using dep qa.hedgehog::hedgehog-core:0.14.0
//> using dep qa.hedgehog::hedgehog-runner:0.14.0
import hedgehog.*, hedgehog.core.*, hedgehog.runner.*

object Props extends Properties:
  def tests: List[Test] = List(
    property("total: Before == After", totalAgrees),
    property("no discount, no tax: total == subtotal", plainTotalIsSubtotal),
  )

  // Raw values, so the same input can be fed to both Before.Order and After.Order.
  val genLine: Gen[(Int, Int)] =
    for p <- Gen.int(Range.linear(-100, 1000)); q <- Gen.int(Range.linear(0, 20)) yield (p, q)
  val genOrder: Gen[(List[(Int, Int)], Int, Int)] =
    for
      items <- genLine.list(Range.linear(0, 10))
      d     <- Gen.int(Range.linear(0, 100))
      t     <- Gen.int(Range.linear(0, 30))
    yield (items, d, t)

  def totalAgrees: Property =
    for o <- genOrder.forAll
    yield
      val (items, d, t) = o
      Before.total(Before.Order(items.map(Before.Line(_, _)), d, t))
        ==== After.total(After.Order(items.map(After.Line(_, _)), d, t))

  def plainTotalIsSubtotal: Property =
    for items <- genLine.list(Range.linear(0, 10)).forAll
    yield
      val lines = items.map(After.Line(_, _))
      After.total(After.Order(lines, 0, 0)) ==== After.subtotal(lines)

@main def spec(): Unit =
  val results = Props.tests.map { t =>
    val r = Property.check(t.withConfig(PropertyConfig.default), t.result, Seed.fromTime())
    println(Test.renderReport("Props", t, r, ansiCodesSupported = false))
    r.status
  }
  if !results.forall(_ == Status.ok) then sys.exit(1)

Spec · Haskell

{-# LANGUAGE OverloadedStrings #-}
module Main where

import Control.Monad (unless)
import System.Exit (exitFailure)
import Hedgehog
import qualified Hedgehog.Gen as Gen
import qualified Hedgehog.Range as Range
import qualified Before
import qualified After

-- Raw values, so the same input can be fed to both Before.Order and After.Order.
genLine :: Gen (Int, Int)
genLine = (,) <$> Gen.int (Range.linear (-100) 1000) <*> Gen.int (Range.linear 0 20)

genOrder :: Gen ([(Int, Int)], Int, Int)
genOrder = (,,) <$> Gen.list (Range.linear 0 10) genLine
                <*> Gen.int (Range.linear 0 100)
                <*> Gen.int (Range.linear 0 30)

prop_total_agrees :: Property
prop_total_agrees = property $ do
  (items, d, t) <- forAll genOrder
  Before.total (Before.Order (map (uncurry Before.Line) items) d t)
    === After.total (After.Order (map (uncurry After.Line) items) d t)

prop_plain_total_is_subtotal :: Property
prop_plain_total_is_subtotal = property $ do
  items <- forAll (Gen.list (Range.linear 0 10) genLine)
  let ls = map (uncurry After.Line) items
  After.total (After.Order ls 0 0) === After.subtotal ls

main :: IO ()
main = do
  ok <- checkParallel $ Group "Props"
    [ ("total: Before == After", prop_total_agrees)
    , ("no discount, no tax: total == subtotal", prop_plain_total_is_subtotal)
    ]
  unless ok exitFailure

2 · Running balance: the region closes over locals

The fold’s step function reads limit and fee, which are parameters of settle. A top-level extraction would have to make those free variables leading parameters — Johnsson’s lambda lifting [6], and HaRe’s generalise definition [10]. But both languages also let the definition stay where it is used: step nests inside settle, limit and fee remain in scope and are captured, and only balance and tx — the values the fold supplies — become the parameters. This is the scope judgement from the Motivation section: the same region, extracted with its dependencies kept in scope instead of made explicit, earns a boundary of its own without giving its caller a new signature.

Extracting step from settle as a nested definition. Before: settle folds the transactions with an inline lambda whose free variables are limit and fee. After: step stays inside settle; limit and fee remain in scope and are captured, balance and tx are the parameters, and settle calls txs.foldLeft(opening)(step). before after settle(opening, limit, fee, txs) = txs.foldLeft(opening) { (balance, tx) => val next = balance + tx if tx < 0 && next < -limit then next - fee else next } free in the lambda: limit, fee settle(opening, limit, fee, txs) = def step(balance, tx) = val next = balance + tx if tx < 0 && next < -limit then next - fee else next txs.foldLeft(opening)(step) limit, fee — stay in scope, captured balance, tx — the fold's arguments 1 1 step

Before · Scala

// Closing balance after a run of transactions; a debit that leaves
// the account below its overdraft limit is charged a fee.
object Before:
  def settle(opening: Int, limit: Int, fee: Int, txs: List[Int]): Int =
    txs.foldLeft(opening) { (balance, tx) =>
      val next = balance + tx
      if tx < 0 && next < -limit then next - fee else next
    }

Before · Haskell

-- Closing balance after a run of transactions; a debit that leaves
-- the account below its overdraft limit is charged a fee.
module Before where

import Data.List (foldl')

settle :: Int -> Int -> Int -> [Int] -> Int
settle opening limit fee =
  foldl' (\balance tx ->
           let next = balance + tx
           in if tx < 0 && next < negate limit then next - fee
              else next)
        opening

After · Scala

// Closing balance after a run of transactions; `step` is extracted from
// the fold lambda and stays nested, capturing `limit` and `fee`.
object After:
  def settle(opening: Int, limit: Int, fee: Int, txs: List[Int]): Int =
    def step(balance: Int, tx: Int): Int =
      val next = balance + tx
      if tx < 0 && next < -limit then next - fee else next
    txs.foldLeft(opening)(step)

After · Haskell

-- Closing balance after a run of transactions; `step` is extracted from
-- the fold lambda and stays nested, capturing `limit` and `fee`.
module After where

import Data.List (foldl')

settle :: Int -> Int -> Int -> [Int] -> Int
settle opening limit fee =
  foldl' step opening
  where
    step balance tx =
      let next = balance + tx
      in if tx < 0 && next < negate limit then next - fee else next

Nesting keeps step private: callers of settle can observe only that the closing balance agrees with the unrefactored version — exactly what the single property checks. The inverse picture is Danvy and Schultz’s lambda dropping [7], restoring block structure by dropping parameters that are invariant across a call graph back into scope.

The property: Before.settle == After.settle on generated transaction runs

Spec · Scala

//> using scala 3.3.4
//> using dep qa.hedgehog::hedgehog-core:0.14.0
//> using dep qa.hedgehog::hedgehog-runner:0.14.0
import hedgehog.*, hedgehog.core.*, hedgehog.runner.*

object Props extends Properties:
  def tests: List[Test] = List(
    property("settle: Before == After", settleAgrees).withTests(500),
  )

  val genAmount: Gen[Int] = Gen.int(Range.linear(-30, 30))
  val genLimit: Gen[Int]  = Gen.int(Range.linear(0, 20))
  val genFee: Gen[Int]    = Gen.int(Range.linear(1, 20))

  def settleAgrees: Property =
    for
      opening <- genAmount.forAll
      limit   <- genLimit.forAll
      fee     <- genFee.forAll
      txs     <- genAmount.list(Range.linear(0, 20)).forAll
    yield Before.settle(opening, limit, fee, txs) ====
      After.settle(opening, limit, fee, txs)

@main def spec(): Unit =
  val results = Props.tests.map { t =>
    val r = Property.check(t.withConfig(PropertyConfig.default),
      t.result, Seed.fromTime())
    println(Test.renderReport("Props", t, r,
      ansiCodesSupported = false))
    r.status
  }
  if !results.forall(_ == Status.ok) then sys.exit(1)

Spec · Haskell

{-# LANGUAGE OverloadedStrings #-}
module Main where

import Control.Monad (unless)
import System.Exit (exitFailure)
import Hedgehog
import qualified Hedgehog.Gen as Gen
import qualified Hedgehog.Range as Range
import qualified Before
import qualified After

genAmount, genLimit, genFee :: Gen Int
genAmount = Gen.int (Range.linear (-30) 30)
genLimit  = Gen.int (Range.linear 0 20)
genFee    = Gen.int (Range.linear 1 20)

prop_settle_agrees :: Property
prop_settle_agrees = withTests 500 $ property $ do
  opening <- forAll genAmount
  limit   <- forAll genLimit
  fee     <- forAll genFee
  txs     <- forAll (Gen.list (Range.linear 0 20) genAmount)
  Before.settle opening limit fee txs ===
    After.settle opening limit fee txs

main :: IO ()
main = do
  ok <- checkParallel $ Group "Props"
    [ ("settle: Before == After", prop_settle_agrees)
    ]
  unless ok exitFailure

3 · Expression evaluator: extraction inside a recursive match

Three cases of a recursive evaluator share a shape: evaluate the left operand, then the right, then combine, with division by zero yielding no value rather than an exception. The shape becomes binary, parameterised by the combining operation. The one design decision is that binary takes the operands unevaluated: hand it eval(l) and eval(r) instead and Scala would evaluate the right operand even when the left one has no value, which Before never did. In Haskell the same choice keeps the short-circuit exact under laziness, and the second property checks it by putting undefined in the right operand. One partiality survives on both sides: Haskell’s div still overflows at minBound divided by -1. The refactoring preserves that; it does not fix it, and the property confirms that both versions throw on the same input.

Extracting binary from eval. Before: eval handles Add, Mul and Div with the same shape, for a from eval(l) and b from eval(r), differing only in the combining step. After: each case calls binary(l, r)(op) with the operands unevaluated and the combining step as op; binary evaluates l then r and applies op, calling back into eval. before after eval(e) = e match case Lit(n) => Some(n) case Add(l, r) => for a <- eval(l); b <- eval(r) yield a + b case Mul(l, r) => for a <- eval(l); b <- eval(r) yield a * b case Div(l, r) => for a <- eval(l); b <- eval(r); if b != 0 yield a / b the shape repeats three times; only the combining step differs, and it becomes op eval(e) = e match case Lit(n) => Some(n) case Add(l, r) => binary(l, r)((a, b) => Some(a + b)) case Mul(l, r) => binary(l, r)((a, b) => Some(a * b)) case Div(l, r) => binary(l, r)((a, b) => Option.when(b != 0)(a / b)) binary(l, r)(op) = for a <- eval(l); b <- eval(r) c <- op(a, b) yield c 1 1 1 1 l, r — the operands, unevaluated op — the combining step calls back: eval(l), eval(r)

Before · Scala

// Evaluate an arithmetic expression; division by zero has no value.
object Before:
  enum Expr:
    case Lit(n: Int)
    case Add(l: Expr, r: Expr)
    case Mul(l: Expr, r: Expr)
    case Div(l: Expr, r: Expr)
  import Expr.*

  def eval(e: Expr): Option[Int] = e match
    case Lit(n)    => Some(n)
    case Add(l, r) => for a <- eval(l); b <- eval(r) yield a + b
    case Mul(l, r) => for a <- eval(l); b <- eval(r) yield a * b
    case Div(l, r) => for a <- eval(l); b <- eval(r); if b != 0 yield a / b

Before · Haskell

-- Evaluate an arithmetic expression; division by zero has no value.
module Before where

data Expr = Lit Int | Add Expr Expr | Mul Expr Expr | Div Expr Expr
  deriving Show

eval :: Expr -> Maybe Int
eval (Lit n)   = Just n
eval (Add l r) = do
  a <- eval l
  b <- eval r
  Just (a + b)
eval (Mul l r) = do
  a <- eval l
  b <- eval r
  Just (a * b)
eval (Div l r) = do
  a <- eval l
  b <- eval r
  if b == 0 then Nothing else Just (a `div` b)

After · Scala

// Evaluate an arithmetic expression; division by zero has no value.
object After:
  enum Expr:
    case Lit(n: Int)
    case Add(l: Expr, r: Expr)
    case Mul(l: Expr, r: Expr)
    case Div(l: Expr, r: Expr)
  import Expr.*

  def eval(e: Expr): Option[Int] = e match
    case Lit(n)    => Some(n)
    case Add(l, r) => binary(l, r)((a, b) => Some(a + b))
    case Mul(l, r) => binary(l, r)((a, b) => Some(a * b))
    case Div(l, r) => binary(l, r)((a, b) => Option.when(b != 0)(a / b))

  // Takes the operands unevaluated, so the right one is still only evaluated
  // when the left one has a value, exactly as in Before.
  def binary(l: Expr, r: Expr)(op: (Int, Int) => Option[Int]): Option[Int] =
    for a <- eval(l); b <- eval(r); c <- op(a, b) yield c

After · Haskell

-- Evaluate an arithmetic expression; division by zero has no value.
module After where

data Expr = Lit Int | Add Expr Expr | Mul Expr Expr | Div Expr Expr
  deriving Show

eval :: Expr -> Maybe Int
eval (Lit n)   = Just n
eval (Add l r) = binary (\a b -> Just (a + b)) l r
eval (Mul l r) = binary (\a b -> Just (a * b)) l r
eval (Div l r) = binary (\a b -> if b == 0 then Nothing else Just (a `div` b)) l r

-- Takes the operands unevaluated, so the right one is still only forced
-- when the left one has a value, exactly as in Before.
binary :: (Int -> Int -> Maybe Int) -> Expr -> Expr -> Maybe Int
binary op l r = do
  a <- eval l
  b <- eval r
  op a b
The property: Before.eval == After.eval on generated trees, and the short-circuit survives

Spec · Scala

//> using scala 3.3.4
//> using dep qa.hedgehog::hedgehog-core:0.14.0
//> using dep qa.hedgehog::hedgehog-runner:0.14.0
import hedgehog.*, hedgehog.core.*, hedgehog.runner.*

object Props extends Properties:
  def tests: List[Test] = List(
    property("eval: Before == After", evalAgrees),
    property("dividing by zero has no value, never throws", divByZeroIsNone),
  )

  import Before.Expr, Before.Expr.*

  val genLit: Gen[Expr] = Gen.int(Range.linear(-20, 20)).map(Lit(_))
  def genExpr(depth: Int): Gen[Expr] =
    if depth == 0 then genLit
    else
      val sub = genExpr(depth - 1)
      Gen.choice1(
        genLit,
        for l <- sub; r <- sub yield Add(l, r),
        for l <- sub; r <- sub yield Mul(l, r),
        for l <- sub; r <- sub yield Div(l, r),
      )

  def toAfter(e: Expr): After.Expr = e match
    case Lit(n)    => After.Expr.Lit(n)
    case Add(l, r) => After.Expr.Add(toAfter(l), toAfter(r))
    case Mul(l, r) => After.Expr.Mul(toAfter(l), toAfter(r))
    case Div(l, r) => After.Expr.Div(toAfter(l), toAfter(r))

  def evalAgrees: Property =
    for e <- genExpr(4).forAll
    yield Before.eval(e) ==== After.eval(toAfter(e))

  def divByZeroIsNone: Property =
    for e <- genExpr(3).forAll
    yield Before.eval(Div(e, Lit(0))) ==== None and After.eval(toAfter(Div(e, Lit(0)))) ==== None

@main def spec(): Unit =
  val results = Props.tests.map { t =>
    val r = Property.check(t.withConfig(PropertyConfig.default), t.result, Seed.fromTime())
    println(Test.renderReport("Props", t, r, ansiCodesSupported = false))
    r.status
  }
  if !results.forall(_ == Status.ok) then sys.exit(1)

Spec · Haskell

{-# LANGUAGE OverloadedStrings #-}
module Main where

import Control.Monad (unless)
import System.Exit (exitFailure)
import Hedgehog
import qualified Hedgehog.Gen as Gen
import qualified Hedgehog.Range as Range
import qualified Before
import qualified After

genExpr :: Gen Before.Expr
genExpr = Gen.recursive Gen.choice
  [ Before.Lit <$> Gen.int (Range.linear (-20) 20) ]
  [ Gen.subterm2 genExpr genExpr Before.Add
  , Gen.subterm2 genExpr genExpr Before.Mul
  , Gen.subterm2 genExpr genExpr Before.Div
  ]

toAfter :: Before.Expr -> After.Expr
toAfter (Before.Lit n)   = After.Lit n
toAfter (Before.Add l r) = After.Add (toAfter l) (toAfter r)
toAfter (Before.Mul l r) = After.Mul (toAfter l) (toAfter r)
toAfter (Before.Div l r) = After.Div (toAfter l) (toAfter r)

prop_eval_agrees :: Property
prop_eval_agrees = property $ do
  e <- forAll genExpr
  Before.eval e === After.eval (toAfter e)

-- A left operand without a value short-circuits: the right operand is never
-- forced, before and after. (Division by zero has no value, so it does not throw here.)
prop_short_circuit_preserved :: Property
prop_short_circuit_preserved = property $ do
  e <- forAll genExpr
  Before.eval (Before.Add (Before.Div e (Before.Lit 0)) undefined) === Nothing
  After.eval (After.Add (After.Div (toAfter e) (After.Lit 0)) undefined) === Nothing

main :: IO ()
main = do
  ok <- checkParallel $ Group "Props"
    [ ("eval: Before == After", prop_eval_agrees)
    , ("short-circuit on a valueless left operand is preserved", prop_short_circuit_preserved)
    ]
  unless ok exitFailure

Pitfalls

The equation has hypotheses, and each is one of the constructive criteria. Where a hypothesis fails, extraction changes the program. In a language with referential transparency the OO precondition does not become easier to satisfy; it disappears, and the move becomes an equation. The structures that make that true are gathered in the footnote at the end of this section.

  • Side effects and evaluation order. If the region performs effects, moving it into a definition can change when and how often they happen. This is the OO precondition, and the only one imperative languages need because it subsumes the rest. In Scala a def is re-evaluated at each call and a val once, so extracting an effectful expression into a def can multiply effects, and into a val can move them to initialisation.
  • Sharing and evaluation count. In a pure language the value is the same but the work may not be. A Scala def recomputes; a val shares. In Haskell a let-bound expression is evaluated at most once per binding, a top-level constant applicative form is shared for the program’s lifetime, and a function body is recomputed per call unless full laziness floats it out [8]. Extraction can change space and time, including turning a bounded computation into a leak, without changing the result.
  • Strictness. A definition that pattern-matches on a parameter forces it when applied, even if the original expression only used it in a branch not taken. Extraction can introduce a force and inlining remove one; where the argument is bottom the two programs differ. Totality, no undefined and no partial functions, is exactly the condition under which this cannot arise. Example 3 is built around this.
  • Exceptions and non-termination. An expression that throws or diverges is a value only in a language that models those outcomes as values. If the region can throw and the call site evaluates it in a different order, the exception observed changes; if it can diverge, the strictness argument applies. Termination removes the second case, total error handling the first.
  • Name capture. Substituting the body for the call, or lifting the region past a binder, must not let a free variable of the region be captured by an inner binding of the same name. Tools rename; by hand this is the commonest way to make Inline wrong. A type checker catches most captures, since a captured variable usually has the wrong type, but not all.

In each case the fix is the same: restore the hypothesis, by making the region pure, total and terminating and by renaming, or admit that this is not a refactoring and test it as a change.

The functional reading

In a referentially transparent language the region is an expression, and an expression depends only on its free variables. Extracting it means naming it: write a definition whose parameters are the free variables of the region and whose body is the region, then replace the region with an application of the new name to those variables. There is no environment to rebuild because there is no environment; the free variables are the whole of what the expression could see, and the type checker tells you what they are.

This is not a new idea dressed up. It is the abstraction step of Burstall and Darlington’s 1977 fold/unfold system, where a program is a set of equations and the permitted moves are to define a new equation, to unfold a call by replacing it with its right-hand side, and to fold a sub-expression back into a call wherever it matches one [5]. Extract is definition followed by fold; Inline is unfold. Johnsson’s lambda lifting, which turns nested local functions into top-level equations by adding their free variables as parameters, is extraction pushed to the whole program [6]; Danvy and Schultz’s lambda dropping is the inverse, restoring block structure by dropping parameters that are invariant across a call graph back into scope [7]. Let-floating in GHC moves bindings inward or outward for sharing and allocation, relying on the same fact that a binding may be placed anywhere its free variables are in scope [8]. And GHC’s inliner performs the inverse of extraction thousands of times a build, unfolding and beta-reducing wherever the result is smaller or faster; Peyton Jones and Marlow’s account of it is, read from the other side, an account of when extraction costs nothing at runtime [9].

The Haskell Refactorer, HaRe, offers the pair as tool operations: introduce definition, which names a selected sub-expression; generalise definition, which turns a sub-expression into a parameter; and unfold, which replaces a call with the body [10], [11]. Thompson’s Advanced Functional Programming lecture notes set these out as equations between programs and discuss where the equations hold [12].

That is the point. With referential transparency the OO precondition does not become easier to satisfy; it disappears, because the transformation is an instance of the language’s own equational theory. Replacing an expression with a name bound to it is the beta rule read backwards. Extraction stops being something you hope preserved behaviour and becomes an equation you wrote down.

Verification

Because extraction is an equation, its correctness is a property: for all inputs x in the domain of the entry point, Before x == After x. That is a one-line property in the sense Claessen and Hughes introduced with QuickCheck, where a generator produces inputs and the framework searches for a counterexample and shrinks it to a minimal one [13]. The catalogue states every entry this way, in Scala and in Haskell, with hedgehog on both sides [14]. Hedgehog is used because its shrinking is integrated into the generator, so a shrunk counterexample obeys the same invariants as a generated one and the minimal failing input it reports is a real input of the program, not an artefact of a separate shrinker.

A property is only worth having if it can fail, so each spec above was mutation-checked: change After so it is no longer equivalent, by dropping a parameter, altering a boundary or reordering a match, confirm the property reports and shrinks a counterexample, then restore After. A property that does not fail under mutation is testing the generator, not the refactoring.

To run everything on this page yourself, from a checkout of the site repository:

sh pages/refactorings/extract-method/run.sh

It needs scala-cli and either GHC with hedgehog installed or Docker, and ends with all properties passed.

References

  1. Martin Fowler, with contributions by Kent Beck, John Brant, William Opdyke and Don Roberts. Refactoring: Improving the Design of Existing Code. Addison-Wesley, 1999. https://martinfowler.com/books/refactoring.html
  2. Martin Fowler. Refactoring: Improving the Design of Existing Code, second edition. Addison-Wesley, 2018. Catalogue entry “Extract Function” (formerly Extract Method; inverse of Inline Function). https://refactoring.com/catalog/extractFunction.html
  3. William F. Opdyke. Refactoring Object-Oriented Frameworks. PhD thesis, University of Illinois at Urbana-Champaign, 1992 (Tech. Report UIUCDCS-R-92-1759). https://www.laputan.org/pub/papers/opdyke-thesis.pdf
  4. William G. Griswold. Program Restructuring as an Aid to Software Maintenance. PhD thesis, University of Washington, 1991. Technical report 91-08-04. https://cseweb.ucsd.edu/~wgg/Abstracts/gristhesis.pdf
  5. R. M. Burstall and John Darlington. “A Transformation System for Developing Recursive Programs”. Journal of the ACM 24(1):44–67, 1977. https://doi.org/10.1145/321992.321996
  6. Thomas Johnsson. “Lambda Lifting: Transforming Programs to Recursive Equations”. In Functional Programming Languages and Computer Architecture (FPCA 1985), LNCS 201, pp. 190–203. Springer, 1985. https://doi.org/10.1007/3-540-15975-4_37
  7. Olivier Danvy and Ulrik P. Schultz. “Lambda-dropping: transforming recursive equations into programs with block structure”. Theoretical Computer Science 248(1–2):243–287, 2000. https://www.sciencedirect.com/science/article/pii/S0304397500000542
  8. Simon Peyton Jones, Will Partain and André Santos. “Let-floating: moving bindings to give faster programs”. In Proceedings of the ACM SIGPLAN International Conference on Functional Programming (ICFP 1996), pp. 1–12. https://doi.org/10.1145/232627.232630
  9. Simon Peyton Jones and Simon Marlow. “Secrets of the Glasgow Haskell Compiler inliner”. Journal of Functional Programming 12(4–5):393–434, 2002. https://doi.org/10.1017/S0956796802004331
  10. Huiqing Li, Claus Reinke and Simon Thompson. “Tool support for refactoring functional programs”. In Proceedings of the ACM SIGPLAN Workshop on Haskell (Haskell 2003), pp. 27–38. https://doi.org/10.1145/871895.871899
  11. Huiqing Li, Simon Thompson and Claus Reinke. “The Haskell Refactorer, HaRe, and its API”. Electronic Notes in Theoretical Computer Science 141(4):29–34, 2005 (LDTA 2005). https://doi.org/10.1016/j.entcs.2005.02.053
  12. Simon Thompson. “Refactoring Functional Programs”. In Advanced Functional Programming (AFP 2004), Revised Lectures, LNCS 3622, pp. 331–357. Springer, 2005. https://doi.org/10.1007/11546382_9
  13. Koen Claessen and John Hughes. “QuickCheck: a lightweight tool for random testing of Haskell programs”. In Proceedings of the ACM SIGPLAN International Conference on Functional Programming (ICFP 2000), pp. 268–279. https://doi.org/10.1145/351240.351266
  14. Jacob Stanley and contributors. Hedgehog: release with confidence, state-of-the-art property testing. https://github.com/hedgehogqa/haskell-hedgehog and https://github.com/hedgehogqa/scala-hedgehog
  15. Mirko Stocker. Scala Refactoring. Master’s thesis, HSR Hochschule für Technik Rapperswil, 2010. https://eprints.ost.ch/id/eprint/286/