Обсудим стратегию вычислений в Haskell.

Большинство языков программирования используют строгую модель вычислений. Haskell использует нестрогие вычисления (иногда называемые “ленивыми”).

На базовом уровне, нестрогие вычисления означают, что большинство выражений вычисляются только при необходимости. Когда процесс вычисления начинается, для каждого выражения создаётся “задумка” (thunk – иногда можно встретить кальку “санк” или “занк”, реже “клауза”; устоявшегося перевода видимо пока нет). “Задумку” можно представить как инструкцию для вычисления и область памяти для хранения результата этого вычисления в графе вычисления программы.

Если результат вычисления используется в какой-то момент в процессе выполнения программа, “задумка” вычисляется и результат вычисления сохраняется (так, что вычисление происходит только один раз). Если результат не используется, то “задумка” не вычисляется и впоследствии удаляется сборщиком мусора.

Общий принцип такой: выражения не вычисляются, пока они не нужны, и не вычисляются повторно, если этого можно избежать. Мы обсудим как это работает, какие есть исключения, и как добавить строгость при необходимости.

Расходящиеся вычисления

В рамках анализа типов в строго типизированных тьюринг-полных языках обычно вводят тип Bottom, который является подтипом всех типов. Этот тип назначается результатам расходящихся вычислений – вычислений, которые никогда не завершаются или завершаются ошибкой. У типа Bottom нет никаких значений, и он вводится исключительно как теоретическая конструкция – действительно, при проверке типов невозможно назначить тип Bottom ничему, поскольку для этого нужно было бы решить проблему останова (которая как известно алгоритмически неразрешима).

В Haskell, тип Bottom не вводится явно как тип, но каждый тип расширяется значением, обозначаемым ⊥, символизирующим ошибку времени выполнения или незавершение вычислений. С точки зрения стратегии вычисления, вычисление явного ⊥ немедленно генерирует ошибку времени выполнения и завершает работу программы. В Haskell есть две встроенных функции, возвращающих ⊥: undefined :: a и error :: String -> a.

Если бы Haskell был строгим, любое использование undefined или error гарантированно приводило бы к ошибке времени выполнения. Однако при нестрогих вычислениях, если значение ⊥ не используется, то оно не вычисляется, и, следовательно, не генерирует ошибку времени выполнения. Мы используем этот факт в дальнейшем при обсуждении строгости.

Отличие нестрогости и ленивости

Технически, стандарт Haskell определяет вычисления как нестрогие, но не ленивые. Основное отличие в том, что истинно ленивый язык запоминает результаты всех вычислений с целью переиспользования. Такой подход на практике потребляет неприемлемо большой объём памяти, поэтому за исключением исследовательских проектов практически не применяется. Нестрогость не требует сохранения результатов вычислений, а только того, что неиспользуемые результаты не вычисляются.

В качестве примера, следующий код работает только в силу нестрогости:

fst (1, undefined)
snd (undefined, 2)

Стандарт таким образом требует только чтобы конечное поведение соответствовало нестрогой семантике, и не накладывает конкретных ограничений на детали реализации и повторные вычисления.

Порядок вычисления

При обсуждении стратегий редукции λ-исчисления, мы уже обсуждали строгие и нестрогие вычисления. “На пальцах” можно считать, что строгие вычисления производятся “изнутри наружу”, т.е. сначала вычисляются внутренние термы, затем внешние. Нестрогие вычисления производятся “снаружи внутрь”, т.е. сначала вычисляется внешний терм. Как следствие, порядок вычисления и что именно вычисляется, может определяться вводом.

Рассмотрим следующий код:

maybeBottom f = f fst snd (0, undefined)

-- булевские значения Чёрча
tru a b = a
fls a b = b

Вычисление maybeBottom будет зависеть от переданного аргумента. Так, maybeBottom tru, если подставить определения, вычисляется следующим образом:

tru fst snd (0, undefined)
(\a -> \b -> a) fst snd (0, undefined)
(\b -> fst) snd (0, undefined)
fst (0, undefined)
0

maybeBottom fls же получит undefined.

