[Перевод] Неупакованные типы объединений в Scala на основе изоморфизма Карри-Ховарда
Примечание переводчика. В будущей версии Scala (“Don Giovanni”) анонсирована поддержка типов объединения (union types). Miles Sabin, широко известный в узких кругах как создатель Shapeless, демонстрирует в этой статье 2011 года, как создать типы объединения уже сейчас.
Scala имеет очень выразительную систему типов. Однако она не включает (по крайней мере как примитивы) всех вожделенных элементов. Есть несколько поистине полезных типов, подпадающих под эту категорию — это типы полиморфных функций высшего ранга (higher-rank) и рекурсивные структурные типы. Но о них я расскажу подробнее в следующих постах, а сегодня я собираюсь показать вам, как в Scala мы можем создать типы объединения (union types). В ходе объяснения я пролью немного света на изоморфизм Карри-Ховарда и покажу, как использовать его в наших целях.
Итак, для начала, что такое тип объединения? Тип объединения это во многом то, чего вы от него ожидаете: объединение двух (или больше, но я ограничусь только двумя) типов. Значения этого типа включают все значения каждого из объединяемых типов. Что это значит нам поможет выяснить пример, но для начала введём систему обозначений. По причинам, которые станут вскоре понятны, я буду записывать объединение типов T и U с помощью символа операции ИЛИ: T ∨ U. Таким образом объединение типов Int и String записывается как Int ∨ String. Значения этого типа объединения включают все значения типа Int и все значения типа String.
Но что же это значит более конкретно? А значит это то, что если бы мы имели возможность напрямую выразить такой тип в Scala, то мы смогли бы, к примеру, написать так:
def size(x: Int ∨ String) = x match {
case i: Int => i
case s: String => s.length
}
size(23) == 23 // OK
size("foo") == 3 // OK
size(1.0) // Не OK, ошибка компиляции
Другими словами, метод size может принимать аргументы либо типа Int, либо типа String (включая их подтипы Null и Nothing), и никакие другие.
Важно подчеркнуть отличие между использованием этого типа объединения и станадартного Either. Either, известный как тип суммы (sum type), это аналог типа объединения в языках не поддерживающих подтипы. Переписывание нашего примера с использованием Either даст нам:
def size(x: Either[Int, String]) = x match {
case Left(i) => i
case Right(s) => s.length
}
size(Left(23)) == 23 // OK
size(Right("foo")) == 3 // OK
Тип Either[Int, String] может моделировать тип объединения Int ∨ String, так как между ними и их значениями существует соответствие (изоморфизм). Однако абсолютно ясно, что тип Either добивается этого будучи дополнительным уровнем упакованного (boxed) представления, а не как неупакованный (unboxed) примитив системы типов. Можем ли мы создать нечто лучшее, чем Either? Можем ли мы найти способ представления типов объединения в Scala без привлечения упаковки и со всеми ожидаемыми статическими гарантиями?
Оказывается, что мы можем, но на пути к результату нам необходимо совершить объезд через логику первого порядка с помощью изоморфизма Карри-Ховарда. Данный изоморфизм говорит нам, что отношения между типами в системе типов могут рассматриватья как образ отношений между высказываниями в логической системе (и наоборот). Мы можем интерпретировать данное утверждение различными способами в зависимости от того, о какой системе типов мы говорим, и какую логическую систему мы выбрали, но для для нашего обсуждения я проигнорирую большинство деталей и сосредоточусь на простых примерах.
Проиллюстрируем изоморфизм Карри-Ховарда в контексте системы типов с подтипами как в Scala. Можно заметить, что существует соответствие между типами пересечения (A with B) и логической конъюнкцией (A ∧ B); между моими гипотетическими типами объединения (A ∨ B) и логической дизъюнкцией (так же A ∨ B, на что был сделан намёк выше); и между подтипами (A <: B) и логической импликацией (A ⇒ B). В левой колонке представленной ниже таблицы мы имеем отношения подтипов выполняемые в Scala (но в случае типов объединения не выражаемые напрямую в языке), а в правой колонке мы имеем логические формулы полученные из отношений между типами слева путём простой замены with на ∧ и <: на ⇒. В каждом из случаев такая замена даёт логически верную формулу.
| (A with B) <: A | (A ∧ B) ⇒ A |
| (A with B) <: B | (A ∧ B) ⇒ B |
| A <: (A ∨ B) | A ⇒ (A ∨ B) |
| B <: (A ∨ B) | B ⇒ (A ∨ B) |
Суть изоморфизма Карри-Ховарда в том, что механический процесс замены всегда сохраняет корректность — верная типовая формула всегда переписывается в верную логическую формулу, и наоборот. И это выполняется не только для конъюнкции, дизъюнкции и импликации. Мы также можем обобщить соответствие на логические формулы включающие отрицание (ключевая операция в сегодняшнем рассмотрении) и кванторы общности и существования.
Что же будет для нас значить добавление отрицания? Конъюнкция двух типов (т.е. A with B) имеет значения, которые являются экземплярами одновременно и A, и B. Подобным же образом мы можем предполагать, что отрицание типа A (я буду записывать его как ¬[A]) должно иметь значения, которые не являются экземплярами типа A. Отрицание также не может быть напрямую выражено в языке Scala, но к чему мы придём, предположив, что это не так?
В таком случае мы могли бы использовать изоморфизм Карри-Ховарда и законы Де Моргана, чтобы получить определение типов объединения из типов пересечения и отрицания. Вот как это мого бы получиться…
Для начала вспомним равенство Де Моргана:
(A ∨ B) ⇔ ¬(¬A ∧ ¬B)
Затем применим изоморфизм Карри-Ховарда (используя операцию эквивалентности =:= языка Scala):
(A ∨ B) =:= ¬[¬[A] with ¬[B]]
Если бы мы только могли найти способ записи этого в Scala, то наша цель была бы достигнута и мы бы имели наши типы объединения. Так можем ли мы выразить отрицанение типа в Scala?
К сожалению, мы не можем. Но, что мы можем сделать, так это преобразовать все наши типы таким образом, чтобы сделать возможным запись отрицания в преобразованном контексте. Затем нам понадобится найти способ завставить всё это работать в оригинальном непреобразованном контексте.
Некоторые читатели возможно были немного удивлены, когда я ранее проиллюстрировал изоморфизм Карри-Ховарда используя типы пересечения в паре с конъюнкцией, типы объединения в паре с дизъюнкцией и отношение подтипов в паре с импликацией. Обычно же типы произведения (product types), т.е. (A, B) моделируют конъюнкцию, типы суммы (Either[A, B]) моделируют дизъюнкцию и типы функций моделируют импликацию. Если мы перепишем нашу предыдущую таблицу с использованием произведений, сумм и функций, то получим следующее:
| (A, B) => A | (A ∧ B) ⇒ A |
| (A, B) => B | (A ∧ B) ⇒ B |
| A => Either[A, B] | A ⇒ (A ∨ B) |
| B => Either[A, B] | B ⇒ (A ∨ B) |
В левой части мы больше не ожидаем корректности с точки зрения отношения подтипов, вместо этого нам необходимо соблюдение принципа параметричности, который позволяет нам определить может ли тип функции быть реализован исходя только лишь из сигнатуры функции. Очевидно, что все сигнатуры функций в левой колонке могут быть реализованы. Для первых двух случаев мы имеем пару (A, B) как аргумент нашей функции, поэтому мы легко можем получить из этой пары значение типа A или B, использовав _1 или _2:
val conj1: ((A, B)) => A = p => p._1
val conj2: ((A, B)) => B = p => p._2
Во втором и третьем случае аргументами функции являются значения типа A и B соответственно, поэтому мы можем получить результат типа Either[A, B] воспользовавшись конструкторами Left[A] и Right[B]:
val disj1: A => Either[A, B] = a => Left(a)
val disj2: B => Either[A, B] = b => Right(b)
Именно в такой форме изоморфизм Карри-Ховарда обычно выражается для языков без подтипов. Однако типы объединения, также как и типы пересечения, по своей сути основаны на подтипах. Поэтому рассмотренное отображение ни в коей степени не поможет нам с объединением. Зато оно может помочь нам с отрицанием, которое является той самой недостающей деталью пазла.
С подтипами или без, наименьший тип (bottom type), представленный в Scala как Nothing, отображается в логическую ложь. Например, все следующие равенства справедливы:
| A => Either[A, Nothing] | A ⇒ (A ∨ false) |
| B => Either[Nothing, B] | B ⇒ (false ∨ B) |
Это следует из того, что все сигнатуры функций слева реализуемы, а логические формулы справа верны (пост Джеймса Айри объясняет почему я не показываю случай соответствия произведений/конъюнкций). Теперь подумаем, что соответствует функции со следующей сигнатурой:
A => Nothing
На правой логической стороне изоморфизма Карри-Ховарда эта сигнатура отображается в формулу A ⇒ false, которая эквивалентна ¬A. Это кажется вполне интуитивно разумным — не существует значений типа Nothing, следовательно сигнатура A => Nothing не может быть реализована (кроме как выбрасыванием исключения, но в нашем случае это не позволено).
Теперь давайте посмотрим, что будет, если мы используем эту сигнатуру как наше представление отрицания типа,
type ¬[A] = A => Nothing
и применим его в контексте законов Де Моргана, чтобы получить тип объединения:
type ∨[T, U] = ¬[¬[T] with ¬[U]]
Теперь мы можем проверить наш тип используя Scala REPL:
scala> type ¬[A] = A => Nothing
defined type alias $u00AC
scala> type ∨[T, U] = ¬[¬[T] with ¬[U]]
defined type alias $u2228
scala> implicitly[Int <:< (Int ∨ String)]
<console>:11: error: Cannot prove that Int <:<
((Int) => Nothing with (String) => Nothing) => Nothing.
implicitly[Int <:< (Int ∨ String)]
REPL показывает нам, что решение ещё не совсем получено. Выражение implicitly[Int <:< (Int ∨ String)] спрашивает компилятор, может ли он доказать, что Int является подтипом Int ∨ String, что должно быть справедливо для типа объединения.
Что же пошло не так? Проблема в том, что мы преобразовали типы в правой части оператора <:< в типы функций, чтобы использовать отрицание типа, заданное как A => Nothing. Это значит, то сам тип объединения является типом функции. Но это, очевидно, не согласуется с тем, чтобы Int был подтипом типа объединения, что и показывает сообщение об ошибке от REPL. Чтобы устранить ошибку мы должны также преобразовать левую часть оператора <:< в тип, который был бы подтипом типа в правой части. Какой же может быть эта трансформация? Как насчёт двойного отрицания?
type ¬¬[A] = ¬[¬[A]]
Давайте посмотрим, что на это скажет компилятор:
scala> type ¬¬[A] = ¬[¬[A]]
defined type alias $u00AC$u00AC
scala> implicitly[¬¬[Int] <:< (Int ∨ String)]
res5: <:<[((Int) => Nothing) => Nothing,
((Int) => Nothing with (String) => Nothing) => Nothing] =
<function1>
scala> implicitly[¬¬[String] <:< (Int ∨ String)]
res6: <:<[((String) => Nothing) => Nothing,
((Int) => Nothing with (String) => Nothing) => Nothing] =
<function1>
Бинго! И ¬¬[Int], и ¬¬[String] являются подтипами Int ∨ String!
Теперь надо проверить, что мы не просто каждый раз возвращаем положительный ответ:
scala> implicitly[¬¬[Double] <:< (Int ∨ String)]
<console>:12: error: Cannot prove that
((Double) => Nothing) => Nothing <:<
((Int) => Nothing with (String) => Nothing) => Nothing.
Итак, мы практически закончили, осталось нанести последние штрихи. Отношения подтипов, которые мы имеем, изоморфны тем, какие мы хотим получить (поскольку тип ¬¬[T] изоморфен T). Но у нас пока что нет способа выразить те же отношения с непреобразованными типами, что нам как раз и необходимо.
Мы можем решить эту проблему считая ¬[T], ¬¬[T] и T ∨ U фантомными типами и используя их только, чтобы представить требуемые отношения подтипов, а не работая напрямую со значениями данных типов. Вот как это происходит на нашем тестовом примере:
def size[T](t: T)(implicit ev: (¬¬[T] <:< (Int ∨ String))) =
t match {
case i: Int => i
case s: String => s.length
}
Здесь используется обобщённое ограничение типа, требующее, чтобы компилятор мог доказать, что любой T, выведенный как аргумент типа для метода size, удовлетворяет тому, что его двойное отрицание является подтипом Int ∨ String. Как показывает следующая сессия REPL данное условие выполняется только, если T — это Int или String:
scala> def size[T](t: T)(implicit ev: (¬¬[T] <:< (Int ∨ String))) =
| t match {
| case i: Int => i
| case s: String => s.length
| }
size: [T](t: T)(implicit ev: <:<[((T) => Nothing) => Nothing,
((Int) => Nothing with (String) => Nothing) => Nothing])Int
scala> size(23)
res8: Int = 23
scala> size("foo")
res9: Int = 3
scala> size(1.0)
<console>:13: error: Cannot prove that
((Double) => Nothing) => Nothing <:<
((Int) => Nothing with (String) => Nothing) => Nothing.
А теперь последняя хитрость. С точки зрения синтаксиса неявный параметр доказательства смотрится уродливо и тяжеловесно, однако мы можем это исправить преобразовав его в контекстное ограничение параметра типа T:
type |∨|[T, U] = { type λ[X] = ¬¬[X] <:< (T ∨ U) }
def size[T: (Int |∨| String)#λ](t: T) =
t match {
case i: Int => i
case s: String => s.length
}
Готово! Мы получили незапакованное, статически типобезопасное представление типов объединения в Scala, без модификации самого языка!
Естественно было бы лучше, если бы Scala поддерживала типы объединения как примитивы. Но по крайней мере полученное нами решение демонстрирует, что компилятор Scala имеет всю необходимую информацию, чтобы сделать это. Теперь осталось только донимать Мартина и Адриаана, чтобы они сделали типы объединения доступными напрямую.
