4

在原始代码中可以看到我只是将一个表达式提取到一个绑定中，这是 haskell 声称应该始终可能的基本内容之一。

最小案例（在 freenode 上 @dminuoso 的帮助下创建）

我想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

4 回答 4

1

关于模式类型签名的文档的相关位是：

与表达式和声明类型签名不同，模式类型签名不是隐式概括的。

因此，就像您所写的那样，模式签名是一种特殊情况，其中泛化（t即将提到范围外类型变量的单a态类型转换为多态类型的forall a. t过程）没有完成。您可以使用任何其他形式的类型签名来恢复泛化过程；例如，而不是

let foo :: forall a. a = undefined

尝试：

let foo :: forall a. a
    foo = undefined
于 2019-01-21T18:03:10.657 回答
1

第1部分

好的

当你写作时会发生什么

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

? 具体来说，GHC 正在寻找什么类型的表达式来填补空缺（_）？您可能认为它正在寻找 a forall f. Functor f => f ()，但这并不完全正确。相反，a它实际上更像一个函数，并且 GHC 隐式插入了两个参数：一个f以 kind命名的类型参数* -> *和一个约束实例Functor f（与所有实例一样，它是未命名的）。

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

GHC 正在寻找，在 . 这与在 的上下文中查找 a和查找 a之间的区别相同。如果我直接有，在第一种情况下我可以只写，但在第二种情况下，我必须写出。type f :: * -> *; instance Functor ff ()(A -> B) -> C -> DD f :: A -> B; c :: Csolution :: (A -> B) -> C -> Dsolutionsolution f c

坏的

这不是你写的时候发生的事情

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

因为您使用了模式类型签名，而不是普通类型签名，所以 GHC 不再为您隐式绑定类型变量和实例。GHC 现在，老实说，希望你_用forall f. Functor f => f (). 这很难，我们很快就会看到...

（我真的不认为丹尼尔瓦格纳引用的东西在这里是相关的。我相信它只是指隐含意味着的方式和不意味着的方式之间的差异（何时ScopedTypeVariables开启type a且不在范围内）。）5 :: Num a => a5 :: forall a. Num a => ag :: a -> a = id g :: forall a. a -> a = id

第2部分

当你写作时会发生什么

undefined

? 具体来说，它的类型是什么？你可能认为它是forall a. a，但这并不完全正确。是的，的确，all by itselfundefined有 type ，forall a. a但是 GHC 不允许你自己写undefined。相反，表达式中的每次出现undefined总是应用于类型参数。上面的内容被隐式改写为

undefined @_a0

并创建了一个新的统一变量（实际上没有名称）_a0。这个表达式有类型_a0。如果我在需要 , then 的上下文中使用此表达式Int，则_a0必须等于Int，并且 GHC 设置_a0 := Int，将表达式重写为

undefined @Int

（因为_a0可以设置什么，所以称为统一变量。它在“我们的”，内部控制之下。上面，f 不能设置为任何东西。它是一个给定的，它在“他们的”（用户的），外部控制之下，这使它成为一个 skolem 变量。）

第 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

，你让一些非常奇怪的事情发生。正如我之前所说，带有 a 的模式类型签名forall不会引入任何东西。RHS 上的undefined实际需要是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 ()). 通常，这是一个禁忌，因为这是暗示性多态性：将类型变量设置为包含foralls 的类型。但是，在足够过时的 GHC 中，某些功能允许这样做。也就是说，undefined不是用 type 定义的forall (a :: *). a，而是forall (a :: OpenKind). a， whereOpenKind允许这种不可预测性。这意味着您的代码通过

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

如果你写

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

，它不起作用，因为bot没有相同的魔法酱undefined。此外，这在最近的 GHC 中不起作用，这些 GHC 已经消除了这种奇怪的暗示性多态性。（我说这是一件非常好的事情）。

坏的

您对 的定义a，即使使用模式签名，也确实得出了所需的 type 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 现在有 type _f0 ()，而 LHS 希望它有 type forall f. Functor f => f ()。这些看起来不一样。因此，键入错误。

由于您不能停止对a类型变量的隐式应用而只是编写g = a，因此您必须改为允许类型变量的隐式绑定g：

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

这行得通。

于 2019-01-21T22:43:19.037 回答
1

正如freenode上的@Lears指出的那样，将类型声明放在声明之上可以修复它，因此它可能是GHC中的某种错误。IE

{-# 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"

成功。

于 2019-01-21T16:27:58.153 回答
-1

如果我输入一个输入孔，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可能您正在尝试的内容尚不可能。

于 2019-01-21T16:33:14.173 回答