Существуют ли альтернативы типам для статического анализа?

Статическая типизация на языке программирования может быть полезна для обеспечения определенных гарантий во время компиляции, но являются ли типы единственным инструментом для этой работы? Существуют ли другие способы указания инвариантов?

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

Меня поинтересовало, есть ли какие-либо не декларативные способы для статического анализа ( по большей части типы являются декларативными ).

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

• Проверка модели - это метод анализа и проверки для параллельных систем, который позволяет вам доказать, что ваша программа хорошо себя ведет при всех возможных чередованиях потоков.

• Анализ потока данных собирает информацию о возможных значениях переменных, которые могут определить, являются ли некоторые вычисления избыточными или какая-то ошибка не учитывается.

• Абстрактная интерпретация консервативно моделирует эффекты программы, обычно таким образом, что анализ гарантированно прекращается - проверки типов могут быть реализованы аналогично абстрактным интерпретаторам.

• Логика разделения - это логика программы (используемая, например, в анализаторе Infer ), которую можно использовать для рассуждения о состояниях программы и выявления проблем, таких как разыменование нулевого указателя, недопустимые состояния и утечки ресурсов.

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

Оптимизирующие компиляторы выполняют много небольших анализов, чтобы создать промежуточные структуры данных для использования во время оптимизации, такие как SSA, оценки затрат на встраивание, информацию о парах команд и так далее.

Другой пример не декларативного статического анализа можно найти в проверке типов Hack , где обычные конструкции потока управления могут уточнить тип переменной:

$x = get_value();
if ($x !== null) {
    $x->method();    // Typechecks because $x is known to be non-null.
} else {
    $x->method();    // Does not typecheck.
}

И если говорить об «уточнении», то назад в мире систем типов уточненные типы (используемые в LiquidHaskell ) объединяют типы с предикатами, которые гарантированно сохраняются для экземпляров «уточненного» типа. И зависимые типы идут дальше, позволяя типам зависеть от значений. «Привет мир» зависимой типизации обычно является функцией конкатенации массива:

(++) : (a : Type) -> (m n : Nat) -> Vec a m -> Vec a n -> Vec a (m + n)

Здесь, ++принимает два операнда типа Vec a mи Vec a n, будучи векторы с типом элемента aи длиной mи , nсоответственно, которые являются натуральными числами ( Nat). Возвращает вектор с тем же типом элемента, длина которого равна m + n. И эта функция доказывает это ограничение абстрактно, не зная конкретных значений mи n, поэтому длины векторов могут быть динамическими.

Ответ @ JonPurdy лучше, но я хотел бы добавить еще несколько примеров:

Очевидные:

• проверка синтаксиса

• пыление

Не очевидно:

• Rust позволяет программисту указать, являются ли «привязки» изменчивыми , и применяет эти ограничения.

• Это как-то связано: некоторые языки позволяют запускать некоторый код во время компиляции, что означает, что многие вещи, которые в противном случае были бы ошибками во время выполнения, могут быть обнаружены во время компиляции. Некоторые примеры - это макросы и процедуры языка Nim, помеченные compileTimeпрагмой .

• Логическое программирование в основном строит программу, предоставляя утверждения.

Полустатическая печать:

• Поток Facebook позволяет гибрид между динамической и статической типизацией. Идея состоит в том, что даже динамический код неявно типизирован. Flow позволяет запускать сервер, который отслеживает ваш код во время его работы, чтобы обнаружить возможные ошибки типов, даже если вы не аннотируете свои функции.

Тип анализа много не значит.

Известно, что Agda имеет систему типов, полную по Тьюрингу, очень отличающуюся (и гораздо более сложную для вычислений), чем языки ML (например, Ocaml ).