Alexander Kuklev (akuklev) wrote,
Alexander Kuklev
akuklev

Categories:

О данных, коданных, HoTT и DOT

Данные задаются через конструкторы (т.е. грубо говоря генеративную грамматику, определяющую какие выражения мы считаем представителями того или иного типа данных). У нас есть грамматика nat ::= zero | succ nat, она задаёт нам натуральные числа. Если есть грамматика языка программирования, она задаёт нам тип _данных_ "алгоритм, выраженный на этом языке".

Коданные задаются через деконструкторы (т.е. представитель какого-то типа коданных это blackbox, у которого задан интерфейс, интерфейс (если угодно, сигнатура или тайпкласс) это и есть деконструкторы). Лучший пример коданных -- потоки Stream[T] (т.е. потенциально бесконечные списки). Они задаются деконструктором pick, который из чёрного ящика типа Stream[T] берёт первый элемент и возвращает первый элемент и остаток потока (тоже чёрный ящик)
pick: Stream[T] => (head: T, tail: Stream[T] | EndOfStream)

Функция из натуральных чисел в натуральные числа (любая, не обязательно вычислимая) это тоже элемент коданных, она задаётся деконструктором apply: (Function, Nat) => Nat, который применяет функцию (чёрный ящик) к числу.

Между данными и коданными имеется асимметрия: тип данных может быть подтипом коданных, но никогда наоборот. Более того, исключая тривиальные случаи, типы данных не исчерпывают типы коданных.
Так список является подтипом потока. Вычислимые функции (т.е. заданные алгоритмом) являются подтипом произвольных, но не исчерпывают их, и так далее.

Для представителей данных существует естественное определение равенства: definitional equality (термы равны тогда и только тогда, когда одинаковы, т.е. одинкого построены), для представителей коданных тоже существует естественное определение равенства: observational equality, т.е. объекты равны тогда и только тогда, когда различий между ними невозможно установить, используя методы, задекларированные в их интерфейсах. Т.е. сколь угодно длинные равные конечные цепочки применения к ним деконструкторов всегда приводят к одному и тому же результату.

В "хороших" теориях типов (OTT и HoTT) типом вычислимых функций называют не тип определяющих их выражений на языке программирования, а его-фактор где вычислимые считаются равными если они равны как коданные (т.е. выдают одинаковые outputs на одинаковых inputs). Обёртывание типа данных в более общий тип коданных с последующим "забыванием" деталей имплементации (т.е. отказ от конструктивного равенства в пользу наблюдаемого) это в точности то, что в ООП называется инкапсуляцией.

HoTT выглядит очень многообещающим вариантом универсальной теории типов данных, однако чтобы там было что-то по части коданных я не слышал, по крайней мере никакого "комфорта" по работе с сигнатурами коданных HoTT заведомо не предоставляет, представления инкапсуляции (т.е. неизбежно monotonicity breaking) там заведомо нет. HoTT это transparent closed system, а для коданных нужна open system with incapsulation.

Зато вот DOT (разработка Scala Team) тянет на роль очень универсальной теории коданных, там фактически все о тайпклассах и их инстансах, вместе с инкапсуляцией, иерархичностью, миксингом, валентностью, номинальным refl-равенством (точно как надо! нужно номинальное равенство по умолчанию и доказуемое равенство через изоморфизм, структурого равенства не нужно, оно является частным случаем равенства через изоморфизм). Только разработчики DOT пытаются довольно неуклюже применять свою систему коданных в качестве универсальной, не смотря на то что в ней нельзя определить ни одного типа именно "данных", т.е. sealed-типа, так чтобы можно было использовать pattern matching.
Можно попробовать ввести алгебраические типы данных в DOT, введя ключевое слово для построения минимальных стационарных точек сигнатур, навроде
object List[T] = minimal {
  List: Type
  Empty: List
  Cons: (head: T, tail: List) => List
},

однако авторы настойчиво идут на поводу у предрассудков родом из С++ и Джавы и пытаются определять конструкторы Nil и Cons как типы-наследники List, а не как конструкторы, и засунуть методы-хелперы не в companion-object List, а в саму сигнатуру типа List.

Рано или поздно нужен будет синтез теорий типов данных и типов косчётных коданных, вот тогда заживём.
Subscribe

  • (no subject)

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

  • Прогресс

    Десять дней назад, вторая ступень SpaceX'овского корабля Starship своим ходом слетала своим ходом на десять километров вверх, и усмепшно приземлилась…

  • О водосбережении

    Как известно, питьевая вода во многих странах дефицитный ресурс. И даже в дождливой Германии летом иногда случаются засухи, в результате которых она…

  • 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.
  • 17 comments

  • (no subject)

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

  • Прогресс

    Десять дней назад, вторая ступень SpaceX'овского корабля Starship своим ходом слетала своим ходом на десять километров вверх, и усмепшно приземлилась…

  • О водосбережении

    Как известно, питьевая вода во многих странах дефицитный ресурс. И даже в дождливой Германии летом иногда случаются засухи, в результате которых она…