Категории типов. Часть 7. Исчисление концов

[kovserg]

Можете на простых примерах показать нафига где это нужно. Или хотя бы где без этого не обойтись.

[Underskyer1]

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

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

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

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

В дальнейшем планирую продемонстрировать, как реализация расширений Кана в виде (ко)концов приводит к конкретным реализациям монад продолжений, свободных монад и т.п. То есть будет показан метод вывода монад для произвольны функторов, а также техники сборки композитных монад (в том числе классы типов Traversablе и Distributable).

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

[kovserg]

С помощью этой теории можно, например, доказать что модификатор const в системе типов не только не нужен, но и вреден?

[Underskyer1]

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

Алгоритм описывает способ решения класса задач (разных начальных условий). Значения переменных алгоритма меняются от задаче к задаче, но не изменяются в рамках одной задачи! Такая устойчивость математических алгоритмов позволяет сравнивать их друг с другом, оптимизировать и выявлять ошибки до их исполнения.

Функциональное программирование старается по максимуму использовать эту идею - неизменяемые типы данных и переменные переносят огромную долю тестирования на этап компиляции. В Scala, например, по умолчанию все идентификаторы константные, а потенциальную опасность несёт противоположный модификатор var. В более распространённой императивной парадигме программистам по умолчанию даётся опасная возможность менять значения в памяти (потому что на низком уровне это даётся почти бесплатно!), но "по желанию" всегда можно "усложнить" код модификатором const. Как будто разработчики языка наоборот хотят отбить желание сделать код более предсказуемым...

Так что проблема const - это не столько про систему типов, сколько про те языки, что следуют популярной низкоуровневой парадигме императивного управления компьютером, в том числе и его памятью. Сама эта парадигма мешает обеспечивать достойное качество алгоритмов.

[summerwind]

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

[Underskyer1]

Верно.

В сложных задачах легко запутаться. Упростить решение помогает декомпозиция по базовым абстракциям. Причём, чем фундаментальнее абстракции, тем меньше их требуется в строительстве программировании.