`forall {..}` in GHC 9

Question

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

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

- Sridhar Ratnakumar

---

看起来这是一个无法使用ign @MyF @MyP应用的推断类型变量：https://downloads.haskell.org/ghc/latest/docs/html/users_guide/exts/type_applications.html?highlight=typeapplications#manually-defining-inferred-variables - chi

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（而不是召唤“蜗牛小队”：@_，嗯，“部分类型签名”），我们可以将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推导得出。您可能更喜欢在MkApply中将k标记为隐式的，这样您可以编写 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

- Iceland_jack

---

总的来说，我认为在可能的情况下应该推断出类型变量。这与默认相反，这是不幸的。例如，GHC.Generics.Generic1需要指定的类型参数，因此to1和from1也需要。这是可怕的用户体验。 - dfeuer

我同意这个观点，它阻止了我将Category类型多态化为指定的类型（type Category :: forall ob. Cat ob -> Constraint）。这将会改变方法中ob的量化方式从推断变为指定，因此你必须写成id @Type @(->) @Int :: Int -> Int。如果在kind中指定了{ob}，则无法在方法中指定其为推断类型。我不喜欢这种情况，在我添加Generically1时，我必须使用GADT语法，并量化Generically1 :: forall {k} f a. f a -> Generically1 @k f a构造函数中的所有变量。 - Iceland_jack

我不确定最佳默认值是什么，但没有办法覆盖方法！我不知道这是否已经改变；有一个关于顶级方法签名的提案，您可以编写 id :: forall {ob :: Type} (cat :: Cat ob) (a :: ob) :: Category @ob cat => cat a a。我不喜欢在类声明之外重复签名，但至少它允许微调！ - Iceland_jack

啊，现在我明白了。你想为类指定一个无法推断的类型参数，但又想避免将同样可推断的参数指定给方法。有道理。 - dfeuer

是的，可见性（在未来）可能会发生类似的事情。sizeOf :: forall a. Sizeable a => a -> Int 实际上并没有使用 a 参数，因此可以使用 sizeOf (undefined :: A) 来提供它。如果删除参数，则可以使用类型应用程序指定它 sizeOf :: forall a. Sizeable a => Int，但是使用可见量化更有意义：forall a -> Sizeable a => Int。但即使使用了 forall->，如何才能在方法上明确量化呢？类的类型参数已经在方法范围之外隐式量化了。我不知道。 - Iceland_jack