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

Тип Bottom – подтип всех типов, тип результата расходящихся вычислений.

Bottom не населён. Чисто теоретическая конструкция. Проверка типов не может назначить Bottom (проблема останова).

В Haskell нет явного Bottom (не добавляет выразительной силы). Но каждый тип расширяется значением “bottom”, обозначаемым ⊥. Вычисление ⊥ – немедленно ошибка и завершение.

undefined :: a
error :: String -> a

В строгом языке, ⊥ – немедленное завершение. В нестрогом, если ⊥ не используется, то не вычисляется, тогда нет ошибки.

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

Технически Haskell – нестрогий, не ленивый.

Ленивый – запоминает результаты всех вычислений. Высокое потребление памяти, на практике почти не применяется. Нестрогость не гарантирует отсутствие повторных вычислений, только отсутствие “ненужных”.

Работает только в силу нестрогости:

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

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

Обсуждалось в лекции 1.

Упрощённо: строгие – “изнутри наружу”; нестрогие “снаружи внутрь”. Следствие – в нестрогих что вычисляется определяется вводом.

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

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)

За счёт нестрогости – более выразительный; можем ссылаться на значения, которые не вычислены. В строгих языках – невозможно назвать значение без вычисления.

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

length [undefined, undefined, undefined] == 3

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

seq :: a -> b -> b

“Магическая” функция. Cначала вычисляет первый аргумент, затем возвращает второй. Называется форсирование. Обычно форсирование – когда требуется значение. Можем принудительно форсировать через seq.

seq x y всё равно нестрого. Удобно думать как о связывании порядка вычислений: seq x y – прежде y, вычислить x, y не зависит от x.

Семантика seq касательно ⊥:

seq ⊥ b = ⊥
seq x b = b

Weak Head Normal Form

Вычисление – до слабой головной нормальной формы (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, не 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#
      }

В Core, case всегда форсируют вычисления. b_a1yq вычисляется до вычисления результата. I# 0# – литерал целого в Core.

Предыдущий пример:

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

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 = \ _ -> 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
          }
      }

Для кода

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

в Core x нет:

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

Компилятор молча убирает неиспользуемые имена.

Если форсируем x при помощи seq:

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

то вывод Core:

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

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

Ключевое: два вложенных case: первое – для x, второе – для b.

Отличие Core от Haskell: в 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 – примитивное, но не вычисляется.

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

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 дважды, следовательно 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

test1 выведет f один раз. test2 выведет f два раза.

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

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

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

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

Имена без конструкторов, например

case x of
  y -> ...

y – неопровержимый.

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

Возможно явно пометить шаблон неопровержимым: перед шаблоном ставится символ ~. Удобно для типов данных с одним конструктором:

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"

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

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

Расширение BangPatterns

