Информационная, Техническая информация

Системы типов в языках программирования

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

Для проверки корректности отдельных частей программы могут применяться статический анализ кода до его исполнения и проведение тестирования поведения программы на реальных запусках.

При статическом анализе используется математический аппарат из теории вычислительных систем — от простой теории формальных языков и трансляции, до теории типов и логики Хоара. Самый часто используемый на практике формализм, которым пользуются статические анализаторы, компиляторы, плагины автодополнения к IDE, это системы типов в языках программирования, формальным обоснованием которых является теория типов.

Какими бы ни были языки программирования, в них используется система типов. Тип выражения программы — это высказывание, накладывающее определённое ограничение на значение этого выражения. Системы типов различного уровня подробно рассмотрены в книге Пирса «Типы в языках программирования». В качестве основы определения семантики языка программирования берётся формализм из теории вычислимости, чаще всего лямбда-исчисление. Затем, добавляя в язык лямбда-исчисления расширения и типы, можно получать системы типов различного уровня сложности. Системы типов в порядке раста мощности можно выделить следующие: простые типы, подтипы, рекурсивные типы, система типов с полиморфизмом (System F), системы типов высшего порядка с ограничениями, зависимые типы и исчисление конструкций.

Проверка согласования типов в программе происходит с использованием алгоритма вывода типов, который очень похож на алгоритмы в системах доказательства теорем. Отсутствие ошибок согласования типов гарантирует, что в программе нет определённого рода ошибок. Чем строже система типов, тем тщательнее проверяется программа на ошибки. Система типов считается нестрогой, если в языке есть неявные преобразования типов или операции приведения типов.

Простая система типов состоит из типов, соответствующих непересекающимся множествам значений. Это примитивные типы (числовые, логические, строковые, перечисления), составные типы (структуры, кортежи), а также, функциональные типы (типы функции или «стрелочные» типы). Простую типизацию имеют только самые простые языки, чаще всего низкоуровневые.

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

Рекурсивные типы служат для представления рекурсивных структур данных, таких как связные списки, деревья и графы.

Система типов, где присутствуют функции над типами, обладает ещё большей гибкостью и полиморфизмом. Это лямбда-исчисление второго порядка, называемое System F. Некоторые элементы этой системы типов представлены в различных языках в виде generics (C#, Java), templates (C++, D, Rust).

Системы типов высших порядков сопоставимы по сложности с логикой Хорара. Зависимые типы присутствуют в таких языках как TypeScript, шаблоны C++, Scala, Kotlin.

В языках с динамической типизацией на самом деле тоже можно каждому выражению приписывать определённые типы. Можно даже поверх таких скриптовых языков как Python, JavaScript, Ruby, Perl, сделать системы типов большой мощности для применения при статическом анализе. Интерпретаторы этих языков пользуются меньшим количеством информации о типах. Но отличие динамической типизации от статической только в том, что при динамической типизации типы не проверяются на этапе компиляции (которой может не быть).

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

Знание систем типов позволяет лучше понимать дизайн языков программирования и использовать эффективно компилятор, статические анализаторы и средства IDE, а также, придерживаться определённых практик написания кода, при которых будет меньше вероятности допустить ошибку или перерабатывать много кода после внесения изменений в требования задачи.

Нет комментариев.