`forall {..}` in GHC 9

Question

这是GHC 9中的有效语法。{..}是什么意思(与 GHC 8.10 在此要求的(..)不同)？

ign :: forall {f :: Type -> Type} {p}. Applicative f => p -> f ()
ign _ = pure ()

Answer 1

参见6.4.14.1。推断类型变量与指定类型变量：

从 9.0.1 版本开始，GHC 允许将用户编写的类型或种类变量标记为推断，而不是指定的默认值。通过将类型变量绑定器写在大括号中作为{tyvar}或{tyvar :: kind}，新变量将被分类为推断变量，而不是指定。

• ..是指定的类型
• {..}是推断类型

forall a.和forall {a}.是不可见的量词，GHC 将通过统一自动实例化它们。

const :: forall a b. a -> b -> a
const a _ = a

这意味着const True EQ实例化a(@Bool)和b(@Ordering)，而无需用户帮助。

如果用户想要显式实例化它们，则可以使用可见类型应用程序"覆盖其可见性"。这就是它们是指定类型的原因。(尽管">指定">可能是一个更准确的术语)

>> :set -XTypeApplications
>> :t const @Bool @Ordering True EQ
const @Bool @Ordering True EQ :: Bool

如果出于某种原因我们只想指定b(不召唤"蜗牛小队"：@_，嗯"部分类型签名")，我们可以创建一个推断类型。然后删除第一个类型

const2 :: forall {a} b. a -> b -> a
const2 a _ = a
>> :t const2 @Ordering True EQ
const2 @Ordering True EQ :: Bool

对于您的示例，这意味着 ghc 必须推断f和p的类型。你不能写ign @IO @Int.

---

当你有善良的多态性时，这变得更加有用。如果定义

-- MkApply @Type @[] @Int :: [Int] -> Apply @Type [] Int
-- MkApply @_    @[] @Int :: [Int] -> Apply @Type [] Int
type    Apply :: forall (k :: Type). (k -> Type) -> (k -> Type)
newtype Apply f a where
MkApply :: forall (k :: Type) (f :: k -> Type) (a :: k). f a -> Apply @k f a

实例化时必须指定种类kMkApply @Type @[] @Int但这种类型由[]和Int隐含。您可能更喜欢将k标记为在MkApply中推断出来，这样您就可以编写MkApply @[] @Int

-- MkApply @[] @Int :: [Int] -> Apply @Type [] Int
type    Apply :: forall (k :: Type). (k -> Type) -> (k -> Type)
newtype Apply f a where
MkApply :: forall {k :: Type} (f :: k -> Type) (a :: k). f a -> Apply @k f a