Заблуждение о классах типов и назначении переменных в Haskell

i :: a; i = 1

Я ожидал, что, поскольку я был напечатан как можно более обобщенно, я мог присвоить ему абсолютно все, что угодно. (Я знаю, что, вероятно, ничего не могу сделать с переменной i, но это не важно.)

Нет, все наоборот. Тип представляет, как это значение может быть использовано позже, т. е. он указывает, что пользователь может использовать i, притворяясь, что это значение любого типа, который может потребоваться в данный момент. По сути, пользователь выбирает тип a, и код, определяющий i :: a, должен соответствовать любому такому выбору пользователя.

(Кстати, мы обычно называем i = 1 привязкой или определением, а не присваиванием, поскольку это означает, что мы можем переназначить позже.)

gg :: Num a => a; gg = g 1.3
(error)

Здесь действует тот же принцип. gg претендует на любой числовой тип, который может понадобиться пользователю, но если пользователь позже выберет, скажем, Int, определение g 1.3 не подходит Int.

Пользователь может выбрать тип, используя явную сигнатуру (print (gg :: Int)) или поместив его в контекст, который определяет тип (print (length "hello" + gg) заставляет Int, поскольку length возвращает Int).

Если вы знакомы с дженериками в некоторых других языках, вы можете провести сравнение с этим кодом:

-- Haskell
i :: a
i = 1            -- type error

-- pseudo-Java
<A> A getI() {
  return 1;      -- type error
}

С более теоретической точки зрения вы думаете о неправильном квантификаторе. Когда вы пишете i :: a, вы думаете, что i :: exists a . a (не настоящий тип Haskell), который читается как i, является значением некоторого типа (выбранного во время определения). Вместо этого в Haskell i :: a означает i :: forall a . a, которое читается как i, является значением всех типов (любого типа, который может понадобиться при использовании). Следовательно, все сводится к существующим и forall или к тому, кто выбирает тип a на самом деле.