GHC не может связать полиморфную функцию без ее мономорфизации - PullRequest
Новая
       74

GHC не может связать полиморфную функцию без ее мономорфизации

0 голосов
/ 21 января 2019

В исходном коде видно, что я просто извлекаю выражение в привязку, что является одной из основных вещей, которые, как заявляет haskell, должны быть всегда возможны.

Минимальный регистр (создается с помощьюпомощь @dminuoso на freenode)

Я бы хотел, чтобы g оставался полиморфным (чтобы я мог передать его другим функциям, которые ожидают этого): 

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}

main = do
    let a :: forall t. Functor t => t () = undefined
    let g :: forall u. Functor u => u () = a
    pure ()

ошибка: 

source_file.hs:6:44:
    Couldn't match expected type ‘forall (u :: * -> *).
                                  Functor u =>
                                  u ()’
                with actual type ‘t0 ()’
    When checking that: t0 ()
      is more polymorphic than: forall (u :: * -> *). Functor u => u ()
    In the expression: a

Исходный вопрос (мотивация) размещен на #haskell IRC: 

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}


class Monad m => Monad' m where

instance Monad' IO where

f1 :: (forall m . Monad' m => m Int) -> IO Int
f1 g = do
    let a :: forall n . Monad' n => n Int = g
    a

-- this works
--f1 :: (forall m . Monad' m => m Int) -> IO Int
--f1 g = do
--    g

main = print $ "Hello, world!"

но я получаю: 

source_file.hs:12:45:
    Couldn't match expected type ‘forall (n :: * -> *).
                                  Monad' n =>
                                  n Int’
                with actual type ‘m0 Int’
    When checking that: m0 Int
      is more polymorphic than: forall (n :: * -> *). Monad' n => n Int
    In the expression: g

На основе https://ghc.haskell.org/trac/ghc/ticket/12587 Я пытался явно применить тип, чтобы помочь проверщику типов: 

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}

class Monad m => Monad' m where

instance Monad' IO where

f1 :: (forall m . Monad' m => m Int) -> IO Int
f1 g = do
    let a :: forall n . Monad' n => n Int = g @n
    a

main = print $ "Hello, world!"

, но затем я получаю: 

main.hs:13:48: error: Not in scope: type variable ‘n’

Ответы [ 4 ]

0 голосов
/ 22 января 2019

часть 1

Добро

Что происходит, когда вы пишете 

a :: forall f. Functor f => f ()
a = _

? В частности, какой тип выражения GHC ищет, чтобы заполнить дыру (_)? Вы можете подумать, что он ищет forall f. Functor f => f (), но это не совсем верно. Вместо этого a на самом деле немного больше похоже на функцию, и GHC неявно вставляет два аргумента: один аргумент типа с именем f с видом * -> * и один экземпляр ограничения Functor f (который безымянный, как и все экземпляры). 

a :: forall f. Functor f => f ()
a @f {Functor f} = _
-- @-syntax is a currently proposed extension, {}-syntax is fake

GHC ищет, в контексте type f :: * -> *; instance Functor f, f (). Это та же разница, что и между поиском (A -> B) -> C -> D и поиском D в контексте f :: A -> B; c :: C. Если у меня непосредственно есть solution :: (A -> B) -> C -> D, в первом случае я могу просто написать solution, но во втором случае я должен выписать solution f c.

Плохой

Это не то, что происходит, когда вы пишете 

a :: forall f. Functor f => f () = _

Поскольку вы использовали сигнатуру типа шаблона, а не обычную, GHC больше неявно связывает переменную типа и экземпляр для вас. Теперь GHC, честно и искренне, хочет, чтобы вы заполнили _ forall f. Functor f => f (). Это сложно, как мы скоро увидим ...

(Я действительно не думаю, что то, что цитировал Дэниел Вагнер, уместно здесь. Я полагаю, что это просто относится к разнице (когда ScopedTypeVariables включен и type a не входит в область видимости) между тем, как 5 :: Num a => a неявно означает 5 :: forall a. Num a => a, а значение g :: a -> a = id не означает g :: forall a. a -> a = id.)

Часть 2

Что происходит, когда вы пишете 

undefined

? В частности, каков его тип? Вы можете подумать, что это forall a. a, но это не совсем верно. Да, это правда, что само по себе , undefined имеет тип forall a. a, но GHC не позволяет вам писать undefined само по себе. Вместо этого каждое вхождение undefined в выражении всегда применяется к аргументу типа. Вышесказанное неявно переписано на 

undefined @_a0

и новая переменная объединения (которая на самом деле не имеет имени) _a0 создана. Это выражение имеет тип _a0. Если я использую это выражение в контексте, который требует Int, то _a0 должен быть равен Int, и GHC устанавливает _a0 := Int, переписывая выражение в 

undefined @Int

(Поскольку _a0 может быть , установить на что-то, это называется переменной объединения. Она находится под «нашим», внутренним контролем. Выше f не может быть установить на что угодно. Это данность, и она находится под «своим» (пользователем) внешним управлением, что делает его переменной сколем.)

часть 3

Добро

Обычно автоматическое связывание переменных типа и автоматическое применение переменных объединения работают хорошо. Например, оба из них работают нормально: 

undefined :: forall a. a

bot :: forall a. a
bot = undefined

Потому что они соответственно расширяются как 

(\@a -> undefined @a) :: forall a. a

bot :: forall a. a
bot @a = undefined @a

Средний

Когда вы делаете 

a :: forall f. Functor f => f () = undefined

, вы делаете что-то очень странное, случается. Как я уже говорил, сигнатура типа шаблона с forall ничего не вводит. undefined на RHS фактически должно быть forall f. Functor f => f (). Неявное применение переменных объединения все еще происходит: 

a :: forall f. Functor f => f () = undefined @_a0

undefined @_a0 :: _a0, поэтому _a0 ~ (forall f. Functor f => f ()) должно удерживаться. GHC, таким образом, должен установить _a0 := (forall f. Functor f => f ()). Обычно это нет-нет, потому что это непредсказуемый полиморфизм: установка переменной типа для типа, содержащего forall s. Однако в достаточно устаревших GHC это разрешено для определенных функций. То есть undefined не определен с типом forall (a :: *). a, но forall (a :: OpenKind). a, где OpenKind допускает эту непредсказуемость. Это означает, что ваш код проходит как 

a :: forall f. Functor f => f () = undefined @(forall f. Functor f => f ())

Если вы напишите 

a :: forall f. Functor f => f () = bot

, это не сработает, так как bot не имеет того же волшебного соуса, что и undefined. Кроме того, это не будет работать в более поздних GHC, которые исключили этот странный вид непредсказуемого полиморфизма. (Что я говорю, это очень хорошая вещь).

Плохое

Ваше определение a, даже с сигнатурой шаблона, действительно дает желаемый тип forall f. Functor f => f (). Теперь проблема в g: 

g :: forall f. Functor f => f () = a

g, опять же, не связывает type f :: * -> * или instance Functor f. Между тем a применяется к некоторым неявным вещам: 

g :: forall f. Functor f => f () = a @_f0 {_}

Но ... RHS теперь имеет тип _f0 (), и LHS хочет, чтобы он имел тип forall f. Functor f => f (). Они не похожи друг на друга. Поэтому введите error.

Поскольку вы не можете остановить неявное применение a к переменной типа и просто написать g = a, вы должны вместо этого разрешить неявное связывание переменных типа в g: 

g :: forall f. Functor f => f ()
g = a

Это работает.

0 голосов
/ 21 января 2019

Если я вставлю напечатанное отверстие, GHC даст мне это: 

foo.hs:11:45: error:
    • Cannot instantiate unification variable ‘t0’
      with a type involving foralls:
        forall (b :: * -> *). Monad' b => b Int
        GHC doesn't yet support impredicative polymorphism
    • In the expression: _
      In a pattern binding:
        a :: forall (b :: * -> *). Monad' b => b Int = _
      In the expression:
        do let a :: forall b. Monad' b => b Int = _
           a
   |
11 |     let a :: forall b . Monad' b => b Int = _
   |

С учетом комментария GHC doesn't yet support impredicative polymorphism возможно, то, что вы пытаетесь, пока невозможно.

0 голосов
/ 21 января 2019

Соответствующий бит документации о сигнатурах типов шаблонов таков:

В отличие от сигнатур типов выражений и объявлений, сигнатуры типов шаблонов неявно обобщаются.

Таким образом, сигнатуры шаблонов, как и то, что вы написали, представляют собой особый случай, когда обобщение (которое представляет собой процесс превращения мономорфного типа t, в котором упоминается переменная типа вне области действия a, в полиморфный типforall a. t) не сделано.Вы можете восстановить процесс обобщения, используя любую другую форму сигнатуры типа;например, вместо 

let foo :: forall a. a = undefined

попробуйте: 

let foo :: forall a. a
    foo = undefined
0 голосов
/ 21 января 2019

, как указал @Lears на freenode, поместив объявление типа выше , объявление исправляет его, так что, скорее всего, это какая-то ошибка в GHC. т.е. 

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}

main = do
    let a :: forall t. Functor t => t () = undefined
    let g :: forall u. Functor u => u () = a
    putStrLn "success"

не может

но 

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}

main = do
    let a :: forall t. Functor t => t () = undefined
    let g :: forall u. Functor u => u ()
        g = a
    putStrLn "success"

успешно.

...