Та же идея с аналогичным поведением в более читаемом Haskell:

maybeBottom b =
  case b of
    True  -> fst tup
    False -> snd tup
  where tup = (0, undefined)

Когда мы говорим, что вычисление работает “снаружи внутрь”, мы говорим о вычислении вложенных выражений. Причём мы не только начинаем с самого внешнего выражения, мы ещё и не вычисляем подвыражения, которые не используются непосредственно в результате.

Нестрогость делает Haskell более выразительным, в том смысле, что мы можем ссылаться на значения, которые ещё не вычислены. В строгих языках, нельзя просто связать вычисление с именем, не произведя это вычисление.

Этот паттерн применим и к структурам данных. Так, например, мы можем вычислить длину списка, не трогая его значений:

length [undefined, undefined, undefined] == 3

Принудительная строгость

В Haskell есть “магическая” функция seq :: a -> b -> b, которая сначала вычисляет первый аргумент, затем возвращает второй. Эта операция называется форсирование первого аргумента. Обычно форсирование происходит, когда требуется значение, но мы можем принудительно форсировать любое вычисление, передав его seq. Следует понимать, что само выражение seq x y всё равно вычисляется нестрого, т.е. если это значение нигде не используется, то ни x ни y вычислены не будут. Удобно думать о seq как о связывании порядка вычислений: seq x y означает, что при вычислении seq x y, прежде, чем вычислять y надо вычислить x, даже если он не используется в y.

Семантика seq в терминах ⊥ определяется следующим образом:

seq ⊥ b = ⊥
seq x b = b

Weak Head Normal Form

Когда мы говорим, что seq форсирует вычисление первого аргумента, на самом деле мы имеем ввиду что вычисление производится к слабой головной нормальной форме (WHNF), а не к полной нормальной форме. Вычисление WHNF означает, что вычисление останавливается на первом встреченном конструкторе данных или лямбда-выражении:

dc = (,) undefined undefined
lam = \_ -> undefined
noDc = undefined

dc `seq` 1 == 1
lam `seq` 1 == 1
noDc `seq` 1 == ⊥

В dc, вычисление останавливается на конструкторе (,), в lam – на лямбда-выражении. noDc содержит “голый” undefined, поэтому приводит к ошибке времени выполнения.

Форсирование без seq

Форсирование в WHNF происходит автоматически не только с помощью seq. Кроме, собственно, прямого вычисления, форсирование вызывает сопоставление с шаблоном (в функциях, выражениях case и пр.)

Рассмотрим пример:

data Test = A Test2 | B Test2 deriving Show
data Test2 = C Int | D Int deriving Show

notForcing :: Test -> Int
notForcing _ = 0

forceTest :: Test -> Int
forceTest (A _) = 1
forceTest (B _) = 2

forceTest2 :: Test -> Int
forceTest2 (A (C i)) = i
forceTest2 (B (C i)) = i
forceTest2 (A (D i)) = i
forceTest2 (B (D i)) = i

notForcing не производит непосредственно сопоставления с шаблоном, только связывает вычисление с именем _ (которое игнорируется).

forceTest форсирует значение типа Test, поскольку сопосотавление происходит с конструкторами Test, но вложенный Test2 не форсируется.

forceTest2 форсирует значения Test и Test2, но вообще говоря не Int, которое возвращается из функции.

GHC Core

GHC использует двухуровневую модель компиляции, первый этап транслирует Haskell в язык GHC Core, в целом более простой (в смысле количества конструкций), а GHC Core уже компилируется в машинный код.

В GHC Core может быть более очевидно, какие выражения и в каком порядке вычисляются. Чтобы получить вывод GHC Core, можно передать компилятору ключ -ddump-simpl. В GHCi можно передать команду :set -ddump-simpl.

Рассмотрим пример:

discriminatory :: Bool -> Int
discriminatory b =
  case b of
    False -> 0
    True -> 1

Вывод будет иметь вид:

