Какой вид Пустоты?

Ответ 1

0 не считалось числом. "Как ничто не может быть чем-то?" Но со временем мы стали принимать 0 как число, заметив его свойства и полезность. Сегодня идея о том, что 0 - это не число, столь же абсурдна, как и идея о том, что это было 2000 лет назад.

Void является типом так же, как 0 является числом. Его вид *, как и все другие типы. Сходство между Void и 0 проходит довольно глубоко, как показывает ответ Тихона Джелвиса. Существует сильная математическая аналогия между типами и числами, где Either играет роль сложения, tupling (,) играет роль умножения, функции (->) - возведение в степень (a → b означает b ^a), () (произносится). "unit") как 1, а Void как 0.

Число значений, которые может принимать тип, является числовой интерпретацией типа. Так

Either () (Either () ())

интерпретируется как

1 + (1 + 1)

поэтому мы должны ожидать три значения. И действительно, их ровно три.

Left ()
Right (Left ())
Right (Right ())

Так же,

(Either () (), Either () ())

интерпретируется как

(1 + 1) * (1 + 1)

поэтому мы должны ожидать четыре значения. Вы можете перечислить их?

Возвращаясь к Void, вы можете иметь, скажем, Either() Void, который будет интерпретироваться как 1 + 0. Конструкторами этого типа являются Left() и Right v для каждого значения v типа Void - однако есть нет значений типа Void, поэтому единственным конструктором для Either() Void является Left(). И 1 + 0 = 1, поэтому мы получили то, что ожидали.

Упражнение: какой должна быть математическая интерпретация " Maybe a быть"? Сколько значений Maybe Void существует - соответствует ли это интерпретации?

Заметки

• Я игнорирую пристрастность в этом обращении, притворяясь, что Хаскелл тотален. Технически undefined может иметь тип Void, но нам нравится использовать быстрые и свободные рассуждения, которые игнорируют их.
• То, как void используется в языках на основе C, на самом деле намного больше похоже на Haskell () чем на Haskell Void. В Haskell функция, возвращающая Void вообще не может возвращаться, тогда как в языках C функция, возвращающая void может возвращать, но возвращаемое значение неинтересно - есть только одна вещь, так что зачем беспокоиться?

Ответ 2

Это тип вида * как Int, Bool или (). Это просто имеет 0 значений вместо 1 или 2 или более.

Это не хак, а фундаментальная часть системы типа Haskell. Он играет роль от 0 до () 1 и, если мы рассматриваем типы как предложения, Void соответствует предложению "ложь". Он также идентичен типам сумм (Either), точно так же, как () является идентификатором типов продукта: Either a Void изоморфен a.

На практике он часто выступает как двойственный (); лучший пример этого, который я видел, находится в pipes, где () используется для тега объектов, которые не принимают входы, и Void (с именем X) используется для обозначения объектов, не выдающих выходы. (См. Приложение: Типы в учебнике.)

Это способ отметить вещи как невозможные или отсутствующие, но это отнюдь не взломать.

Ответ 3

Еще один поворот в этом вопросе: предположим, я попросил вас написать гарантированную функцию завершения типа a -> b:

aintGonnaWork :: a -> b
aintGonnaWork a = _

Как можно надеяться, невозможно написать такую ​​функцию. Из этого следует, что тип a -> b не имеет определенных значений. Также обратите внимание, что тип a -> b равен *:

(->)   :: * -> * -> *
a      :: *
b      :: *
---------------------
a -> b :: *

И там у нас это: тип вида *, построенный из "vanilla" элементов Haskell (без "хаков" ), но тем не менее не имеющих определенных значений. Таким образом, существование таких типов, как Void, уже подразумевается в "vanilla" Haskell; все, что делает явный тип Void, - это стандарт, названный одним.

Я завершу простую реализацию типа Void в терминах вышеизложенного; единственное необходимое расширение - RankNTypes.

{-# LANGUAGE RankNTypes #-}

newtype Void = Void (forall a b. a -> b)

absurd :: Void -> a
absurd (Void f) = f f

Ответ 4

Луис Касильяс показал, что полиморфный тип может быть необитаем в ванильном Хаскеле. Но есть и необитаемые мономорфные типы. Классический выглядит так:

data Void = Void !Void

absurd :: Void -> a
absurd (Void x) = absurd x

Представьте, что вы пытаетесь создать что-то типа Void.

void :: Void
void = Void _

Вам нужно что-то типа Void чтобы заполнить дыру. Так как в этом весь смысл void, единственный разумный выбор

void :: Void
void = Void void

Если бы конструктор Void был ленивым, это была бы циклическая структура Void (Void (Void...)). Но поскольку оно строгое, void может быть записана как

void = void 'seq' Void void

который явно не собирается летать.