Статическая и динамическая типизация

Статическая типизация проверяет типы до запуска программы, тогда как динамическая типизация проверяет их во время выполнения; постепенная типизация стремится объединить эти два подхода в рамках одного языка.

Definition

Статическая типизация проверяет ограничения типов на этапе компиляции, так что программы с корректными типами принимаются до выполнения; динамическая типизация откладывает проверки типов до времени выполнения, вызывая ошибки, когда операции применяются к значениям неподходящего типа.

Scope

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

Core questions

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

Key theories

Постепенная типизация

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

Корректность статической типизации

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

Clinical relevance

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

History

Ранние языки разделились на статически типизированные (Algol, Pascal, ML) и динамически типизированные (Lisp, Smalltalk). По мере роста популярности динамических языков для повышения производительности исследователи стремились примирить эти подходы; постепенная типизация Зика и Тахи 2006 года и одновременные работы по опциональным типам привели к широко используемым системам постепенной типизации, построенным поверх динамических языков.

Debates

Стоимость и корректность постепенной типизации

Исследователи обсуждают, может ли корректная постепенная типизация избежать непомерных затрат на проверку во время выполнения на типизированных/нетипизированных границах и является ли некорректная «опциональная» типизация лучшим практическим компромиссом.

Key figures

• Benjamin Pierce
• Jeremy Siek
• Walid Taha
• Matthias Felleisen

Seminal works

• pierce2002
• siek2006
• wright1994

Frequently asked questions

Всегда ли статическая типизация лучше динамической?

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

Что такое постепенная типизация?

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