==================== Tidy Core ====================
-- snip
discriminatory :: Bool -> Int
[GblId, Arity=1, Caf=NoCafRefs, Unf=OtherCon []]
discriminatory
  = \ (b_a1wX :: Bool) ->
      break<2>(b_a1wX)
      case b_a1wX of {
        False -> break<0>() GHC.Types.I# 0#;
        True -> break<1>() GHC.Types.I# 1#
      }
-- snip

Этот вывод достаточно “шумный”, в том смысле, что выводит много дополнительной информации. “Лишний” шум можно убрать, передав флаг -dsuppress-all. Тогда вывод

discriminatory
  = \ b_a1yq ->
      case b_a1yq of {
        False -> I# 0#;
        True -> I# 1#
      }

В языке GHC Core выражения case всегда форсируют вычисления. Из этого вывода мы можем сказать, что значение вычисления, обозначенного b_a1yq должно быть вычислено до вычисления результата. I# 0# это представление числовых литералов в GHC Core.

Если аналогично рассмотреть предыдущий пример, то получится следующее:

notForcing = \ _ -> I# 0#

forceTest
  = \ ds_d2Rz ->
      case ds_d2Rz of {
        A ds1_d2RH -> I# 1#;
        B ds1_d2RI -> I# 2#
      }

forceTest2
  = \ ds_d2Rj ->
      case ds_d2Rj of {
        A ds1_d2Rx ->
          case ds1_d2Rx of {
            C i_a1Nh -> i_a1Nh;
            D i_a1Nj -> i_a1Nj
          };
        B ds1_d2Ry ->
          case ds1_d2Ry of {
            C i_a1Ni -> i_a1Ni;
            D i_a1Nk -> i_a1Nk
          }
      }

Мы видим, что notForcing ничего не форсирует, forceTest форсирует вычисление Test, а forceTest2 – вычисление Test2.

Если мы выведем Core для кода

discriminatory :: Bool -> Int
discriminatory b =
  let x = undefined
  in case b of
    False -> 0
    True -> 1

мы обнаружим, что имени x в выводе вообще нет:

discriminatory
  = \ b_a2TH ->
      case b_a2TH of {
        False -> I# 0#;
        True -> I# 1#
      }

GHC видит, что x не используется, и убирает его сразу же. Если же мы его форсируем при помощи seq

discriminatory :: Bool -> Int
discriminatory b =
  let x = undefined
  in case x `seq` b of
    False -> 0
    True -> 1

то увидим следующий код:

discriminatory
  = \ b_a2XO ->
      let {
        x_a2XP
        x_a2XP
          = \ @ a_a2Y2 ->
              -- snip
              undefined ($dIP_s2Yu `cast` <Co:4>) } in
      case case x_a2XP of { __DEFAULT -> b_a2XO } of {
        False -> I# 0#;
        True -> I# 1#
      }

Под -- snip скрывается определение для сообщения об ошибке, но ключевое здесь что мы имеем здесь два вложенных выражения case: первое – для x, второе – для b.

Следует отметить, что в Haskell выражения case форсируют значения только при сопоставлении с шаблоном, выражение

case x of { _ -> b }

не форсирует значение x поскольку сопоставления с шаблоном нет. В Core, выражения case всегда форсируют вычисление.

“Задумки”

Как было сказано выше, “задумка” означает вычисление, которые могут быть выполнены позже. Некоторые значения вычисляются сразу – не для всех создаются “задумки”. Чтобы посмотреть, какие значения уже вычислены, в GHCi есть функция :sprint. Рассмотрим пример:

Prelude> let list = [1,2,3] :: [Int]
Prelude> :sprint list
list = [1,2,3]

Но в то же время

Prelude> let list = tail [1,2,3] :: [Int]
Prelude> :sprint list
list = _

В первом случае, list оказался сразу вычислен. Во втором – нет. Причина достаточно простая: GHC по возможности вычисляет полностью применённые конструкторы данных к WHNF сразу. Конструкторами данных являются конструкторы списка : и [], значения Int и т.д. Эта оптимизация допустима, поскольку полностью применённые конструкторы данных по сути всегда являются константами. Это не относится к частично применённым конструкторам:

Prelude> let list = (: [])
Prelude> :sprint list
list = _

