В теории типов , теории в рамках математической логики , нижний тип - это тип, не имеющий значений. Он также называется нулевым или пустым типом и иногда обозначается символом закрепки вверх (⊥).
Функция с возвращаемым типом bottom не может возвращать никакого значения, даже если тип блока нулевого размера . Следовательно, функция, возвращаемым типом которой является нижний тип, не может вернуться. В корреспонденции Карри – Ховарда нижний тип соответствует ложности.
Приложения для информатики
В системах подтипов нижний тип является подтипом всех типов. [1] (Однако обратное неверно - подтип всех типов не обязательно является нижним типом.) Он используется для представления возвращаемого типа функции, которая не возвращает значение: например, тот, который зацикливается навсегда , сигнализирует об исключении или завершает работу.
Поскольку нижний тип используется для обозначения отсутствия нормального возврата, он обычно не имеет значений. Он контрастирует с верхним типом , который охватывает все возможные значения в системе, и типом единицы , который имеет ровно одно значение.
Нижний тип часто используется для следующих целей:
- Чтобы сигнализировать, что функция или вычисление расходятся ; другими словами, не возвращает результат вызывающей стороне. (Это не обязательно означает, что программа не может завершиться; подпрограмма может завершиться без возврата к вызывающей стороне или выйти с помощью других средств, таких как продолжение .)
- В сочетании с интерпретацией дна по соответствию Карри – Ховарда как «ложности» это дает вычислительную интерпретацию неконструктивной логики в терминах операторов потока управления . [2]
- Как указание на ошибку; это использование в основном встречается в теоретических языках, где различение ошибок не важно. Рабочие языки программирования обычно используют другие методы, такие как типы опций (включая тегированные указатели ) или обработку исключений .
В ограниченной квантификации с Bottom , [1] Пирс говорит , что «Bot» имеет множество применений:
- В языке с исключениями естественным типом конструкции повышения является raise ∈ exception -> Bot , и аналогично для других управляющих структур. Интуитивно понятно, что Бот - это тот тип вычислений, который не дает ответа.
- Бот полезен при вводе «листовых узлов» полиморфных структур данных. Например, List (Bot) - хороший тип для nil.
- Bot естественный тип для « указателя нулевой стоимости» (указатель , который не указывает на какой - либо объект) языков , таких как Java: в Java , то тип нуль является универсальным подтипом ссылочных типов.
null
- единственное значение нулевого типа; и его можно привести к любому ссылочному типу. [3] Однако нулевой тип не удовлетворяет всем свойствам нижнего типа, как описано выше, потому что нижние типы не могут иметь никаких возможных значений, а нулевой тип имеет значениеnull
. - Система типов, включающая как Top, так и Bot, кажется естественной целью для вывода типа , позволяя фиксировать ограничения на пропущенный параметр типа парой границ: мы пишем S <: X <: T, чтобы обозначать «значение X должен находиться где-то между S и T. " В такой схеме полностью неограниченный параметр ограничен снизу Bot, а сверху - Top.
В языках программирования
Наиболее часто используемые языки не имеют возможности явно обозначить пустой тип. Есть несколько заметных исключений.
Начиная с Haskell2010, Haskell поддерживает пустые типы данных. Таким образом, это позволяет определение data Empty
(без конструкторов). Тип Empty
не совсем пустой, так как он содержит программы без завершения и undefined
константу. undefined
Константа часто используется , когда вы хотите что - то , чтобы иметь пустой тип, потому что undefined
матчи любого типа (так это своего рода «подтипа» всех типов), и попытка оценить undefined
вызовет программу для прерывания, поэтому он никогда не возвращает ответ .
В Common Lisp символ NIL
, помимо прочего, является также именем типа, не имеющего значений. Это дополнение T
к высшему типу. Именованный тип NIL
иногда путают с названным типом NULL
, который имеет одно значение, а именно сам символ NIL
.
В Scala нижний тип обозначается как Nothing
. Помимо его использования для функций, которые просто генерируют исключения или иным образом не возвращаются нормально, он также используется для ковариантных параметризованных типов . Например, Scala List является конструктором ковариантного типа, поэтому он List[Nothing]
является подтипом List[A]
для всех типов A. Итак, Scala Nil
, объект для обозначения конца списка любого типа, принадлежит к этому типу List[Nothing]
.
В Rust нижний тип называется никогда-типом и обозначается !
. Он присутствует в сигнатуре типа функций, которые гарантированно никогда не вернутся, например, при вызове panic!()
или бесконечном цикле. Это также тип определенных ключевых слов потока управления, таких как break
и return
, которые не производят значения, но, тем не менее, могут использоваться как выражения. [4]
На Цейлоне нижний тип - Nothing
. [5] Он сравним с Nothing
Scala и представляет собой пересечение всех других типов, а также пустой набор.
В Юлии нижний тип есть Union{}
. [6]
В TypeScript нижний тип - never
. [7] [8]
В JavaScript с аннотациями Closure Compiler нижним типом является !Null
(буквально, ненулевой член типа Null
модуля ).
В Python нижний тип - typing.NoReturn
. [9]
Смотрите также
Рекомендации
- ^ a b Пирс, Бенджамин С. (1997). «Ограниченная количественная оценка с дном». CiteSeerX 10.1.1.17.9230 . Цитировать журнал требует
|journal=
( помощь ) - ^ Гриффин, Тимоти Г. (1990). «Понятие управления формулами как типами». Конф. Рекордный 17-й ежегодный симпозиум ACM. о принципах Языки программирования, POPL '90, Сан - Франциско, штат Калифорния, США, 17-19 Jan 1990 . С. 47–57.
- ^ «Раздел 4.1: Виды типов и значений» . Спецификация языка Java (3-е изд.).
- ^ «Первобытный тип никогда» . Документация стандартной библиотеки Rust . Проверено 24 сентября 2020 .
- ^ «Глава 3. Система типов - 3.2.5. Тип нижний» . Цейлонский язык . Red Hat, Inc . Проверено 19 февраля 2017 .
- ^ Основы - Язык Джулии
- ^ The never type, примечания к выпуску TypeScript 2.0 , Microsoft, 2016-10-06 , получено 2019-11-01
- ^ Never type, примечания к выпуску TypeScript 2.0, исходный код , Microsoft, 2016-10-06 , получено 2019-11-01
- ^ typing.NoReturn, typing - Supprot для подсказок типов, документация Python, Python Software Foundation , получено 25 февраля 2020 г.
- ^ Ничего , получено 15 мая 2020 г.
- ^ Никогда , получено 25.03.2021
дальнейшее чтение
- Пирс, Бенджамин С. (2002). Типы и языки программирования . MIT Press . ISBN 0-262-16209-1.