Зависимые типы

Вот есть какая-то функция. Давайте, для примера, возьмём деление. Что мы знаем о входных значениях?

Оба аргумента -- числа.
Второй аргумент -- не ноль. На ноль делить нельзя.

То есть, у нашей функции есть условия для входных параметров. Как эти условия задать в программе?

Типизация

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

С условием "число не равно нулю" сложнее. Причём такие ограничения на допустимые значения внутри одного типа встречаются довольно часто. Ещё один пример -- взятие индекса от списка. А вдруг список короче? На каждый размер списка отдельными типами не запастись, да и работать с таким будет сложно. К тому же, необходимая длина списка зависит от конкретного значения индекса, которое мы не знаем.

Исключения

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

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

Специальное значение

Можно вообще не рассматривать такие ситуации как что-то особенное. Делим на ноль? Возвращаем Infinity. Взяли несуществующи индекс? Вернули Null. Проблемы:

Такие случаи всё равно надо явно обрабатывать, точно так же, как и исключения. То-то ваши пользователи, не опубликовавшие ни одного поста, обрадуются, когда их средний рейтинг будет Infinity.
А вдруг первый аргумент деления был Infinity? А вдруг по нужному индексу в списке лежал Null? В итоге, такие особые ситуации становится невозможно отличить от случаев, когда всё идёт как и задумано.

Оборачиваем значения

Можно обернуть возвращаемое значение в специальный тип. Это гибрид исключений и специальных значений. А поведение для случаев с ошибкой мы пропишем явно: нужно ли нам сразу пробросить ошибку выше, или же сначала закончить переводить зарплаты остальным. К тому же, это хорошо ложится на типизацию. В функциональных языках это монада Maybe. В Python её потрогать можно с помощью библиотеки returns.

Контрактное программирование

Предыдущий подход удобен, когда мы заранее не можем быть уверены в корректности приходящих извне данных, и нам приходится проверять это уде внутри функции. Но давайте вспомним первый пример с типизацией: мы объявляли, что наша функция принимает только числа, и потребовали соблюдение этого условия от внешнего кода, и внутри функции мы можем избежать всяческих проверок. Точно так же мы можем сделать контракт, который будет говорить внешнему коду о том, что на 0 делить нельзя. Это называется Контрактное Программирование. Контракт может накладывать ограничение на входные параметры, результат функции и внутреннее состояние атрибутов класса. Можно проверять это всё в рантайме, как это делается в deal, но хочется узнать о проблемах ещё на этапе компиляции. Итак, что мы можем проверить статически:

Некоторые ограничения, которые известны из типа. Например, контракт orderable, который требует, чтобы передаваемые объекты могли быть сравниваемы друг с другом (это нужно для функций сортировки, например). Обычно такое реализуется с помощью интерфейсов.
Передаваемые константы. Если мы видим, что вот тут в функцию передается число 42, то, очевидно, контракт != 0 соблюдён.

И всё?

Зависимые типы

Нет, не всё. Тут на сцене появляются зависимые типы. Зависимые типы -- это когда тип данных зависит от конкретных значений. Примеры всё те же: при делении второе число не может равняться 0, а при взятии индекса индекс не может быть больше длины вектора. И язык с зависимыми типами не даст скомпилировать программу, пока все неявные моменты не будут явно покрыты:

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

Доказательство -- сложно, но это даёт офигенную надёжность кода. Тесты проверяют только частные случаи и предназначены показать наличие ошибок, тогда как строгое доказательство показывает их отсутствие. Тесты тоже нужны, конечно, но достаточно протестировать только доказательную базу.

Первое практическое применение в программировании -- язык Coq, созданный для доказательства теорем. В нём вообще всё строится вокруг строгих доказательств, пожтому зависимые типы для его задач -- как раз то, что нужно. Но можно ли это использовать в языках общего назначения?

Idris

Idris -- чистый функциональный язык общего назначения со строгой статической типизацией с зависимыми типами.

Плюсы: БЕЗОПАСНОСТЬ.

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

Особенности:

Синтаксис вдохновлён Haskell, конечно же.
Ещё один источник вдохновения -- Agda. Оттуда пришли зависимые типы, механизм доказательства теорем, вот это всё.
Termination analysis -- компилятор проверит, что каждая функция покрывает и корректно обрабатывает ВСЕ возможные варианты входных значений.
Proof assistant -- можно прям из IDE интерактивно взаимодействовать с магической тукой, которая может разворачивать доказательства, искать частные случаи, выносить леммы и прочее. Математическая индукция, всё такое.

В общем, даже не знаю, что добавить. Это точно не тот язык, на котором через 10 лет будут написаны все web-сайты. Так же это не тот язык, на котором хочется написать свой бложик. Но пока что это тот язык, коорый в наиболее дружелюбной форме реализует зависимые типы и доказательства. Пока что не очень дружелюбно полуается, но всё же. Возможно, эти идеи пройдут путь упрощения и адаптации, и в какой-нибудь там версии Kotlin или Scala (ха-ха, шучу, Scala уже) мы увидим упрощенный theorem prover. Ну а пока что если хочется почувствовать себя профессором кафедры математики (или добить свою самооценку), Idris отличный вариант.

Ссылки по теме: