Нижний тип
В теории типов , теории в рамках математической логики , нижний тип системы типов — это тип, который является подтипом всех других типов. [1]
Там, где такой тип существует, его часто обозначают символом закрепки (⊥).
Связь с пустым типом
[ редактировать ]Когда нижний тип необитаемый , функция, возвращаемый тип которой — нижний, не может возвращать какое-либо значение, даже единственное значение типа единицы .Поэтому в таком языке нижний тип может быть известен как нулевой , никогда или пустой тип , который в соответствии Карри-Ховарда соответствует ложности.
Однако когда нижний тип обитаем, он отличается от пустого типа.
Приложения в области информатики
[ редактировать ]В системах подтипирования нижний тип является подтипом всех типов. [1] Он двойственен верхнему типу , который охватывает все возможные значения в системе.
Если система типов правильная , то нижний тип необитаем, а термин нижнего типа представляет собой логическое противоречие. В таких системах обычно не проводится различие между нижним типом и пустым типом , и эти термины могут использоваться как взаимозаменяемые.
Если нижний тип является обитаемым, его термины обычно соответствуют условиям ошибки, таким как неопределенное поведение, бесконечная рекурсия или неисправимые ошибки.
В ограниченной количественной оценке с нижней границей [1] Пирс говорит, что «Бот» имеет множество применений:
- В языке с исключениями естественным типом конструкции подъема является raise ∈Exception -> Bot , и аналогично для других управляющих структур. Интуитивно понятно, что бот — это тип вычислений, которые не возвращают ответ.
- Бот полезен при наборе «листовых узлов» полиморфных структур данных. Например, List(Bot) — хороший тип для nil.
- Bot — это естественный тип для значения « нулевого указателя » (указатель, который не указывает ни на какой объект) в таких языках, как Java: в Java нулевой тип является универсальным подтипом ссылочных типов .
null— единственное значение нулевого типа; и его можно привести к любому ссылочному типу. [2] Однако нулевой тип не является нижним типом, как описано выше, и не является подтипомintи другие примитивные типы. - Система типов, включающая как Top, так и Bot, кажется естественной целью для вывода типа , позволяя фиксировать ограничения на пропущенный параметр типа с помощью пары границ: мы пишем S<:X<:T, чтобы означать «значение X должен лежать где-то между S и T». В такой схеме полностью неограниченный параметр ограничен снизу Bot и сверху Top.
В языках программирования
[ редактировать ]В наиболее часто используемых языках нет способа обозначить нижний тип. Есть несколько заметных исключений.
В Haskell нижний тип называется Void. [3]
В Common Lisp тип NIL, не содержит значений и является подтипом каждого типа. [4] Тип с именем NIL иногда путают с типом с именем NULL, который имеет одно значение, а именно символ NIL сам.
В Scala нижний тип обозначается как Nothing. Помимо использования для функций, которые просто генерируют исключения или иным образом не возвращаются нормально, он также используется для ковариантных параметризованных типов . Например, список Scala является конструктором ковариантного типа, поэтому List[Nothing] является подтипом List[A] для всех типов A. Итак, Scala Nil, объект для обозначения конца списка любого типа принадлежит типу List[Nothing].
В Rust нижний тип называется типом Never и обозначается !. Он присутствует в сигнатуре типа функций, которые гарантированно никогда не возвращаются, например, путем вызова panic!() или зацикливаться навсегда. Это также тип некоторых ключевых слов потока управления, таких как break и return, которые не создают значения, но, тем не менее, могут использоваться в качестве выражений. [5]
На Цейлоне нижний тип — Nothing. [6] Это сравнимо с Nothing в Scala и представляет собой пересечение всех других типов, а также пустое множество.
В Julia нижний тип — Union{}. [7]
В TypeScript нижний тип — never. [8] [9]
В JavaScript с аннотациями Closure Compiler нижний тип — !Null (буквально, ненулевой член Null тип агрегата ).
В PHP нижний тип — never.
В дополнительных аннотациях статического типа Python общий нижний тип — typing.Never (введено в версии 3.11), [10] пока typing.NoReturn (представленный в версии 3.5) может использоваться в качестве возвращаемого типа невозвращающих функций (и дублироваться как общий нижний тип до введения Never). [11]
В Котлине нижний тип — Nothing. [12]
В Dart , начиная с версии 2.12 с обновлением безопасности Sound Null , Never тип был представлен как нижний тип. До этого нижний тип был Null. [14] [15]
См. также
[ редактировать ]Ссылки
[ редактировать ]- ↑ Перейти обратно: Перейти обратно: а б с Пирс, Бенджамин К. (1997). «Ограниченная количественная оценка с низом» . Технический отчет CSCI Университета Индианы (492): 1.
- ^ «Раздел 4.1: Виды типов и значений» . Спецификация языка Java (3-е изд.).
- ^ «Данные.Пустота» . Хакадж . Проверено 20 сентября 2023 г.
- ^ «Тип НИЛ» . Common Lisp HyperSpec . Проверено 25 октября 2022 г.
- ^ «Примитивный тип никогда» . Документация стандартной библиотеки Rust . Проверено 24 сентября 2020 г.
- ^ «Глава 3. Типовая система — 3.2.5. Нижний тип» . Цейлонский язык . Красная шляпа, Inc. Проверено 19 февраля 2017 г.
- ^ «Основы — язык Julia» , Документация по языку программирования Julia , получено 13 августа 2021 г.
- ^ Тип «никогда», Примечания к выпуску TypeScript 2.0 , Microsoft, 06 октября 2016 г. , получено 1 ноября 2019 г.
- ^ Тип Never, Примечания к выпуску TypeScript 2.0, исходный код , Microsoft, 06 октября 2016 г. , получено 1 ноября 2019 г.
- ^ «Ввод текста — Поддержка подсказок типов — Документация Python 3.12.0a0» . docs.python.org . Проверено 2 марта 2024 г.
- ^ typing.NoReturn, typing — Поддержка подсказок по типам, документация Python , Python Software Foundation , получено 2 марта 2024 г.
- ^ Ничего , получено 15 мая 2020 г.
- ^ «Типы — язык программирования D» . dlang.org . Проверено 20 октября 2022 г.
- ^ Понимание нулевой безопасности — верх и низ , получено 13 апреля 2022 г.
- ^ Понимание нулевой безопасности — никогда для недостижимого кода , получено 13 апреля 2022 г.