Функциональное проектирование

На основе главы 5 Richard Bird. Thinking functionally with Haskell. Cambridge University Press, 2014.

Использование чистого функционального языка позволяет использовать определённый подход к проектированию программ. Этот подход известен как “equational reasoning”, в вольном переводе “рассуждение на основе уравнений”. Функциональная чистота, собственно, обеспечивает отсутствие побочных эффектов, и, как следствие, возможность рассуждать о программах в более строгих математических терминах.

Рассмотрим этот подход на примере: напишем решатель судоку.

Судоку – логическая игра на сетке 9х9. Сетка поделена на 9 квадратов 3х3. В клетках сетки ставятся цифры от 1 до 9. Ни в какой строчке, столбце или квадрате 3х3 не должно быть повторяющихся цифр. В начале игры некоторые ячейки уже содержат цифры, задача – заполнить сетку целиком.

Начнём со спецификации в терминах Haskell, затем оптимизируем решение, используя рассуждения на основе уравнений.

Спецификация

Для представления сетки, используем список списков. Возможно не самое эффективное представление, однако оно достаточно простое и подходит для наших целей.

type Matrix a = [Row a]
type Row a = [a]

Матрицу мы рассматриваем как список строк, строку – как список значений. Для судоку, возможные значения в ячейках – это цифры от 1 до 9, либо пустые. Мы введём тип данных перечисления вида

data Digit =
  D1 | D2 | D3 | D4 | D5 | D6 | D7 | D8 | D9
  deriving (Show, Read, Enum, Bounded, Eq, Ord)

тогда начальная сетка судоку (с пропусками) будет иметь вид

type InitialGrid = Matrix (Maybe Digit)

а заполненная сетка

type Grid = Matrix Digit

Сейчас наша задача – определить спецификацию не слишком задумываясь об эффективности. Функциональная чистота позволяет сравнительно легко полученную (неэффективную) спецификацию преобразовать к более эффективному виду не меняя наблюдаемого поведения.

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

solve :: InitialGrid -> [Grid]
solve = filter valid . completions

Чтобы не путаться лишний раз в уровнях списков, введём тип

newtype Choice a = Choice [a]
  deriving (Show, Semigroup, Monoid, Functor, Applicative, Monad, Eq, Foldable)

(используя расширение GeneralizedNewtypeDeriving)

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

solve :: InitialGrid -> Choice Grid
solve = filter' valid . completions

filter' :: (a -> Bool) -> Choice a -> Choice a
filter' p (Choice xs) = Choice (filter p xs)

и тогда

valid :: Grid -> Bool
completions :: InitialGrid -> Choice Grid

Один из вариантов как можно определить completions – это через композицию двух функций,

completions = expand . choices

где

choices :: InitialGrid -> Matrix (Choice Digit)
expand :: Matrix (Choice Digit) -> Choice Grid

Функция choices подставляет в пустые ячейки списки возможных значений. Если в ячейке уже есть значение, то choices помещает в соответствующую ячейку список из 1 элемента.

choices = map (map choice)
choice :: Maybe Digit -> Choice Digit
choice Nothing = Choice [D1 .. D9]
choice (Just d) = pure d

Функция expand преобразует матрицу списков возможных значений в список возможных сеток. Как она должна работать? По-видимому, она должна строить декартово произведение множеств сеток для всех ячеек. Определим для начала декартово произведение для элементов-списков списка.

cartesianProduct :: [ Choice a ] -> Choice [a]
cartesianProduct (choiceX:xs) = do
  x <- choiceX
  ys <- cartesianProduct xs
  return $ x:ys
cartesianProduct [] = return []

Монада списка моделирует нондетерминизм. Один из результатов у нас получится, если взять одно значение x из первого элемента списка choiceX и одно возможное “продолжение” ys из декартова произведения “хвоста” xs, и соединить их в x:ys. В случае декартова произведения списка вернём пустой список (обёрнутый в Choice) – декартово произведение 0 элементов с 0 элементов даёт множество состоящее из пустого множества.

Вообще говоря, эта реализация будет вычислять cartesianProduct xs многократно, что нежелательно. Избежать этого достаточно легко, связав это вычсиление с именем:

