Возьмите скромную функцию идентификации в Haskell,
id :: forall a. a -> a
Учитывая, что Haskell предположительно поддерживает недискриминационный полиморфизм, представляется разумным, что я должен "ограничивать" id
типом (forall a. a -> a) -> (forall b. b -> b)
по типу типа. Но это не работает:
Prelude> id :: (forall a. a -> a) -> (forall b. b -> b)
<interactive>:1:1:
Couldn't match expected type `b -> b'
with actual type `forall a. a -> a'
Expected type: (forall a. a -> a) -> b -> b
Actual type: (forall a. a -> a) -> forall a. a -> a
In the expression: id :: (forall a. a -> a) -> (forall b. b -> b)
In an equation for `it':
it = id :: (forall a. a -> a) -> (forall b. b -> b)
Конечно, можно определить новую ограниченную форму тождественной функции с нужной сигнатурой:
restrictedId :: (forall a. a -> a) -> (forall b. b -> b)
restrictedId x = x
Однако определение его в терминах общего id
не работает:
restrictedId :: (forall a. a -> a) -> (forall b. b -> b)
restrictedId = id -- Similar error to above
Итак, что здесь происходит? Похоже, что это может быть связано с трудностями с непроницаемостью, но включение -XImpredicativeTypes
не имеет значения.