Типизируя техническое интервью

Предлагаю читателям "Хабрахабра" перевод статьи Kyle Kingsbury, a.k.a "Aphyr".
Ранее: Заклиная техническое интервью

В прежние времена, задолго до восхода Церкви, все заклятья произносились по чистому случаю, все действия были разрешены, а смерть была обыденностью. Многие ведьмы покалечились из-за своей магии, их находили изломанными в центре круга искривленных, застеклившихся деревьев и горящих камней, не гаснущих даже под водой; некоторые полностью исчезали, или начинали путешествовать по горным перевалам, никогда не касаясь ногами земли, никогда не согревая воздух своим дыханием.

Еще ребенком ты услышала историю о Гульвейг-затем-Хьёр, возродившейся трижды из судного огня, которая путешествовала по миру, совершая seidr — прочтение и сплетение заново будущего. Ее предсказания (а их было множество) стали знаменитыми — их повторяли даже ходящие-за-краем-мира — но историю изменило ее выживание. В экстатическом трансе seidr она провидела свое будущее, и победила смерть. Ее заклятья никогда не ломались, и она стала другом для изгнанных женщин, предков твоего рода. Говорят, что сам Один научился бессмертию от нее.

По сей день все ведьмы в долгу перед Хьёр. Лишь немногие ныряют в древнюю, неструктурированную магию в наши дни. Сами языки, на которых написаны заклятья, стабилизированы самим seidr в своей структуре, проводя вызываемую энергию по безопасным путям — в большей или меньшей степени. Конечно, иногда происходят случайные взрывы. Но они по большей части из разновидности сжигающих брови, а не создающих новые фьорды интересных очертаний.

"Всё хорошо?"

Собеседующий — Крис, судя по имени на бейдже — довольно юн, что соответствует обычаю Долины. Он носит толстовку, которая, судя по отсутствию торговых марок, стоит как минимум сотни три долларов. Он вообще не напоминает ни одно животное, что заставляет тебя задуматься. Обычно такие вещи даются тебе легко.

"Имеешь в виду вообще? Не думаю", — ты осматриваешь конференц-зал, как будто ища подтверждения. Стены пахнут уходом от конфликтов и сообщениями Slack.

"Ну, эм, хорошо. Да, наверное ты права". его голос звучит робко. "Но тем не менее я хотел бы провести небольшое упражнение. Простую программистскую задачку, чтоб я мог понять как ты решаешь проблемы".

Как-то раз ты решила проблему при помощи ножа из осколка обсидиана. Ты раздумываешь о том, имеет ли Крис достаточно сил, чтобы повторить совершенное тобой.

"Таак… эта задачка называется N-ферзей, и она довольно простая. Имея шахматную доску размером NxN, тебе надо найти способ безопасно разместить N королев на этой доске".

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

"Э, нет — это неправильно. Видишь? Эта королева одним ходом может срубить любую их этих четырех".

"Ты действительно не в состоянии", — спрашиваешь ты голосом, холодным как камень, — "вообразить восьмерых могущественных женщин в одной комнате, которые не стремятся друг друга убить?"

"Э… это просто постановка задачи".

Наверное это матриархи враждующих кланов. Собрались обсудить перемирие — но ни одна не доверяет другой, если та может дотянуться кинжалом. Такое тоже происходило в истории твоего рода.

"Я могу использовать любой язык?"

"Конечно."

Действуй быстро, пока он не понял своей ошибки.