cartesianProduct :: [ Choice a ] -> Choice [a]
cartesianProduct (choiceX:xs) = do
  x <- choiceX
  ys <- yss
  return $ x:ys
  where yss = cartesianProduct xs
cartesianProduct [] = return []

Строго говоря наша реализация cartesianProduct это просто sequenceA.

Вернёмся теперь к функции expand. Мы представляем матрицу как список строк, строки как списки значений. Тогда мы можем сформулировать функцию expand в терминах

expand = cartesianProduct . map expandRow
expandRow :: Row (Choice a) -> Choice (Row a)

В свою очередь,

expandRow = cartesianProduct

Другой путь получить то же выражение – это посмотреть внимательно на типы:

expand :: Matrix (Choice Digit) -> Choice Grid

подставив синонимы:

expand :: [[Choice Digit]] -> Choice [[Digit]]

несложно заметить, что Choice перемещается “изнутри” списков “наружу”. Одно такое перемещение – это применение функции

sequenceA :: Applicative f => t (f a) -> f (t a)

Тогда если x :: [[Choice Digit]], то

fmap sequenceA x :: [Choice [Digit]]

Здесь мы используем fmap чтобы “обменять” внутренние конструкторы. Тогда соответственно

sequenceA (fmap sequenceA x) :: Choice [[Digit]]

И тогда

expand = sequenceA . fmap sequenceA

или синонимично

expand = cartesianProduct . map cartesianProduct

Обратимся теперь к функции valid. Корректная сетка – это сетка, в которой нет дубликатов в строках, столбцах и квадратах. Мы можем определить

valid grid = all nodups (rows grid)
          && all nodups (cols grid)
          && all nodups (boxes grid)

Здесь

rows :: Matrix a -> [Row a]
cols :: Matrix a -> [Col a]
boxes :: Matrix a -> [Box a]

type Col a = [a]
type Box a = [a]

nodups :: [Digit] -> Bool

(синонимы типов вводятся для целей документации и повышения читаемости)

Реализация nodups возможна в терминах свёртки, а именно:

nodups = fst . foldr (\d (b, ds) -> (b && d `notElem` ds, d:ds)) (True, [])

иначе эквивалентно можно сформулировать в виде

nodups [] = True
nodups (x:xs) = all (/=x) xs && nodups xs

оба варианта имеют квадратичную сложность. Альтернативный вариант – отсортировать список и проверить что элементы строго возрастают, что будет иметь сложность \(O(n\log n)\), но для списка из 9 элементов это несущественно (и возможно сортировка медленнее за счёт больших накладных расходов)

Функция rows по сути ничего не делает, т.к. матрица и так представлена в виде списка строк:

rows = id

Функция cols должна по сути транспонировать матрицу:

cols = Data.List.transpose

однако попробуем реализовать transpose:

transpose :: [[a]] -> [[a]]
transpose [] = []
transpose ([] : xss) = transpose xss
transpose xss
  = [ h | (h:_) <- xss ]
    : transpose [ t | (_:t) <- xss ]

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

Наконец, функция boxs. По сути нам нужно сгруппировать элементы по 3, затем сгруппировать строки по 3, затем взять каждую из таких групп. Рассмотрим на уменьшенном примере, когда сетка имеет размер 4х4 и берутся группы по 2:

[ [11, 12, 13, 14]
, [21, 22, 23, 24]
, [31, 32, 33, 34]
, [41, 42, 43, 44]
] =>
[ [[11, 12], [13, 14]]
, [[21, 22], [23, 24]]
, [[31, 32], [33, 34]]
, [[41, 42], [43, 44]]
] =>
[ [ [[11, 12], [13, 14]]
  , [[21, 22], [23, 24]]
  ]
, [ [[31, 32], [33, 34]]
  , [[41, 42], [43, 44]]
  ]
] =>
[ [ [[11, 12], [13, 14]]
  , [[21, 22], [23, 24]]
  ]
, [ [[31, 32], [33, 34]]
  , [[41, 42], [43, 44]]
  ]
]

Можно заметить, что мы получили список двух матриц 2x2 содержащих списки двух элементов. Если их транспонировать, то получим