{-# LANGUAGE BangPatterns #-}

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

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

*Main> lazy undefined
"OK"
*Main> strict undefined
"*** Exception: Prelude.undefined

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

strict !x = "OK"
strictSeq x = x `seq` "OK"

Вывод Core одинаковый:

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

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

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

Конструкторы данных – нестрогие.

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

test (Test undefined) вернёт "OK".

Идея: иногда дешевле сразу вычислить значение, чем хранить клаузу этого вычисления. Если уверенность, что результат используется или вычисление очень быстрое.

Строгие аргументы конструктора. Тогда вычисление аргументов при вычислении значения:

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

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

Аннотации строгости часто встречаются в вычислительном коде.

Strict и StrictData

В GHC 8.0 добавлены расширения языка Strict и StrictData.

Strict – шаблоны, не помеченные явно ~, становятся строгими.

StrictData – все аргументы конструкторов данных становятся строгими.

По сути, просто способ сэкономить нажатия клавиш на расстановку ! и/или seq.

Встроенный механизм исключений:

• Исключения в IO
• Неточные исключения – генерируемые чистым кодом
• Асинхронные исключения – бросаемые между потоками управления

Основной модуль – Control.Exception.

Исключения могут быть брошены откуда угодно, но обработаны – только в IO.

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

Пакет exceptions стремится объединить различные способы бросания/обработки исключений в единый интерфейс.

Класс Exception

Исключения – обычные типы и значения. Типы исключений – в классе Exception:

class (Typeable e, Show e) => Exception e where
  toException :: e -> SomeException
  fromException :: SomeException -> Maybe e
  displayException :: e -> String

Определяет описание ошибки (displayException) и преобразования в/из экзистенциальный тип SomeException.

Классу Exception принадлежат много типов: IOException, Deadlock, BlockedIndefinitelyOnSTM, AsyncException, AssertionFailed и т.д.

Рассмотрим ArithException – исключения в арифметике:

data ArithException
  = Overflow
  | Underflow
  | LossOfPrecision
  | DivideByZero
  | Denormal
  | RatioZeroDenominator
  deriving (Eq, Ord, Show)

Экзистенциальная квантификация

data SomeException = forall e. Exception e => SomeException e

Требует расширения ExistentialQuantification. Позволяет экзистенциально-полиморфный конструктор типа.

Не то же самое, что полиморфный тип!

data Polymorphic a = Polymorphic a

не позволяет использовать Polymorphic 1 и Polymorphic "1" в одном контексте — значения разных типов, Polymorphic Int и Polymorphic String. Значение типа a в каждом случае инстанцированно конкретным типом.

data SomeException = forall e. Exception e => SomeException e

Если тип экзистенциальный, конструктор может быть использован с любым значением (удовлетворяющим ограничениям), и это будут значения одного и того же типа

Ключевой момент: значение типа может содержать что угодно, поэтому к значению применимы только операции, применимые к любому возможному значению. Т.е., нельзя применить к значению в SomeException никаких функций, кроме определённых для класса Exception.

Пример:

{-# LANGUAGE ExistentialQuantification #-}
data AnyNumber = forall a. (Show a, Num a) => AnyNumber a

instance Show AnyNumber where
  showsPrec d (AnyNumber x)
    = showParen (d > app_prec)
    $ showString "AnyNumber "
    . showsPrec (app_prec+1) x
    where app_prec = 10

negateAnyNumber :: AnyNumber -> AnyNumber
negateAnyNumber (AnyNumber x) = AnyNumber (negate x)

int = AnyNumber (1 :: Integer)
float = AnyNumber (1.0 :: Double)
ratio = AnyNumber (1.0 :: Rational)

negateAnyNumber int == AnyNumber (-1)
negateAnyNumber float == AnyNumber (-1.0)
negateAnyNumber ratio == AnyNumber ((-1) % 1)

Typeable

Класс Typeable определён в модуле Data.Typeable. Позволяет производить проверку типов динамически. Позволяет узнать тип значения во время выполнения и сравнить типы разных значений. Автоматически выводится для всех типов в GHC.

Если добавить в экзистенциальный конструктор ограничение Typeable, сможем определить для AnyNumber бинарные операции:

import Data.Typeable

data AnyNumber
  = forall a. (Typeable a, Show a, Num a)
      => AnyNumber a
-- ...
sumAnyNumbers ::
  AnyNumber -> AnyNumber -> Maybe AnyNumber
sumAnyNumbers (AnyNumber x) (AnyNumber y) =
  AnyNumber . (y +) <$> cast x

cast, определённый для Typeable, возвращает Just x, если типы x и y эквивалентны:

sumAnyNumbers float float == Just (AnyNumber 2.0)
sumAnyNumbers int ratio == Nothing

Аналогично cast работает функция fromException.

Когда кидается исключение:

1. Ищется catch выше по стеку вызовов
2. Проверяется тип исключения, которое ловит этот catch
3. Если catch ловит SomeException вызывается обработчик.
4. Если catch ловит более конкретный тип, преобразование через fromException
5. Если результат Just, вызвать обработчик.
6. Если результат Nothing продолжить поиск.

Обработка исключений

Функция

catch :: Exception e => IO a -> (e -> IO a) -> IO a

{-# LANGUAGE ScopedTypeVariables #-}
import Control.Exception

main :: IO ()
main = do
  let someValue = 2 `div` 0
  print someValue
    `catch` \(e :: ArithException)
      -> putStrLn
         $ "Got arithmetic error: "
         <> displayException e

Повторимся, обработка исключений возможна только в IO.

catch в такой записи относится только к последней строчке. Если исключение произойдёт раньше, оно не будет поймано:

main :: IO ()
main =   let someValue = 2 `div` 0
  in someValue `seq` (print someValue
    `catch` \(e :: ArithException)
      -> putStrLn
       $ "Got arithmetic error: "
       <> displayException e)

Исключение бросается до print someValue.

Особенность: если catch (или любой другой инфиксный оператор) на верхнем уровне do-блока, то он относится ко всему do-блоку:

main = do
  let someValue = 2 `div` 0
  someValue `seq` print someValue
  `catch` \(e :: ArithException)
    -> putStrLn
       $ "Got arithmetic error: "
       <> displayException e

означает

main = (do
  let someValue = 2 `div` 0
  someValue `seq` print someValue
  ) `catch` \(e :: ArithException)
    -> putStrLn
       $ "Got arithmetic error: "
       <> displayException e

Вызовы catch можно комбинировать:

main :: IO ()
main = do
  let someValue = 2 `div` 0
  error "Some error"
  print someValue
  `catch` (\(e :: ArithException)
    -> putStrLn
       $ "Got arithmetic error: "
       <> displayException e)
  `catch` (\(e :: SomeException)
    -> putStrLn
       $ "Got other error: "
       <> displayException e)

Обычно вместо лямбда-функций пишутся отдельные функции-обработчики, а вместо вложенных catch используется функция catches:

main :: IO ()
main = do
  let someValue = 2 `div` 0
  print someValue
  `catches` [ Handler arithmetic
            , Handler otherError ]
  where
  arithmetic :: ArithException -> IO ()
  arithmetic e = putStrLn
       $ "Got arithmetic error: "
       <> displayException e
  otherError :: SomeException -> IO ()
  otherError e = putStrLn
      $ "Got other error: "
      <> displayException e

Handler – экзистенциальный тип, оборачивающий обработчик исключений.

try

Исключения можно преобразовать в явные значения типа Either:

try :: Exception e => IO a -> IO (Either e a)

Пример:

import Control.Exception
import System.Environment

testDiv :: String -> IO ()
testDiv d = do
  result <- try $ print $ 5 `div` read d
  case result of
    Left e -> print (e :: SomeException)
    Right _ -> return ()

main :: IO ()
main = getArgs >>= mapM_ testDiv

Выполнение даст вывод:

:main 1 a 2 0 4
5
Prelude.read: no parse
2
divide by zero
1

Выбрасывание исключений

Выбрасывание исключений в IO – функцией

throwIO :: Exception e => e -> IO a

Есть функция throw, которая бросает исключения без IO:

throw :: Exception e => e -> a
throwIO :: Exception e => e -> IO a

Использование throw нежелательно. В чистом коде стараются по возможности избегать исключений – хотя бы потому, что поймать их всё равно можно только в IO.

Объявление собственного типа исключений

{-# LANGUAGE ScopedTypeVariables #-}
import Control.Exception
import Data.Char (isAscii)
import Control.Monad (unless)

data NotValidString = NotValidString
  deriving (Eq, Show)

instance Exception NotValidString

isStringOk :: String -> IO ()
isStringOk str =
  unless (all isAscii str) $
    throwIO NotValidString

main :: IO ()
main = lines <$> getContents
  >>= mapM_ (\v ->
    isStringOk v
    `catch` (\(e :: NotValidString) -> print e))

Взаимодействие с ⊥

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

Например,

main = print =<< try @SomeException (undefined :: IO Int)

и

main = print =<< try @SomeException (return undefined :: IO Int)

имеют различное поведение. “Оборачивание” ⊥ в return позволяет ему выйти за пределы try, поскольку try не форсирует результат вычисления.

C осторожностью – ко всем исключениям из чистого кода: исключение бросается там, где форсируется значение, что не обязательно там, где ловится исключение. Ещё одна причина не использовать throw и error, если предполагается продолжать работу программы.

Асинхронные исключения

Асинхронные исключения – достаточно редкое явление в языках программирования.

Асинхронное исключение может быть брошено между потоками: один поток бросает исключение в другой. Это в основном актуально для многопоточного кода, но асинхронные исключения могут быть брошены в любой момент ввиду переполнения стека, кучи, если ОС по какой-то причине пытается “убить” поток и т.п. При работе с критичными данными, следует это учитывать.

Основные функции:

bracket :: IO a -> (a -> IO b) -> (a -> IO c) -> IO c
mask :: ((forall a. IO a -> IO a) -> IO b) -> IO b
throwTo :: Exception e => ThreadId -> e -> IO ()

• mask – временное “отключение” асинхронных исключений
• bracket – работа с ресурсом
• throwTo – кидает асинхронное исключение в заданный поток

bracket :: IO a -> (a -> IO b) -> (a -> IO c) -> IO c

Пример bracket:

import Control.Exception
import System.IO
appendToFile :: FilePath -> String -> IO ()
appendToFile fp text = bracket
  (openFile fp AppendMode)
  hClose $ \h -> hPutStrLn h text

(вообще то же самое делает функция withFile):

withFile :: FilePath -> IOMode -> (Handle -> IO r) -> IO r
withFile name mode = bracket (openFile name mode) hClose

throwTo :: Exception e => ThreadId -> e -> IO ()

Пример throwTo:

import Control.Concurrent (forkIO, threadDelay)
import Control.Exception

main = do
  thread <- forkIO $ interact id
  threadDelay $ 5*1000000
  throwTo thread ThreadKilled

Обработчики в catch “замаскированы”, но try – не маскируется. Поэтому, обрабатывать асинхронные исключения с помощью catch.

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