Ошибка типа при назначении допустимого типа поля для переменной с привязкой - PullRequest
Новая
       31

Ошибка типа при назначении допустимого типа поля для переменной с привязкой

14 голосов
/ 19 ноября 2011

Это ошибка в проверке типов? 

Prelude> let (x :: forall a. a -> a) = id in x 3

<interactive>:0:31:
    Couldn't match expected type `forall a. a -> a'
                with actual type `a0 -> a0'
    In the expression: id
    In a pattern binding: (x :: forall a. a -> a) = id

Тот факт, что вышеописанное не удается проверить тип, но это искажение успешно выполняется: 

Prelude> let (x :: (forall a. a -> a) -> Int) = (\f -> f 3) in x id
3

заставляет меня думать, что«Слабое преобразование пренекса» (см. стр. 23 этой статьи ) может быть как-то связано.Встраивание forall в контравариантную позицию, где его нельзя «выпустить», кажется, защищает его от этой странной ошибки.

Ответы [ 2 ]

4 голосов
/ 20 ноября 2011

Я думаю, что здесь происходит следующее: в стандартном выводе типа Damas - Milner, пусть привязки являются единственным местом, где происходит обобщение типа. Сигнатура типа, используемая в вашем неудачном примере, - это сигнатура типа шаблона , которая «очевидным образом ограничивает тип шаблона». Теперь в этом примере не «очевидно», должно ли это ограничение происходить до или после обобщения, но ваш неудачный пример демонстрирует, я думаю, что оно применяется до обобщения.

Конкретнее: в привязке let let x = id in ... происходит то, что тип id forall a. a->a создается в монотипе, скажем a0 -> a0, который затем присваивается типу x и затем обобщается как forall a0. a0 -> a0. Если, как мне кажется, сигнатура типа шаблона проверяется перед обобщением, то, по сути, она просит компилятор проверить, является ли монотип a0 -> a0 более общим, чем политип forall a. a -> a, а это не так.

Если мы переместим сигнатуру типа на уровень привязки, let x :: forall a. a-> a; x = id in ... сигнатура проверяется после обобщения (поскольку это явно разрешено для обеспечения полиморфной рекурсии), и ошибка типа не возникает.

Является ли это ошибкой или нет, я думаю, вопрос мнения. Кажется, нет реальной спецификации, которая бы указала нам, каково здесь правильное поведение; Есть только наши ожидания. Я бы предложил обсудить этот вопрос с людьми из GHC.

2 голосов
/ 19 ноября 2011

Не настоящий ответ, но слишком длинный для комментария:
Это может быть ошибкой.Немного поэкспериментируя с выражением, неудивительно, что 

let x :: forall a. a -> a; x = id in x 3

работает, если разрешено написание явных сообщений.Это стандартный тип ранга 1.Некоторые другие варианты: 

$ ghci-6.12.3 -ignore-dot-ghci -XRankNTypes -XScopedTypeVariables
Prelude> let (x :: forall a. a -> a) = \y -> id y in x 3
3

Хорошо, это работает, я не знаю, почему лямбда ведет себя по-другому, но это так.Однако: 

$ ghci -ignore-dot-ghci -XRankNTypes -XScopedTypeVariables
Prelude> let (x :: forall a. a -> a) = \y -> id y in x 3

<interactive>:0:31:
    Couldn't match expected type `t0 -> t1'
                with actual type `forall a. a -> a'
    The lambda expression `\ y -> id y' has one argument,
    but its type `forall a. a -> a' has none
    In the expression: \ y -> id y
    In a pattern binding: (x :: forall a. a -> a) = \ y -> id y

(7.2.2; 7.0.4 выдает ту же ошибку).Это удивительно.

...