[ [ [[11, 12], [21, 22]]
  , [[13, 14], [23, 24]]
  ]
, [ [[31, 32], [41, 42]]
  , [[33, 34], [43, 44]]
  ]
]

и теперь каждая “строчка” содержит элементы квадрата 2х2 исходной матрицы. Осталось объединить строки:

[ [[11, 12], [21, 22]]
, [[13, 14], [23, 24]]
, [[31, 32], [41, 42]]
, [[33, 34], [43, 44]]
] =>
[ [11, 12, 21, 22]
, [13, 14, 23, 24]
, [31, 32, 41, 42]
, [33, 34, 43, 44]
]

Мы можем выразить это преобразование следующим образом:

boxes = map concat
      . concat
      . map transpose
      . (groupIn 3)
      . map (groupIn 3)

В свою очередь функцию groupIn можно записать в виде

groupIn :: Int -> [a] -> [[a]]
groupIn n xs = case splitAt n xs of
  (grp, []) -> [grp]
  (grp, rest) -> grp : groupIn n rest

или в бесточечной нотации:

groupIn :: Int -> [a] -> [[a]]
groupIn n = takeWhile (not . null)
          . uncurry (:) . fmap (groupIn n)
          . splitAt n

Законы

Мы можем вывести некоторые законы, которые выполняются для определённых здесь функций для данных, которые мы хотим обрабатывать.

Для начала,

rows . rows = id
cols . cols = id
boxes . boxes = id

Первые два закона достаточно очевидны, rows = id, cols = transpose, хотя доказать cols . cols = id исходя исключительно из определения достаточно сложно.

Докажем, однако, третье свойство. Во-первых, заметим, что

groupIn 3 . concat = id
concat . groupIn 3 = id

и обратим внимание, что

map f . map g = map (f . g)

(это прямо следует из закона композиции функторов)

Тогда:

boxes . boxes =
    map concat
  . concat
  . map transpose
  . groupIn 3
  . map (groupIn 3)
  . map concat
  . concat
  . map transpose
  . groupIn 3
  . map (groupIn 3)
=   map concat
  . concat
  . map transpose
  . groupIn 3
  . map (groupIn 3 . concat)
  . concat
  . map transpose
  . groupIn 3
  . map (groupIn 3)
=   map concat
  . concat
  . map transpose
  . groupIn 3
  . concat
  . map transpose
  . groupIn 3
  . map (groupIn 3)
=   map concat
  . concat
  . map transpose
  . map transpose
  . groupIn 3
  . map (groupIn 3)
=   map concat
  . concat
  . map (transpose . transpose)
  . groupIn 3
  . map (groupIn 3)
=   map concat
  . concat
  . groupIn 3
  . map (groupIn 3)
=   map concat
  . map (groupIn 3)
=   map (concat . groupIn 3)
=   map id
=   id

Аналогично можно вывести законы:

map rows . expand = expand . rows
map cols . expand = expand . cols
map boxes . expand = expand . boxes

Наконец, два закона касаются cartesianProduct, он же sequenceA:

fmap (fmap f) . cartesianProduct = cartesianProduct . fmap (fmap f)
filter (all p) . cartesianProduct = cartesianProduct . fmap (filter p)

Первый закон – закон натуральности: применение функции f к элементам возможно как до так и после вычисления декартова произведения.

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

Удаление вариантов

Наша спецификация, хотя выполнима в теории, на практике совершенно безнадёжна. Сетка состоит из 81 ячейки. Пусть из них заполнены 20, остаётся 61 ячейка, в каждой из которых может быть одна из 9 цифр. Итого имеем \(9^61\) вариантов или 16173092699229880893718618465586445357583280647840659957609 сеток.

Чтобы наш решатель был более эффективный, будем удалять “очевидно неправильные” варианты из ячеек. “Очевидно неправильные” в данном случае – это такие, которые сразу противоречат исходным данным, т.е. если в строке, столбце или квадрате есть ячейка с единственным вариантом, то из прочих ячеек это значение следует исключить.

Рассмотрим функцию

prune :: Matrix (Choice Digit) -> Matrix (Choice Digit)

такую, что

filter' valid . expand = filter valid . expand . prune

Как определить функцию prune? Для начала можно удалить “лишние” элементы из строк:

