Ошибка компиляции Haskell с двумя ошибками полиморфизма

Учитывая следующие определения:

import Control.Monad.ST
import Data.STRef

fourty_two = do
  x <- newSTRef (42::Int)
  readSTRef x

Следующие компиляции под GHC:

main = (print . runST) fourty_two -- (1)

Но это не так:

main = (print . runST) $ fourty_two -- (2)

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

main = ((print . runST) $) fourty_two -- (3)

Но это не компилирует

main = (($) (print . runST)) fourty_two -- (4)

Который, по-видимому, указывает, что (3) компилируется только из-за специальной обработки инфикса $, однако он все еще не объясняет, почему (1) компилируется.

Вопросы:

1) Я прочитал следующие два вопроса (первый, второй), и я ' верили, что $ может быть введено только с мономорфными типами. Но я бы предположил, что . может быть создан только с мономорфными типами, и в результате аналогичным образом потерпит неудачу. Почему первый код преуспевает, а второй - нет? (например, существует ли специальное правило GHC для первого случая, что оно не может применяться во втором?)

2) Существует ли текущее расширение GHC, которое компилирует второй код? (возможно, ImpredicativePolymorphism сделал это в какой-то момент, но, похоже, он устарел, что-нибудь заменило его?)

3) Есть ли способ определить say `my_dollar` с помощью расширений GHC, чтобы делать то, что делает $, но также способен обрабатывать полиморфные типы, поэтому (print . runST) `my_dollar` fourty_two компилирует?

Изменить: Предлагаемый ответ:

Кроме того, следующее не удается скомпилировать:

main = ((.) print runST) fourty_two -- (5)

Это то же самое, что и (1), за исключением использования версии infix ..

В результате кажется, что GHC имеет специальные правила для $ и ., но только для своих инфиксных версий.

Ответы

Ответ 1

  • Я не уверен, что понимаю, почему второй не работает. Мы можем посмотреть на тип print . runST и заметить, что он достаточно полиморфен, поэтому вина не лежит на (.). Я подозреваю, что специального правила, которое GHC имеет для infix ($), просто недостаточно. SPJ и друзья могут быть открыты для повторного изучения, если вы предлагаете этот фрагмент как ошибку на своем трекере.

    Что касается того, почему работает третий пример, ну, так как снова тип ((print . runST) $) достаточно полиморфен; на самом деле он равен типу print . runST.

  • Ничто не заменило ImpredicativePolymorphism, потому что люди GHC не видели каких-либо вариантов использования, в которых дополнительное программистское преимущество перевешивало дополнительный потенциал для ошибок компилятора. (Я не думаю, что они увидят это как убедительное, хотя, конечно, я не авторитет.)

  • Мы можем определить несколько менее полиморфный ($$):

    {-# LANGUAGE RankNTypes #-}
infixl 0 $$
($$) :: ((forall s. f s a) -> b) -> ((forall s. f s a) -> b)
f $$ x = f x

    Тогда ваш пример typechecks в порядке с этим новым оператором:

    *Main> (print . runST) $$ fourty_two
42

Ответ 2

Я не могу сказать слишком много полномочий по этому вопросу, но здесь, как я думаю, может произойти:

Рассмотрим, что должен делать typechecker в каждом из этих случаев. (print . runST) имеет тип Show b => (forall s. ST s t) -> IO (). fourty_two имеет тип ST x Int.

forall здесь - спецификатор экзистенциального типа - здесь это означает, что переданный аргумент должен быть универсальным на s. То есть вы должны пройти в полиморфном типе, который поддерживает любое значение для s. Если вы явно не указали forall, Haskell ставит его на крайний уровень определения типа. Это означает, что fourty_two :: forall x. ST x Int и (print . runST) :: forall t. Show t => (forall s. ST s t) -> IO ()

Теперь мы можем сопоставить forall x. ST x Int с forall s. ST s t, разрешив t = Int, x = s. Так работает случай прямого вызова. Что произойдет, если мы будем использовать $, хотя?

$ имеет тип ($) :: forall a b. (a -> b) -> a -> b. Когда мы разрешаем a и b, так как тип для $ не имеет какого-либо явного типа, как показано на рисунке, аргумент x fourty_two получает доступ к самой внешней области в типе для ($) - so ($) :: forall x t. (a = forall s. ST s t -> b = IO ()) -> (a = ST x t) -> IO (). На этом этапе он пытается сопоставить a и b и не работает.

Если вы вместо этого напишите ((print . runST) $) fourty_two, тогда компилятор сначала разрешит тип ((print . runST $). Он решает тип для ($) как forall t. (a = forall s. ST s t -> b = IO ()) -> a -> b; обратите внимание, что, поскольку вторая ошибка a не ограничена, у нас нет такой переборчивой переменной, которая протекает в самый дальний объем! И поэтому совпадение выполняется успешно, функция частично применяется, и общий тип выражения forall t. (forall s. ST s t) -> IO (), который находится прямо здесь, где мы начали, и поэтому он преуспевает.