Также вычисление прекращается как только обнаружено выражение, не являющееся конструктором данных:

Prelude> let list = [1,2,id 3] :: [Int]
Prelude> :sprint list
list = [1,2,_]

Несмотря на то, что id 3 – примитивное вычисление, GHC оставляет его как есть.

И это не относится к полиморфным значениям:

Prelude> let list = [1,2,3]
Prelude> :t list
list :: Num a => [a]
Prelude> :sprint list
list = _

Ещё один пример:

Prelude> let list = [1,2,3] :: [Int]
Prelude> :sprint list
list = [1,2,3]
Prelude> let list' = list ++ undefined
Prelude> :sprint list'
list' = _

Здесь list' – не вычисляется, поскольку ++ – это функция.

Разделение

Именованные вычисления могут повторно использоваться в любом месте, где они встречаются. Это означает, что результаты вычисления разделяются между местами использования. Разделение вычислений позволяет более эффективно использовать память. Следует отметить, что GHC может произвольно включать и выключать разделение в чистом коде – в основном это делается с целью ускорения выполнения. В монаде IO разделение вычислений всегда отключается.

Для наблюдения за порядком вычислений можно использовать функцию trace :: String -> a -> a из модуля Debug.Trace. При вычислении, эта функция выводит строку на вывод стандартной ошибки.

Рассмотрим два примера:

import Debug.Trace

test  = let x = trace "x" (1 :: Int)
            y = trace "y" (1 :: Int)
        in x + y

test2 = let x = trace "x" (1 :: Int)
        in x + x

*Main> test
x
y
2
*Main> test2
x
2

Как мы видим, в первом случае, и x и y вычисляются. Во втором случае, x вычисляется только один раз, хотя используется дважды. Отдельно следует отметить, что компилятор не обязательно применяет разделение для функций с одинаковыми аргументами. Например следующая программа:

import Debug.Trace
main = print $ trace "x" 1 + trace "x" 1

выведет

x
x
2

то есть функция trace "x" 1 вычисляется дважды.

В то же время,

import Debug.Trace
main = print $ let v = trace "x" 1 in v + v

выведет x только один раз.

Из этого можно вывести следующее правило: если вычисление используется несколько раз, лучше связать его с именем. Это также может повысить читаемость кода.

Функции могут разделяться, но только если они не имеют именованных аргументов. Так, при вычислении следующих двух функций порядок вычисления различный:

import Debug.Trace
test1 = let f = const (trace "f" 1) in f 0 + f 0
test2 = let f _ = trace "f" 1 in f 0 + f 0

*Main> test1
f
2
*Main> test2
f
f
2

Бесточечная нотация таким образом позволяет более эффективно разделять память.

Разделению так же препятствует полиморфизм: полиморфные значения не заделяются. Причина в том, что ограничения классов типов в Core выражаются дополнительными аргументами, а функции не разделяются.

Опровержимые и неопровержимые шаблоны

При разговоре о сопоставлении с шаблоном и строгости, необходимо делать разницу между опровержимыми и неопровержимыми шаблонами.

Неопровержимые шаблоны – это шаблоны, сопоставление с которыми всегда успешно. К неопровержимым шаблонам относятся имена без конструкторов, например

case x of
  y -> ...

y является неопровержимым шаблоном.

Ключевое, что необходимо помнить: неопровержимые шаблоны не форсируют вычисление

Haskell позволяет пометить шаблоны неопровержимыми, чтобы отложить сопоставление с шаблоном до места использования (или вообще не производить в случае отсутствия использования). Для этого перед шаблоном ставится символ ~. Это может быть удобно для типов данных с одним конструктором:

strict (a, b) = "OK"
lazy ~(a, b) = "OK"

*Main> strict undefined
"*** Exception: Prelude.undefined
CallStack (from HasCallStack):
  error, called at libraries/base/GHC/Err.hs:78:14 in base:GHC.Err
  undefined, called at <interactive>:5:8 in interactive:Ghci1
*Main> lazy undefined
"OK"

Следует однако отметить, что форсирование аргументов может быть хорошей идеей для более предсказуемого поведения.