pruneRow :: Row (Choice Digit) -> Row (Choice Digit)
pruneRow row = map (remove fixed) row
  where fixed = [d | Choice [d] <- row]

remove :: [Digit] -> Choice Digit -> Choice Digit
remove _ (Choice [x]) = Choice [x]
remove fixed xs = filter' (`notElem` fixed) xs

Функция purneRow удовлетворяет уравнению

filter' nodups . cartesianProduct
  = filter' nodups . cartesianProduct . purneRow

Иными словами, purneRow не выбрасывает списки, не содержащие дубликатов.

Дополнительно нам понадобятся следующие уравнения, если f . f = id, то:

filter' (p . f) = map f . filter p . map f
filter' (p . f) . map f = map f . filter p

Они достаточно очевидные.

Теперь,

filter' valid . expand
 = filter' (all nodups . boxes)
 . filter' (all nodups . cols)
 . filter' (all nodups . rows)
 . expand

В свою очередь,

filter' (all nodups . boxes) . expand
 = map boxes . filter (all nodups) . map boxes . expand
 = map boxes . filter (all nodups) . expand . boxes
 = map boxes . filter (all nodups)
    . cartesianProduct . map cartesianProduct . boxes
 = map boxes . cartesianProduct
    . map (filter nodups)
    . map cartesianProduct . boxes
 = map boxes . cartesianProduct
    . map (filter nodups . cartesianProduct)
    . boxes

теперь используя свойство

filter nodups . cartesianProduct
 = filter nodups . cartesianProduct . pruneRow

перепишем

filter' (all nodups . boxes) . expand
 = map boxes . cartesianProduct
    . map (filter nodups . cartesianProduct . pruneRow)
    . boxes

оставшиеся преобразования по сути возвращают уравнение к исходному виду (но уже с pruneRow):

map boxes . cartesianProduct
  . map (filter nodups . cartesianProduct . pruneRow)
  . boxes
= map boxes . cartesianProduct
  . map (filter nodups)
  . map (cartesianProduct . pruneRow)
  . boxes
= map boxes . filter (all nodups)
  . cartesianProduct
  . map (cartesianProduct . pruneRow)
  . boxes
= map boxes . filter (all nodups)
  . cartesianProduct
  . map cartesianProduct
  . map pruneRow
  . boxes
= map boxes . filter (all nodups)
  . expand
  . map pruneRow
  . boxes
= filter (all nodups . boxes) . map boxes
  . expand
  . map pruneRow
  . boxes
= filter (all nodups . boxes)
  . expand
  . boxes
  . map pruneRow
  . boxes
= filter (all nodups . boxes)
  . expand
  . pruneBy boxes

где

pruneBy :: (Matrix (Choice Digit) -> Matrix (Choice Digit))
        -> Matrix (Choice Digit) -> Matrix (Choice Digit)
pruneBy f = f . map pruneRow . f

Мы таким образом показали, что

filter (all nodups . boxes) . expand
 = filter (all nodups . boxes) . expand . pruneBy boxes

Производя те же вычисления для rows и cols мы получаем

filter valid . expand
 = filter (all nodups . boxes) . expand . prune

где

prune = pruneBy boxes . pruneBy cols . pruneBy rows

Вообще говоря, prune может понадобятся применить несколько раз. Поэтому объявим функцию

many :: Eq a => (a -> a) -> a -> a
many f x
  | x == y = x
  | otherwise = many f y
  where y = f x

которая применяет функцию f до достижения неподвижной точки.

Итого получаем,

solve' :: InitialGrid -> Choice Grid
solve' = filter' valid . expand . many prune . choices

Последовательное решение

Результатом many prune . choices является матрица вариантов, которую можно поместить в одну из 3 категорий:

  1. Полная матрица, в которой каждая ячейка имеет ровно один вариант
  2. Матрица, не имеющая в какой-то ячейке вариантов
  3. Матрица, не содержащая “пустых” вариантов, но имеющая где-то больше одного варианта.

В третьем случае, до сих пор мы инстанцировали все возможные варианты и проверяли по очереди удовлетворяют ли полученные матрицы требованиям. Более удачная идея – инстанцировать выбор только в одной ячейке, затем повторять many prune и исключать матрицы из категории 2.

