Есть ли какой-либо вариант использования для нижнего типа в качестве типа параметра функции?

Если функция имеет тип возврата of ( нижний тип ), это означает, что она никогда не вернется. Это может, например, выйти или бросить, обе довольно обычные ситуации.

Предположительно, если функция имеет параметр типа ⊥, она никогда не сможет (безопасно) быть вызвана. Есть ли когда-нибудь причины для определения такой функции?

Одним из определяющих свойств или пустого типа является то , что существует функция для каждого типа . На самом деле, существует уникальная такая функция. Поэтому вполне разумно, чтобы эта функция предоставлялась как часть стандартной библиотеки. Часто это называется что-то вроде . (В системах с подтипами это может быть выполнено просто при наличии как подтипа каждого типа. Тогда подразумевается неявное преобразование . Другой связанный подход заключается в определении как который может быть просто создан для любой тип.)$\bot$$\bot \to A$$A$⊥ ⊥ ∀ α . αabsurd$\bot$absurd $\bot$$\forall \alpha.\alpha$

Вы определенно хотите иметь такую ​​функцию или эквивалент, потому что это то, что позволяет вам использовать функции, которые производят . Например, предположим, что я дал тип сумму . Я делаю анализ случая и в случае я собираюсь исключение, используя . В случае, я буду использовать . В целом, я хочу значение типа , так что мне нужно сделать что - то , чтобы превратить в . Это то, что позволило бы мне сделать.$\bot$$E+A$$E$$\mathtt{throw}:E\to\bot$$A$$f:A\to B$$B$$\bot$$B$absurd

Тем не менее, есть не много причин , чтобы определить свои собственные функции . По определению они обязательно будут экземплярами . Тем не менее, вы можете сделать это, если это не предусмотрено стандартной библиотекой, или вам нужна специализированная версия типа, чтобы помочь проверке / выводу типа. Вы можете, однако, легко производить функции , которые в конечном итоге инстанцирован к типу как .$\bot\to A$⊥ → Aabsurdabsurd$\bot\to A$

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

Чтобы добавить к тому, что было сказано о функции, у absurd: ⊥ -> aменя есть конкретный пример того, где эта функция действительно полезна.

Рассмотрим тип данных Haskell, Free f aкоторый представляет общую древовидную структуру с fузлами -образной формы и листьями, содержащими as:

data Free f a = Op (f (Free f a)) | Var a

Эти деревья можно сложить с помощью следующей функции:

fold :: Functor f => (a -> b) -> (f b -> b) -> Free f a -> b
fold gen alg (Var x) = gen x
fold gen alg (Op x) = alg (fmap (fold gen alg) x)

Вкратце, эта операция размещается algв узлах и genна листьях.

Теперь к сути: все рекурсивные структуры данных могут быть представлены с использованием типа данных с фиксированной точкой. В Haskell это есть Fix fи может быть определено как type Fix f = Free f ⊥(то есть деревья с fузлами -образной формы и без листьев вне функтора f). Традиционно эта структура также имеет складку, называемую cata:

cata :: Functor f => (f a -> a) -> Fix f -> a
cata alg x = fold absurd alg x

Что дает довольно аккуратное использование абсурда: поскольку у дерева не может быть никаких листьев (поскольку у ⊥ нет других жителей, кроме undefined), никогда не возможно использовать genдля этого сгиба и absurdиллюстрирует это!

Тип bottom - это подтип любого другого типа, который может быть чрезвычайно полезен на практике. Например, тип NULLв теоретической типобезопасной версии C должен быть подтипом любого другого типа указателя, в противном случае вы не сможете, например, вернуть, NULLгде char*ожидалось a ; аналогично, тип undefinedв теоретически безопасном типе JavaScript должен быть подтипом любого другого типа в языке.

В качестве возвращаемого типа функции также очень полезно иметь определенные функции, которые никогда не возвращаются. Например, в строго типизированном языке с исключениями, какой тип должен exit()или должен throw()возвращаться? Они никогда не возвращают поток управления своему абоненту. А поскольку нижний тип является подтипом любого другого типа, он вполне подходит для функции, возвращающей Intвместо return то есть возвращающая функция также может вообще не возвращать. (Может быть, он вызывает , или, может быть, он входит в бесконечный цикл.) Это хорошо иметь, потому что ли функция когда-либо возвращается или нет, классно неразрешима.$\bot$Intexit()

Наконец, это очень полезно для написания ограничений. Предположим, вы хотите ограничить все параметры на «обеих сторонах», предоставив тип, который должен быть супертипом параметра, и другой тип, который должен быть подтипом. Поскольку дно подтип любого типа, вы можете выразить «любой подтип S» как . Или вы можете выразить «любой тип вообще» как .$\bot \prec T \prec S$$\bot \prec T \prec \top$

Я могу придумать одно применение, и это то, что считается улучшением языка программирования Swift.

Свифт имеет maybeмонаду, пишется Optional<T>или T?. Есть много способов взаимодействия с ним.

• Вы можете использовать условное развертывание как

  if let nonOptional = someOptional {
      print(nonOptional)
  }
  else {
      print("someOptional was nil")
  }
  

• Вы можете использовать map, flatMapчтобы преобразовать значения

• Оператор принудительного развертывания ( !типа (T?) -> T) для принудительного развертывания содержимого, в противном случае происходит сбой

• Оператор nil-coalescing ( ??, типа (T?, T) -> T) принимает свое значение или иным образом использует значение по умолчанию:

  let someI = Optional(100)
  print(someI ?? 123) => 100 // "left operand is non-nil, unwrap it.
  
  let noneI: Int? = nil
  print(noneI ?? 123) // => 123 // left operand is nil, take right operand, acts like a "default" value
  

К сожалению, не было краткого способа сказать «развернуть или выбросить ошибку» или «развернуть или аварийно завершить работу с пользовательским сообщением об ошибке». Что-то вроде

let someI: Int? = Optional(123)
let nonOptionalI: Int = someI ?? fatalError("Expected a non-nil value")

не компилируется, потому что fatalErrorимеет тип () -> Never( ()есть Void, тип Neverустройства Swift, это нижний тип Swift). Вызов его производит Never, что несовместимо с Tожидаемым в качестве правильного операнда ??.

В попытке исправить это, был предложен продукт Swift Evolution SE-0217- оператор «Развернуть или умереть» . Это было в конечном счете отклонено , но это подняло интерес к тому, чтобы Neverбыть подтипом всех типов.

Если Neverзадан подтип всех типов, предыдущий пример будет компилируемым:

let someI: Int? = Optional(123)
let nonOptionalI: Int = someI ?? fatalError("Expected a non-nil value")

потому что сайт вызова ??имеет тип (T?, Never) -> T, который будет совместим с (T?, T) -> Tподписью ??.

Swift имеет тип «Никогда», который, похоже, очень похож на нижний тип: функция, объявленная для возврата «Никогда», никогда не сможет вернуться, функция с параметром типа «Никогда» никогда не может быть вызвана.

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

Для получения подробной информации вы должны взглянуть на новые сообщения в списке рассылки swift-evolution.