Интуиция за кодированием двойного отрицания с типом дна Ничего

Question

Бесформенные кодирует двойное отрицание , как это

type ¬[T] = T => Nothing
type ¬¬[T] = ¬[¬[T]]

, то есть

(T => Nothing) => Nothing

Мили объясняет

... нижний тип (тип Scala Nothing) отображается на логическую ложь ... отрицание типа A (я напишу его как ¬[A]), чтобы иметь в качестве значений все, что не является экземпляр A

Nothing также используется для представления не прекращения , то есть вычисления, которое не может привести к значению

def f[T](x: T): Nothing = f(x)

Применение этой интерпретации к (T => Nothing) => Nothing, кажется, означает:

(          T                   =>                Nothing           )    =>          Nothing 
Assuming a value of type T,   then   the program does not terminate,   hence  it never produces a value.

Правильна ли эта интуиция? Являются ли понятия лжи и не прекращения эквивалентными? Если так, то почему программа, которая не производит значение, которое не производит значение, означает, что у нас есть значение T?

Answer 1

Если это так, почему наличие программы, которая не производит значение, которое не производит значение, означает, что у нас есть значение T?

Это не так. Логика c, вытекающая из соответствия Карри – Ховарда , не классическая, а intuitionisti c. Не существует закона исключенного среднего T ∨ ¬T _{(но есть двойное отрицание закона исключенного среднего)} .

¬¬T не эквивалентно T.

T => ¬¬T, но не ¬¬T => T.

Эквивалентны ли понятия лжи и недопущения?

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

Nothing ( или тип дна ⊥) не заселен (соответствует false). Если T заселен, то T => Nothing не заселен (в противном случае Nothing будет заселен). Если T => Nothing обитаем, то T нет (опять же, в противном случае Nothing будет обитаемым). Это причина для определения ¬T = T => Nothing.

Когда рассматривается отсутствие завершения, это означает, что каждый тип T поднимается до типа T', состоящего из элементов T и нижнего значения ⊥ ( расхождение , не путать с типом дна).