Alexander Kuklev (akuklev) wrote,
Alexander Kuklev
akuklev

Category:

Scala distilled

Женя xeno_by сказал, чем ему нравится Скала; что-ж, попробую и я.

Мне всегда казалось, что язык программирования (ну и proof assistant, это же одно и то же), должен в первую очередь уметь отражать математические концепции без скидок, по честному. Чтаобы на языке можно было с одинаковой лёгкостью работать в рамках стандартной теории множеств (ZFC) или теории зависимых типов, как она реализована в Agda 2.

Для этого нужно, чтобы полиморфизм был синтаксическим (erasure polymorphism), т.е. типы (например «натуральное число» или «действительное число») сперва рассматривались чисто как ярлычки, привязанные к термам, и лишь на следующем этапе совершалась привязка содержательного, то есть появлялись term-level объекты, связанные с ярлычками — ассоциированные с типами модели. Scala обладает именно таким полиморфизмом является базовой причиной её гибкости.

Рассмотрим на конкретном примере в идеализированном варианте Scala, как это может работать. Итак, возьмём функцию
foo[T](x: T, y: T)

Это функция полиморфная по T, принимающая два аргумента типа T. Что мы можем с ними сделать? Решительно ничего! Не бывает никаих операций, определённых для любых объектов любых типов.

Как сделать, чтобы с ними что-то можно было делать? Указать «тип типа X», чтобы какие-то операции появились. Например, так:
foo[T: Set](x: T, y: T)

Тут написано, что T удовлетворяет сигнатуре Set. Для простоты скажем, что эта сигнатура содержит только одну операцию — операцию сравнения. То есть:
type Set[T] = {
  def checkEquality(x: T, y: T): Boolean
}

Теперь можно дешивровать запись foo[T: Set](x: T, y: T)! Эта запись означает
foo[T](implicit T: Set[T])(x: T, y: T)

То есть данная функция прежде чем принять аргументы x и y хочет втихомолку принять скрытый аргумент — модель типа Set, ассоциированную с T. Я назвал модель той же буквой просто для удобства, по смыслу мы всегда сможем различить, имеется ли в виду тип или ассоциированная с ним модель. Итак, что мы теперь можем написать в тело функции foo? Теперь у нас уже есть как минимум одна операция над объектами типа T, мы умеем их сличать!
Мы можем определить например такую функцию:
foo[T: Set](x: T, y: T) = !T.checkEquality(x, y)

Эта функция сличает x и y и обращает результат. Обратите внимание, что операция checkEquality берётся не из воздуха, а из модели, ассоциированного с типом T. Используя дополнительный синтаксический сахар можно конечно писать просто foo[T: Set](x: T, y: T) = (x == y), но в данном случае это только путает картину.

Для объектов, на которых определён частичный порядок, можно определить функцию сортировки:
sort[T: Ordered](xs: Collection[T]): List[T]


Ну и так далее, я думаю вы поняли идею. Итак, что нам для этого нужно? Нам нужны встроенные в язык примитивы «сигнатура» (trait) и «модель» (object), то есть кортеж с именованными и типизированными элементами, который может соответствовать или не соответствовать той или иной сигнатуре. Очень важно, что модели/сигнатуры могут в качестве элементов содержать как объекты (term level), так и типы (type level) — объекты и морфизмы в топосе, в котором сигнатура моделируется. Через type-level элементы реализуется полиморфизм сигнатур. На самом деле запись type Set[T] = {def checkEquality(x: T, y: T): Boolean} это не более чем синтаксических сахар над
type Set = {
  type T
  def checkEquality(x: T, y: T): Boolean}
}

Бывают ведь и сигнатуры, оперирующие более чем двумя типами! Взять, например, векторные пространства — там одно множество это само векторное пространство, а другое — подлежащее поле:
type VectorSpace = {
  type V: AbelianGroup
  type F: Field
  def scalarMultiply(scalar: F, vector: V): V
  ...
}