{-# OPTIONS_GHC -fno-warn-missing-methods #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}

"А, это Haskell! Я его учил в коллежде!". Он замолкает и фыркает. "Undecidable instances?"

"Нам придется это использовать", — радостно информируешь ты его, "поскольку Hask не категория".

"А, правильно", — Крис выдает свое неокончательное мнение, ни к кому особенно не обращаясь. "Поэтому мы обычно мыслили в подмножествах Хаскеля, где у типов не было нижних значений".

"Можно и так", — соглашаешься ты, но слишком тихо для того, чтобы Крис тебя услышал, будучи тем временем полностью уверенной в обратном.

nil = undefined

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

"Конечно, или вектор".

"Списки проще".

"Окей, хорошо, используй что тебе удобней".

Вызываешь из пустоты связный список. Тот плавает по поверхности экрана: классическая структура, выражаемая тысячью способов, но неизменно прекрасная. Ты удовлетворенно вздыхаешь.

data Nil
data Cons x xs

"А нельзя ли было воспользоваться встроенными списками?" — спрашивает Крис, чья бровь ползет вверх.

"Что?" — ты представления не имеешь о чем он говорит. "О, нет — тогда нам придется тащить сюда всю библиотеку. Проще определить их внутри".

class First list x | list -> x
instance First Nil Nil
instance First (Cons x more) x

"Ключевое слово 'class' определяет сигнатуру функции" — напоминаешь ты Крису, который вроде как кое-что забыл. "First принимает список и возвращает значение x из него. У функции два экземпляра — Haskell использует pattern matching, чтобы выбрать который вызывать. First от списка Nil возвращает Nil, а First от ячейки Cons возвращает значение ячейки, x".

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

class ListConcat a b c | a b -> c
instance ListConcat Nil x x
instance (ListConcat as bs cs)
  => ListConcat (Cons a as) bs (Cons a cs)

"А что за стрелка?" — спрашивает Крис. Говоришь ему, что она означает импликацию. "Чтобы получить ListConcat после стрелки, нам нужен ListConcat до стрелки".

Брезжит понимание. "А. правильно! Это рекурсия, поскольку ListConcat появляется с обеих сторон. А определение с Nil — это базовый случай".

"Именно". Ты так гордишься Крисом. Он идет точно в ногу. "А это генерализованный случай, когда мы хотим склеить список списков".

-- Concatenate all lists in a list
class ListConcatAll ls l | ls -> l
instance ListConcatAll Nil Nil
instance (ListConcat chunk acc result,
          ListConcatAll rest acc)
  => ListConcatAll (Cons chunk rest) result

-- Is any element of this list True?
class AnyTrue list t | list -> t
instance AnyTrue Nil              False
instance AnyTrue (Cons True more) True
instance (AnyTrue list t)
  => AnyTrue (Cons False list) t

Это потребовало большей концентрации, чем тебе по нраву, так что отступаем к чему попроще. "Давай займемся булевыми значениями", предлагаешь ты тоном, которым обычно приглашают на обед.

"Зачем?"

"Потому что они нам нужны, конечно"

Хватаешь из пустоты две бессмысленных константы, и наполняешь их смыслом.

data True
data False

class Not b1 b | b1 -> b
instance Not False True
instance Not True  False

class Or b1 b2 b | b1 b2 -> b
instance Or True  True  True
instance Or True  False True
instance Or False True  True
instance Or False False False

Фрейя, наверное, порадуется. Рождение алгебры в мир — прекрасное событие.

"И я полагаю, что еще нам понадобятся интегральные числа, чтобы хранить координаты наших королев" — бормочешь ты. "Мы работаем исключительно в положительных координатах, так что обычной конструкции Пеано будет достаточно". Выдергиваешь волос из прически и завязываешь на нём узелок для ноля.

data Z
data S n

type N0 = Z
type N1 = S N0
type N2 = S N1
type N3 = S N2
type N4 = S N3
type N5 = S N4
type N6 = S N5
type N7 = S N6
type N8 = S N7

"Ты… определяешь натуральные числа вручную? Зачем?"

"Haskell — для математиков", — объясняешь ты, "Мы всегда определяем свои термины."

-- Equality
class PeanoEqual a b t | a b -> t
instance PeanoEqual Z     Z     True
instance PeanoEqual (S a) Z     False
instance PeanoEqual Z     (S b) False
instance (PeanoEqual a b t)
  => PeanoEqual (S a) (S b) t

-- Comparison (<)
class PeanoLT a b t | a b -> t
instance PeanoLT Z      Z     False
instance PeanoLT (S x)  Z     False
instance PeanoLT Z      (S x) True
instance (PeanoLT a b t)
  => PeanoLT (S a) (S b) t

-- Absolute difference
class PeanoAbsDiff a b c | a b -> c
instance PeanoAbsDiff Z Z Z
instance PeanoAbsDiff Z (S b) (S b)
instance PeanoAbsDiff (S a) Z (S a)
instance (PeanoAbsDiff a b c)
  => PeanoAbsDiff (S a) (S b) c

-- Integers from n to 0
class Range n xs | n -> xs
instance Range Z Nil
instance (Range n xs)
  => Range (S n) (Cons n xs)

"Стой, погоди" — прерывает Крис. "А разве не… разве не надо здесь декларацию типа? Ну хотя бы для функций?"

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

Крис выглядит так, как будто проглотил лягушку.

"Смотри, я покажу. Давай проверим, равняется ли один одному."

class LegalCompare t | -> t
  where legalCompare :: t
instance (PeanoEqual (S Z) (S Z) t)
  => LegalCompare t

*Main> :type legalCompare
legalCompare :: True

"Видишь? legalCompare равен True. А теперь давай попробуем записать выражение, которое проводит некорректное сравнение. Например, давай сравним True и List?"

class IllegalCompare t | -> t
  where illegalCompare :: t
instance (PeanoEqual True (Cons Z False) t)
  => IllegalCompare t

"Видишь? Загружается отлично. Сломается только когда мы попытаемся выполнить выражение — вспомни, Haskell ведь ленивый".

*Main> :type illegalCompare
illegalCompare :: PeanoEqual True (Cons Z False) t => t

"Вот, пожалуйста! Ошибка типа в рантайме".

"Но про ошибку ничего не написано..."

"Ну, знаешь ли. Сообщения об ошибках Haskell широко известны своей сложностью для понимания".

Крис выглядит довольно больным. Воспользуйся возможностью перейти к функциям высшего порядка.

"По несчастливому стечению обстоятельств, в Haskell нет каррирования, так что нам придется создать собственный инструментарий для частичного применения функций. Вот сигнатура для генерализованного одно-арного применения функции".

class Apply f a r | f a -> r

"Просто функция f, которая принимает ввод a и возвращает r", — мелодия имён переменных звучит почти как песня. "Для частичного применения мы могли бы определить типы данных вроде Partial1, Partial2 и так далее, но поскольку нам нужны только некоторые из них, проще определить строго каррированные версии функций, которые нам понадобятся. Например так!"

data Conj1 list
instance Apply (Conj1 list) x (Cons x list)

Глубоко вдыхаешь, и позволяешь своему духу воспарить от этих конкретных форм к сияющим высотам функций высшего порядка.

-- Map f over a list
class Map f xs ys | f xs -> ys
instance Map f Nil Nil
instance (Apply f x y, Map f xs ys)
  => Map f (Cons x xs) (Cons y ys)

-- Map f over list and concatenate results together
class MapCat f xs zs | f xs -> zs
instance MapCat f Nil Nil
instance (Map f xs chunks, ListConcatAll chunks ys)
  => MapCat f xs ys

-- Filter a list with an Apply-able predicate function
class AppendIf pred x ys zs | pred x ys -> zs
instance AppendIf True x ys (Cons x ys)
instance AppendIf False x ys ys

class Filter f xs ys | f xs -> ys
instance Filter f Nil Nil
instance (Apply f x t,
          Filter f xs ys,
          AppendIf t x ys zs)
  => Filter f (Cons x xs) zs

На мгновение надо вернуться в мир конкретных значений. Крис всё еще тут, по крайней мере физически. Экран твоего ноутбука превратился в роскошное месиво фиолетовых тонов, благодаря крайнему холоду, но код все еще различим в его глубинах. Экран напоминает тебе замерзшее озеро в сумерках. Жидкий кристалл.

"Крис. Крис." Тот быстро моргает, как будто попал из тьмы на свет. Красивые глаза. Ты вспоминаешь времена, когда твои собственные глаза еще имели цвет. "Мы готовы."

"Да. Хорошо."

"Королева определяется ее двумя координатами на доске: x и y. Еще мы создадим частично применяемый конструктор, чтобы ставить королев на заданной координате x".

data Queen x y
data Queen1 x
instance Apply (Queen1 x) y (Queen x y)

-- A list of queens in row x with y from 0 to n.
class QueensInRow n x queens | n x -> queens
instance (Range n ys, Map (Queen1 x) ys queens)
  => QueensInRow n x queens

"Да, королевы!" — бурчишь ты. Это, к сожалению не тот вид интервью.

Каждая королева может ударить по восьми направлениям. Ты всегда полагала, что это метафора.

-- Does queen a threaten queen b?
class Threatens a b t | a b -> t
instance (PeanoEqual ax bx xeq,
          PeanoEqual ay by yeq,
          Or xeq yeq xyeq,
          PeanoAbsDiff ax bx dx,
          PeanoAbsDiff ay by dy,
          PeanoEqual dx dy deq,
          Or xyeq deq res)
  => Threatens (Queen ax ay) (Queen bx by) res

-- Partial application of Threatens
data Threatens1 a
instance (Threatens a b t)
  => Apply (Threatens1 a) b t

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

-- Is queen b compatible with all queen as?
class Safe config queen t | config queen -> t
instance (Map (Threatens1 queen) config m1,
          AnyTrue m1 t1,
          Not     t1 t2)
  => Safe config queen t2

data Safe1 config
instance (Safe config queen t)
  => Apply (Safe1 config) queen t

-- Add a queen with the given x coordinate to a legal configuration, returning
-- a set of legal configurations.
class AddQueen n x c cs | n x c -> cs
instance (QueensInRow n x candidates,
          Filter (Safe1 c) candidates filtered,
          Map (Conj1 c) filtered cs)
  => AddQueen n x c cs

data AddQueen2 n x
instance (AddQueen n x c cs)
  => Apply (AddQueen2 n x) c cs

-- Add a queen at x to every configuration, returning a set of legal
-- configurations.
class AddQueenToAll n x cs cs' | n x cs -> cs'
instance (MapCat (AddQueen2 n x) cs cs')
  => AddQueenToAll n x cs cs'

"А теперь мы входим в рекурсию", — шепчешь ты, обращая заклятие, скрепленное контролирующим тредом, на само себя. По одной королеве на ряд, в каждой валидной позиции, для каждой конфигурации. Ты представляешь себе, как могла бы выглядеть страничка "о нас" на сайте их стартапа.

-- Add queens recursively
class AddQueensIf pred n x cs cs' | pred n x cs -> cs'
instance AddQueensIf False n x cs cs
instance (AddQueenToAll n x cs cs2,
          AddQueens n (S x) cs2 cs')
  => AddQueensIf True n x cs cs'

class AddQueens n x cs cs' | n x cs -> cs'
instance (PeanoLT x n pred,
          AddQueensIf pred n x cs cs')
  => AddQueens n x cs cs'

-- Solve
class Solution n c | n -> c where
  solution :: n -> c
instance (AddQueens n Z (Cons Nil Nil) cs,
          First cs c)
  => Solution n c where solution = nil

Крис привычно смотрит сквозь всё, как человек, испытавший страшную потерю или, может быть, ставший свидетелем близкого взрыва. Нежно берешь его за плечо. "Псст!", — шепчешь ты,- "Всё готово, решение близко".

*Main> :type solution (nil :: N6)
solution (nil :: N6)
  :: Cons (Queen (S (S (S (S (S Z))))) (S Z))
       (Cons (Queen (S (S (S (S Z)))) (S (S (S Z))))
          (Cons (Queen (S (S (S Z))) (S (S (S (S (S Z))))))
             (Cons (Queen (S (S Z)) Z)
                (Cons (Queen (S Z) (S (S Z)))
                   (Cons (Queen Z (S (S (S (S Z)))))
                      Nil)))))

Глянь-ка, красивый вывод разположил выдачу именно так, создав прелестую линию нулей по вертикальной оси. "Так, у нас королевы на 5,1, на 4,3, на 3, 5, на 2,0, 1,2, и 0,4. Пойдет, Крис?"

Крис пялится на тебя очень, очень долго. "Ты ни ни разу… ни разу не написала настоящее значение. Ты… ты ведь понимаешь, что система типов должна содержать значения, правда?"

"Нет", — информируешь ты его, как заместитель Капитана Очевидность. "Нет, это не так".

Тот откидывается в своем кресле так далеко, что ты думаешь что он вот-вот перевернётся, а затем трёт свое лицо обеими руками. Ты, уже видя сквозь seidr email с отказом, знаешь что он собирается сказать.

"Мы с вами свяжемся".

С искренней благодарностью Патрику Томпсону и Type Level Insanity Конрада Паркера.