deep-econom (deep_econom) wrote,
deep-econom
deep_econom

Category:
----
Сергей Бобровский
Кубическая теория типов для малышей

Вычислительная теория типов (Computational Type Theory, CTT) связывает конструктивную математику Мартина-Лёфа и программирование. CTT -- это теория конструктивной математики, основанная на вычислениях.

Конструктивная математика -- это математика, в которой мы манипулируем объектами конструктивно :) Нас интересуют не абстрактные характеристики со множеством деталей, а конкретные, прикладные в некотором смысле. Например, многие типы данных описываются через теорию множеств весьма сложно, а в конструктивном смысле нам достаточно иметь алгоритм (по Тьюрингу например), который бы формально, пусть и ограниченно, описывал некоторый тип. Кроме того, учитывается, что объекты не существуют вечно, а появляются и исчезают, и т. д. В конструктивной математике мы делаем большие допуски, большие послабления, жертвуя математической строгостью в пользу эффективной вычислимости. Во многих прикладных задачах нас вполне удовлетворит утиная типизация/абстракция отождествления (если что-то выглядит как утка и ходит как утка, то это скорее всего и есть утка), а те объекты, которые явно не похожи на утку, мы просто исключаем из рассмотрения.

Интуиционистская теория типов, например, построена на конструктивной математике. В Корнельском университете ещё с 1980-х годов разрабатывается система автоматических доказательств NuPRL, с её помощью удалось удачно формализовать ряд конструктивных теорий. Крутость NuPRL в том, что она исходит не из формальной системы типов, а из концепции программы, типы в которой -- характеристики её поведения. В результате удаётся сформировать очень богатую систему типов, охватывающую и типы в классическом смысле, и типы, завязанные на вычисления. И вот когда типы насыщаются семантикой, система автоматических доказательств становится очень прагматичной, ориентированной на реализацию, а не на абстрактные концепции.

Основной метод в CTT называется "прояснение смысла", и хоть и связан с формальной теорией типов через концепцию логических отношений, но отказывается от метаматематической абстрактной механики и нацелен именно на семантику типов. Например, в формальных теориях типов переменные -- это скорее неопределенные, неизвестные из алгебры, а в CTT переменные -- это именно значения типа. В CTT акцент делается на исполнении конечных программ, а не на бесконечных вычислениях, тут же и утиная типизация, и т. п.

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

CTT имплементируется теорией доказательств, которая сама по себе достаточно надёжна, чтобы обеспечить удобное применение метода прояснения смысла. При этом теория доказательств не определяет, а описывает CTT, и в некотором смысле является инструментом доступа к истине. Прикладная теория доказательств не нуждается в соответствии (и не должна соответствовать) какой-либо системе формальной логики, и не должна удовлетворять мета-теоретическим свойствам, которые не связаны с семантикой. Главное, она должна быть практичной. Например, NuPRL базируется на теории доказательств, называемой уточняющей логикой, и поддерживает интерактивное формирование, вывод доказательств и извлечение из доказательств программ.

Сегодня самый мировой топчик в развитии CTT -- это кубики, кубическая теория типов, Cubical Computational Type Theory (CCTT). Она расширяет CTT отождествлениями, или путями всех конечных измерений. Самые простые элементы типов имеют измерение 0. Элементы измерения n+1 -- это пути, которые связывают два элемента измерения n и свидетельствуют о взаимозаменяемости этих элементов во всех контекстах. Математически, тут связи с комбинаторной топологией и теорией категорий (точнее, теорией высших категорий [Лейнстер 2002] -- морфизмы морфизмов и вот это вот всё). С точки зрения программиста, такая структура высоких измерений по сути предлагает нам универсальный механизм симметричного(?) "приведения", преобразования типов друг в друга, который только в такой теории называется на casting, а coercion.

В сердце же всего этого -- гениальная аксиома унивалентности Воеводского:

эквивалентные (изоморфные, очень грубо) типы идентичны (взаимозаменяемы).
Как организовать такую структуру? Тут и было решено использовать кубики: типы и термы распределяются по слоям (измерениям), нулевое измерение соответствует стандартной CTT, и объект измерения n+1 будет n+1 - мерным кубом, который можно представить как связи между n-мерными кубиками -- n различными способами, соответствующими парам противоположных граней в каждом измерении. Например, трёхмерный кубик состоит из трёх пар противоположных граней -- двухмерных кубиков (квадратов). Применительно к программированию, кубик -- это программа, вычисление которой "чувствительно" к биндингу переменных доступных измерений, которые, двигаясь к 0 или 1 по своему измерению, индуцируют вычисление конечных точек линий, параметризованных этими переменными.

Наверное, ключевое в кубиках -- это сами линии типов (по которым бегают экземпляры типов в процессе тайпкастинга) и их конечные точки, которые подразумевают взаимозаменяемость типов подчас весьма сложным вычислительным образом. Далее, удалось формализовать понятие хорошо типизированных вычислений -- это те, которые когерентны в отношении порядка измерений (верхняя точка слева должна совпадать с левой точкой вверху). Наконец, линий типов должно быть достаточно, чтобы можно было строить нужные пути через их конкатенацию, ну и должны присутствовать линии более высоких измерений, чтобы обеспечить ассоциативность такой конкатенации. Тут ещё можно вспомнить условие Кана из теорката, переведённое на язык CTT -- результат должен вычисляться из спецификации задачи унифицированным способом.

Активно занимается этим Robert Harper из Карнеги-Меллона, входящий в дюжину святых Computer Science (развивает кубики, формализует ML, пишет самые крутые курсы CMU). Надеюсь, что какие-то кусочки его свежих лекций, пока их ещё можно достать в даркнете :) постепенно получится адаптировать к рациональному просветлению. Ну и попутно, попрактиковаться в тысячекратной компактности кода.

https://vk.com/@lambda_brain-cubical-computational-type-theory
---
Subscribe

  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic
  • 0 comments