Простой пример для ImpredicativeTypes

В руководстве пользователя GHC описывается расширение нежизнеспособного полиморфизма со ссылкой на следующий пример:

f :: Maybe (forall a. [a] -> [a]) -> Maybe ([Int], [Char])
f (Just g) = Just (g [3], g "hello")
f Nothing  = Nothing

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

ghci> f (Just reverse)

<interactive>:8:9:
    Couldn't match expected type `forall a. [a] -> [a]'
                with actual type `[a0] -> [a0]'
    In the first argument of `Just', namely `reverse'
    In the first argument of `f', namely `(Just reverse)'
    In the expression: f (Just reverse)
ghci> f (Just id)

<interactive>:9:9:
    Couldn't match expected type `forall a. [a] -> [a]'
                with actual type `a0 -> a0'
    In the first argument of `Just', namely `id'
    In the first argument of `f', namely `(Just id)'
    In the expression: f (Just id)

По-видимому, только undefined, Nothing или Just undefined удовлетворяет проверке типов.

У меня есть два вопроса, поэтому:

Можно ли вызывать вышеуказанную функцию с помощью Just f для любого не-нижнего f?
Может ли кто-нибудь представить пример значения, определяемого только с помощью недискриминационного полиморфизма и используемого нетривиальным способом?

Последнее особенно связано с страницей HaskellWiki по Импрессивному Полиморфизму, которая в настоящее время делает явно неубедительный случай существования расширения.

Ответ 1

Здесь пример того, как один проект const-math-ghc-plugin использует ImpredicativeTypes для указания списка совпадающих правил.

Идея состоит в том, что когда мы имеем выражение вида App (PrimOp nameStr) (Lit litVal), мы хотим найти соответствующее правило, основанное на имени primop. A litVal будет либо a MachFloat d, либо MachDouble d (d является Rational). Если мы найдем правило, мы хотим применить функцию для этого правила к d, преобразованному в правильный тип.

Функция mkUnaryCollapseIEEE делает это для унарных функций.

mkUnaryCollapseIEEE :: (forall a. RealFloat a => (a -> a))
                    -> Opts
                    -> CoreExpr
                    -> CoreM CoreExpr
mkUnaryCollapseIEEE fnE opts [email protected](App f1 (App f2 (Lit lit)))
    | isDHash f2, MachDouble d <- lit = e d mkDoubleLitDouble
    | isFHash f2, MachFloat d  <- lit = e d mkFloatLitFloat
    where
        e d = evalUnaryIEEE opts fnE f1 f2 d expr

Первый аргумент должен иметь тип Rank-2, потому что он будет создан в Float или Double в зависимости от конструктора литерала. Список правил выглядит следующим образом:

unarySubIEEE :: String -> (forall a. RealFloat a => a -> a) -> CMSub
unarySubIEEE nm fn = CMSub nm (mkUnaryCollapseIEEE fn)

subs =
    [ unarySubIEEE "GHC.Float.exp"    exp
    , unarySubIEEE "GHC.Float.log"    log
    , unarySubIEEE "GHC.Float.sqrt"   sqrt
    -- lines omitted
    , unarySubIEEE "GHC.Float.atanh"  atanh
    ]

Это нормально, если слишком много шаблонов для моего вкуса.

Однако существует аналогичная функция mkUnaryCollapsePrimIEEE. В этом случае правила различны для разных версий GHC. Если мы хотим поддерживать несколько GHC, это становится немного сложнее. Если бы мы приняли тот же подход, определение subs потребовало бы много CPP, что может быть недостижимым. Вместо этого мы определили правила в отдельном файле для каждой версии GHC. Однако mkUnaryCollapsePrimIEEE недоступен в этих модулях из-за циклических проблем с импортом. Возможно, мы могли бы переструктурировать модули, чтобы они работали, но вместо этого мы определили набор правил как:

unaryPrimRules :: [(String, (forall a. RealFloat a => a -> a))]
unaryPrimRules =
    [ ("GHC.Prim.expDouble#"    , exp)
    , ("GHC.Prim.logDouble#"    , log)
    -- lines omitted
    , ("GHC.Prim.expFloat#"     , exp)
    , ("GHC.Prim.logFloat#"     , log)
    ]

Используя ImpredicativeTypes, мы можем сохранить список функций Rank-2, готовый для использования для первого аргумента mkUnaryCollapsePrimIEEE. Альтернативами было бы намного больше CPP/шаблона, изменение структуры модуля (или кругового импорта) или много дублирования кода. Ничего из того, что я хотел бы.

Кажется, я помню штаб-квартиру GHC, указав, что они хотели бы отказаться от поддержки расширения, но, возможно, они пересмотрели. Это очень полезно время от времени.

Ответ 2

Разве это не просто, что ImpredicativeTypes было тихо сброшено с помощью нового typechecker в ghc-7 +? Обратите внимание, что ideone.com по-прежнему использует ghc-6.8, и действительно, ваша программа используется для правильной работы:

{-# OPTIONS -fglasgow-exts  #-}

f :: Maybe (forall a. [a] -> [a]) -> Maybe ([Int], [Char])
f (Just g) = Just (g [3], g "hello")
f Nothing  = Nothing

main   = print $ f (Just reverse)

печатает Just ([3],"olleh"), как ожидалось; см. http://ideone.com/KMASZy

augustss дает красивый прецедент - своего рода имитацию Python dsl - и защиту расширения здесь: http://augustss.blogspot.com/2011/07/impredicative-polymorphism-use-case-in.html, упомянутый в билете здесь http://hackage.haskell.org/trac/ghc/ticket/4295

Ответ 3

Обратите внимание на это обходное решение:

justForF :: (forall a. [a] -> [a]) -> Maybe (forall a. [a] -> [a])
justForF = Just

ghci> f (justForF reverse)
Just ([3],"olleh")

Или это одно (что в основном одно и то же):

ghci> f $ (Just :: (forall a. [a] -> [a]) -> Maybe (forall a. [a] -> [a])) reverse
Just ([3],"olleh")

Похоже, что вывод типа имеет проблемы с отображением типа Just в вашем случае, и мы должны сообщить ему тип.

У меня нет подсказки, если это ошибка или если есть веская причина для этого..:)