Как работают Пустота и Абсурд

Question

Исходный код для Void состояний:

newtype Void = Void Void

instance showVoid :: Show Void where
    show = absurd

absurd :: forall a. Void -> a
absurd a = spin a
    where
    spin (Void b) = spin b

Кажется, Void - бесконечно рекурсивный тип, в то время как absurd - бесконечно рекурсивная функция. Я попытался запустить show ((unsafeCoerce "lol") :: Void) в REPL, и он быстро вошел в бесконечный цикл.

Что меня беспокоит, так это сигнатура типа absurd :: forall a. Void -> a. Как действительна подпись? Разве компилятор распознает бесконечно рекурсивные функции и позволяет им иметь любой возвращаемый тип, зная, что они никогда не прекратят работу при вызове? Разве просто absurd = unsafeCoerce не даст такой же эффект?

Answer 1

Реализация absurd на самом деле не имеет значения, так как невозможно иметь значение Void - его невозможно построить.Вот почему так безопасно иметь такую ​​функцию - она ​​не создает что-то из ничего, просто этого никогда не произойдет, поэтому она используется только для доказательства проверки типов.Так что да, unsafeCoerce также можно безопасно использовать.

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

Answer 2

Нет, компилятор не распознает бесконечно циклические функции. На самом деле известно, что это невозможно - см. Проблема остановки .

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

---

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

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