Нашей задачей таким образом является сконструировать функцию

expand1 :: Matrix (Choice Digit) -> [Matrix (Choice Digit)]

которая произведёт экспансию только для одной ячейки. Для какой ячейки? Наиболее выигрышной кажется стратегия производить в первую очередь экспансию ячеек с наименьшим числом вариантов (само собой больше 1)

Определим expand1:

expand1 :: Matrix (Choice Digit) -> Choice (Matrix (Choice Digit))
expand1 rows = Choice
  [ rowsl <> (midrow c : rowsr) | c <- cs ]
  where
  midrow c = rowl <> (Choice [c] : rowr)
  (rowsl, row: rowsr) = break (any smallest) rows
  (rowl, Choice cs: rowr) = break smallest row
  smallest choices = length choices == minChoices
  minChoices = minimum (counts rows)
  counts = filter (>1) . map length . concat

singleton :: Choice a -> Bool
singleton (Choice [_]) = True
singleton _ = False

Некоторая трудность здесь в том, что функция expand1 является частичной из-за использования minimum и шаблонов требующих непустого списка после break, т.е. передавать ей на вход сетки без вариантов или полностью заполненные сетки – нельзя, это приведёт к ошибке времени выполнения. Поэтому определим функцию search, имеющую следующий вид:

search :: Matrix (Choice Digit) -> Choice (Matrix (Choice Digit))
search g
  | all (all singleton) p = Choice [p]
  | any (any null) p = Choice []
  | otherwise
  = join . fmap search . expand1 $ p
  where p = prune g

Тогда можем переписать функцию solve в виде:

solve'' :: InitialGrid -> Choice Grid
solve'' = filter' valid . join . fmap expand . search . choices

Упражнения

Упражнение 1

Докажите законы, доказательство которых опущено в этом изложении:

map rows . expand = expand . rows
map cols . expand = expand . cols
map boxes . expand = expand . boxes
fmap (fmap f) . cartesianProduct
  = cartesianProduct . fmap (fmap f)
filter (all p) . cartesianProduct
  = cartesianProduct . fmap (filter p)
filter' nodups . cartesianProduct
  = filter' nodups . cartesianProduct . purneRow
-- если f . f = id
filter' (p . f) = map f . filter p . map f
filter' (p . f) . map f = map f . filter p

Упражнение 2

Реализуйте программу, принимающую на вход частично заполненную сетку судоку, и выводящую возможные решения.

Во входе, строчки сетки разделяются переносами строки, а ячейки в строке идут подряд, пропуски – пробелами, например:

53  7
6  195
 98    6
8   6   3
4  8 3  1
7   2   6
 6    28
   419  5
    8  79

В выводе, разделяйте ячейки пробелами, каждые 3 строки вставляйте пустую строку, каждые 3 столбца – дополнительный пробел, например:

5 3 4  6 7 8  9 1 2
6 7 2  1 9 5  3 4 8
1 9 8  3 4 2  5 6 7

8 5 9  7 6 1  4 2 3
4 2 6  8 5 3  7 9 1
7 1 3  9 2 4  8 5 6

9 6 1  5 3 7  2 8 4
2 8 7  4 1 9  6 3 5
3 4 5  2 8 6  1 7 9

Как вариант, каждые 3 строки выводите 21 символ - и каждые 3 столбца выводите |, например:

5 3 4 | 6 7 8 | 9 1 2
6 7 2 | 1 9 5 | 3 4 8
1 9 8 | 3 4 2 | 5 6 7
---------------------
8 5 9 | 7 6 1 | 4 2 3
4 2 6 | 8 5 3 | 7 9 1
7 1 3 | 9 2 4 | 8 5 6
---------------------
9 6 1 | 5 3 7 | 2 8 4
2 8 7 | 4 1 9 | 6 3 5
3 4 5 | 2 8 6 | 1 7 9

Для вставки элементов можно использовать функцию

Data.List.intersperse :: a -> [a] -> [a]

которая вставляет первый аргумент между всеми элементами второго:

intersperse 0 [1..5] == [1,0,2,0,3,0,4,0,5]