GHC 9 中的`forall {..}`

Question

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

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

Answer 1

参见6.4.14.1. Inferred vs. specified type variables:

Since the 9.0.1 release, GHC permits labelling the user-written type or kind variables as inferred, in contrast to the default of specified. By writing the type variable binder in braces as {tyvar} or {tyvar :: kind}, the new variable will be classified as inferred, not specified.

.. 是指定的类型
{..} 是一个 推断的 类型

forall a.和forall {a}.是GHC统一自动实例化的不可见量词

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

这意味着 const True EQ 实例化 a (@Bool) 和 b (@Ordering)没有用户的帮助。

如果用户想要显式实例化它们，他们可以使用可见类型应用程序“覆盖它们的可见性”。这就是为什么它们是 指定的 类型。（尽管“specifiable”可能是更准确的术语）

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

如果出于某种原因我们只想指定 b（不召唤“蜗牛小队”：@_，嗯“partial type signatures”）我们可以使 a 成为推断类型。然后丢弃第一种

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

您必须在实例化 MkApply @Type @[] @Int 时指定类型 k，但 [] 和 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

GHC 9 中的`forall {..}`

`forall {..}` in GHC 9

syntax

haskell

forall