Очень часто случается, что некая структура вообще говоря обобщает другую структуру совместимым образом, для этого удобно использовать наследование. Вот так:
type WellOrdered[T] extends Set[T] = {..}

type VectorSpace[V] extends AbelianGroup[V] = {
  type F: Field
  def scalarMultiply(scalar: F, vector: V): V
  ..
}

Иногда нам нужно чтобы аргумент имел тип, удовлетворяющий нескольким сигнатурам одновременно совместимым образом, для этого нужны операции объединения и подчинения сигнатур. Вот так:
radixSort[T: Ordered ∨ Weighted]
mathstuff[G: Group within Top](elementOfTopologicalGroup: G)


То, что на базе этого дела можно заниматься ООП — совершенно вторичный с точки зрения теоретика аспект. Первичный — то, что это позволяет корректно (сохраняя взаимные отношения) кодировать сигнатуры математических объектов.

Если оснастить Скалу полноценным propositions-as-types кодированием, то в рамки сигнатур будут, естетственно, входить не только операции, но и аксиомы. Так можно будет, например, закодировать стандартную теорию множеств в сигнатуре ZFC.Set и работать в рамках этой теории множеств. Для этого просто нужно ограничиться в работе типами, которые исходно отнаследованы от zfc.Set. Работать в таком мире, естественно, можно будет лишь на уровне доказательства теорем, а не на уровне вычислений, т.к. подавляющее большинство операций над множествами неконструктивно (либо они невычислимы, либо недетерминированы, начиная с взятия произвольного элемента множества размера 2).

Можно напротив работать в мире, где всё наследуется от типа agda.Set, тогда функция вида
last[T: Agda.Set](xs: List[T]): T

после erasure транслируется в
{T: Agda.Set} -> {xs: List T} -> T


Scala как она сейчас существует, работает в мире, где всё отнаследовано от jvm.Type. Начиная с 2.10 мы можем обходить erasure для определённых внутри языка типов при помощи type reflection, т.е. снабжая их привязкой [T: TypeTag].

Именно такая дистиллированная Scala является на мой взгляд самым удачным на сегодняшний день кандидатом на роль базового языка для proof assistant'ов будущего. Обратим внимание, что представленная здесь существенная для этого дела часть семантики Scala вообще не затрагивает того, что написано в фигурных скобках, где определяется тело методов/операций/доказательств, почти не касается используемого там внутри языка, не регламентирует type inference и type checking тел определений, кроме номинального, общего для всех логик. Базовые Scala примитивы — конструирование кортежей и извлечение их полей, интерпретируются в любых категориях с произведением (вообще говоря в любых Circuitries), если исключить неограниченную рекурсию.

Таким образом язык (исчисление) для написания тел определений включая type checking и type inference (а также нормализацию, унификацию и операционистскую семантику там где они возможны), можно вынести в модули-присадки, написанные на самой же Скале. Скалу как она есть сейчас или её чистый тотальный Agda-подобный вариант можно будет реализовать в качестве диалектов, заданных модулями-присадками. Мы получим уникальный язык, в рамках которого можно свободно смешивать всевозможные исчисления, и это, я считаю, прорыв.
Tags: scala
Subscribe

  • О программировании, из комментов у vit_r

    orleans: У ФП есть обьективные преимущества в плане исполнения на многопроцессорных системах и организации юнит тестов. Все то что можно…

  • Effect typing in short

    There are many different classes of functions out there. There are pure functions and there are functions with diverse side effects. Some can perform…

  • Towards Scala 3

    I'd like to share some ideas on features that might be included into next major Scala releases. Some of them might come in question already for Scala…

  • Post a new comment

    Error

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 28 comments

  • О программировании, из комментов у vit_r

    orleans: У ФП есть обьективные преимущества в плане исполнения на многопроцессорных системах и организации юнит тестов. Все то что можно…

  • Effect typing in short

    There are many different classes of functions out there. There are pure functions and there are functions with diverse side effects. Some can perform…

  • Towards Scala 3

    I'd like to share some ideas on features that might be included into next major Scala releases. Some of them might come in question already for Scala…