Дополнительно следует иметь ввиду, что шаблоны в левой части let-выражения по умолчанию являются неопровержимыми:

notForcing _ = ()

ex1 = let (x,y) = undefined in notForcing x -- вычисление даст ()

ex2 = let ~(x,y) = undefined in notForcing x -- эквивалентно ex1

Наконец заметим, что связывание <- в do-нотации по умолчанию строгое. Если совсем точно, то конструкции вида pat <- computation, преобразуются к виду

do pat <- computation     >>>     let f pat = more
   more                   >>>         f _ = fail "…"
                          >>>     in  computation >>= f

соответственно шаблон в левой части <- ведёт себя точно так же, как аргумент функции.

Использование fail с GHC 8.0 требует класса MonadFail:

class Monad m => MonadFail m where
    fail :: String -> m a

Если при использовании шаблона в левой части <- компилятор сообщает об отсутствующем экземпляре MonadFail – теперь Вы знаете почему.

Форсирование шаблонов

GHC поддерживает расширениие BangPatterns, включаемое директивой

{-# LANGUAGE BangPatterns #-}

Это расширение позволяет пометить неопровержимые шаблоны как строгие, например:

{-# LANGUAGE BangPatterns #-}
lazy x = "OK"
strict !x = "OK"

*Main> lazy undefined
"OK"
*Main> strict undefined
"*** Exception: Prelude.undefined
CallStack (from HasCallStack):
  error, called at libraries/base/GHC/Err.hs:78:14 in base:GHC.Err
  undefined, called at <interactive>:9:8 in interactive:Ghci2

По сути это эквивалентно использованию seq:

strict x = x `seq` "OK"

Более того, если сравнить вывод Core, то он одинаковый:

trict
strict
  = \ @ p_asn x_as3 ->
      case x_as3 of { __DEFAULT -> unpackCString#
      "OK"# }

-- RHS size: {terms: 7, types: 4, coercions: 0, joins: 0/0}
strictSeq
strictSeq
  = \ @ t_asa x_as4 ->
      case x_as4 of { __DEFAULT -> unpackCString#
      "OK"# }

Но нотация строгих шаблонов короче и часто легче читается.

Строгие шаблоны можно использовать в левой части let-выражений. Возвращаясь к предыдущему примеру,

notForcing _ = ()

ex1 = let (x,y) = undefined in notForcing x -- вычисление даст ()

ex2 = let ~(x,y) = undefined in notForcing x -- эквивалентно ex1

ex3 = let !(x,y) = undefined in notForcing x -- ошибка!

ex4 = let !x = undefined in notForcing x -- тоже ошибка, x форсируется

ex5 = let !(x,y) = (undefined, undefined) in notForcing x
-- нет ошибки, (x,y) форсируется к WHNF, т.е. x,y не форсируются.

Строгость в конструкторах данных

Конструкторы данных вообще говоря являются нестрогими, т.е. для

data Test = Test Int
test (Test _) = "OK"

вызов test (Test undefined) ожидаемо вернёт "OK". Можно, однако, пометить аргументы конструктора как строгие, используя то же соглашение с восклицательным знаком:

data Test = Test !Int

тогда вычисление значений к WHNF так же будет вычислять и строгие аргументы:

data Test = Test !Int
test (Test _) = "OK"

вызов test (Test undefined) завершится ошибкой.

Идея в том, что иногда дешевле сразу вычислить значение, чем хранить “задумку” этого вычисления – если мы уверены, что результат рано или поздно всё равно понадобится, или вычисление само по себе очень быстрое. Такие аннотации строгости часто встречаются в вычислительном коде, где множества Int и Double дешевле вычислить сразу, чем конструировать и хранить “задумки” их вычислений.

Расширения Strict и StrictData

В GHC 8.0 добавлены расширения языка Strict и StrictData. Первое делает неопровержимые шаблоны, не помеченные явно ~ строгими. Второе делает все аргументы конструкторов данных строгими. По сути, это просто способ сэкономить нажатия клавиш на расстановку ! и/или seq. Эти расширения, как и все остальные, действуют только в рамках модуля, для которого они включены.