Какой тип ничего в Haskell?

Ответ 1

Это не противоречит. Nothing - это значение, и его конкретный тип может быть любым возможным экземпляром Maybe a.

В противном случае значения типа Maybe a продолжают иметь конкретные типы Maybe Int, Maybe String, Maybe Whatever и, в частности, Nothing может быть набрано каждым из них, в зависимости от контекста, Это потому, что его конструктор, который снова называется Nothing :: Maybe a, не принимает никаких параметров и поэтому его можно вызывать как-для генерации значений типа Maybe a. Если хотите, у нас будет один для конкретного типа.

Без контекста, конечно, ghci даст вам самый общий тип, который он может сделать для Nothing, который есть Maybe a, но это не его конкретный тип. Это будет зависеть от отдельных выражений, которые вы будете использовать Nothing in. Например:

ghci> Nothing
Nothing
it :: Maybe a

Это то, что вы, вероятно, набрали, или что-то в этом роде. Дальнейшего контекста нет, поэтому Nothing не набирается с конкретным типом.

ghci> Nothing :: Maybe Int
Nothing
it :: Maybe Int

Здесь я заставил его принять конкретный тип Maybe Int.

ghci> 1 + fromMaybe 2 Nothing
3
it :: Integer

Если я смешиваю его с суммой целых чисел (fromMaybe :: a -> Maybe a -> a принимает значение по умолчанию и Maybe a и возвращает либо значение в Just, либо значение по умолчанию с Nothing), тогда Nothing будет введенный системой Maybe Integer, так как вы ожидаете извлечь из нее целое число. Там нет, поэтому в этом случае мы суммируем 1 со значением по умолчанию 2.

ghci> 1 + fromMaybe 2 (Nothing :: Maybe Integer)
3
it :: Integer

То же самое, чтобы дважды проверить. Мы вынуждаем Nothing иметь конкретный тип, который мы предположили ранее в том же выражении.

ghci> 1 + fromMaybe 2 (Nothing :: Maybe Char)

<interactive>:1:15:
    No instance for (Num Char)
      arising from the literal `2'
    Possible fix: add an instance declaration for (Num Char)
    In the first argument of `fromMaybe', namely `2'
    In the second argument of `(+)', namely
      `fromMaybe 2 (Nothing :: Maybe Char)'
    In the expression: 1 + fromMaybe 2 (Nothing :: Maybe Char)

Для тройной проверки, если мы вынудим его принять другой конкретный тип, так как вы увидите, что его значение будет совершенно иным, что приведет к ошибке типа (в отличие от C, в Haskell Char не действует как число).

Ответ 2

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

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

На самом деле в Haskell существует много полиморфных нефункциональных значений, таких как

1 :: Num a => a
Nothing :: Maybe a
[] :: [a]
Left 1 :: Num a => Either a b

и т.д.. Эти значения существуют для каждого экземпляра a (и b).

Ответ 3

В некотором смысле вы правы. Нет значений типа forall a.Maybe a. Каждое построенное значение Maybe может иметь определенный тип Maybe tau, где tau может быть известен или нет, но является определенным типом.

Обозначение Nothing :: forall a.Maybe a просто говорит нам, что всякий раз, когда мы используем выражение Nothing, оно построит значение ожидаемого типа Maybe.

Ответ 4

Тип Maybe имеет два конструктора: Nothing и Just a, где a - переменная типа. Ничто само не определяет (ограничивает) тип, но в любом разумном контексте вы найдете что-то вроде (я не утверждаю, что это синтаксически корректный Haskell, но то, что я бы написал 10 лет назад):

if (foo == 5)
then Nothing
else Just 5

И затем введите вывод, что (предположим, что 5 был аргументом для этого фрагмента кода "foo" типа Int), который имеет тип foo:

foo :: Int -> Maybe Int

Но, как указывал предыдущий плакат, может быть, это совершенно хороший тип. Вы найдете ту же самую проблему с [], т.е. Тип списка с [] (конструктор для пустого списка).

Ответ 5

Этот разговор в 26:00 отвечает на вопрос: "Каков тип [ ]?" что связано с вопросом: "Каков тип Nothing?".

Также у книги Худака есть хороший параграф: