Доказательство в полиморфных типах
В Практический тип вывода для произвольного типа ранга, авторы говорят о предположении:
![3.3 Subsumption]()
Я пытаюсь проверить вещи в GHCi, когда читаю, но даже если g k2 предназначен для проверки типов, это не происходит, когда я пытаюсь использовать GHC 7.8.3:
λ> :set -XRankNTypes
λ> let g :: ((forall b. [b] -> [b]) -> Int) -> Int; g = undefined
λ> let k1 :: (forall a. a -> a) -> Int; k1 = undefined
λ> let k2 :: ([Int] -> [Int]) -> Int; k2 = undefined
λ> :t g k1
<interactive>:1:3: Warning:
Couldn't match type ‘a’ with ‘[a]’
‘a’ is a rigid type variable bound by
the type forall a1. a1 -> a1 at <interactive>:1:3
Expected type: (forall b. [b] -> [b]) -> Int
Actual type: (forall a. a -> a) -> Int
In the first argument of ‘g’, namely ‘k1’
In the expression: g k1
g k1 :: Int
λ> :t g k2
<interactive>:1:3: Warning:
Couldn't match type ‘[Int] -> [Int]’ with ‘forall b. [b] -> [b]’
Expected type: (forall b. [b] -> [b]) -> Int
Actual type: ([Int] -> [Int]) -> Int
In the first argument of ‘g’, namely ‘k2’
In the expression: g k2
g k2 :: Int
Я до сих пор не дошел до того, что понял документ, но все же, я беспокоюсь, что что-то не понял. Должна ли эта typecheck? Являются ли мои Haskell неправильными?
Ответы
Ответ 1
Признак typechecker не знает, когда применять правило подзапроса.
Вы можете сказать это, когда со следующей функцией.
Prelude> let u :: ((f a -> f a) -> c) -> ((forall b. f b -> f b) -> c); u f n = f n
Это говорит о том, что, учитывая функцию из преобразования для определенного типа, мы можем сделать функцию из естественного преобразования forall b. f b -> f b.
Затем мы можем попробовать его на втором примере.
Prelude> :t g (u k2)
g (u k2) :: Int
Первый пример также дает более информативную ошибку.
Prelude> :t g (u k1)
Couldn't match type `forall a. a -> a' with `[a0] -> [a0]'
Expected type: ([a0] -> [a0]) -> Int
Actual type: (forall a. a -> a) -> Int
In the first argument of `u', namely `k1'
In the first argument of `g', namely `(u k1)'
Я не знаю, можем ли мы написать более общую версию u; нам понадобится понятие уровня ограничения на менее полиморфное, чтобы написать что-то вроде let s :: (a :<: b) => (a -> c) -> (b -> c); s f x = f x
