如何将TypeApplications与typeclass方法一起使用，为什么GHCi会推断出我无法使用的类型？
概括
我有一个类型类，我想为其编写一些“通用术语”。我有两个问题：
- 使用
:t向 GHCi 询问通用术语的类型有效，但使用推断的类型失败 - 为什么？ - 如何使用
TypeApplications类型类的方法？
我正在使用GHC 8.8.4。对于这两个问题，我有以下示例，Main.hs其中包含一个类型类F和类型Empty，它是F.
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
module Main where
import GHC.Types (Type)
class F (f :: k -> Type) where
type Plus f (a :: k) (b :: k) :: k
zero :: f a
plus :: f a -> f b -> f (Plus f a b)
data Empty (a :: Type) = Empty
instance F Empty where
type Plus Empty a b = (a, b)
zero = Empty
plus _ _ = Empty
1. 推断类型不起作用？
我想构造一个 typeclass 的通用术语F。例如，plus zero zero。当我向 GHCi 询问这个术语的类型时，它给出了我的期望：
*Main> :t plus zero zero
plus zero zero :: F f => f (Plus f a b)
令人惊讶的是，如果我尝试分配该术语，则会出现错误。也就是说，如果我将以下内容添加到Main.hs：
-- This doesn't work.
plusZero :: F f => f (Plus f a b)
plusZero = plus zero zero
在 GHCi 中重新加载文件会报错：
• Couldn't match type ‘Plus f a0 b0’ with ‘Plus f a b’
Expected type: f (Plus f a b)
Actual type: f (Plus f a0 b0)
NB: ‘Plus’ is a non-injective type family
The type variables ‘a0’, ‘b0’ are ambiguous
• In the expression: plus zero zero
In an equation for ‘plusZero’: plusZero = plus zero zero
我的第一个问题是：为什么 GHCi 似乎可以推断类型，但在我明确注释该术语时拒绝它？
2. 使用TypeApplications代替注解
我可以通过注释zero术语类型来解决第一个问题：
-- This works
plusZero1 :: forall f a b . F f => f (Plus f a b)
plusZero1 = plus (zero :: f a) (zero :: f b)
但是，当术语变大时，这有点笨拙。我想做的是使用TypeApplications. 我试过这个：
-- This doesn't work
plusZero2 :: forall f a b . F f => f (Plus f a b)
plusZero2 = plus @f @a @b zero zero
但 GHci 抱怨：
• Expecting one more argument to ‘f’
Expected a type, but ‘f’ has kind ‘k -> *’
• In the type ‘f’
In the expression: plus @f @a @b zero zero
In an equation for ‘plusZero2’: plusZero2 = plus @f @a @b zero zero
• Relevant bindings include
plusZero2 :: f (Plus f a b) (bound at Main.hs:36:1)
奇怪的是，如果我首先定义附加功能plus'，zero'如下所示，一切都按预期进行：
zero' :: forall f a . F f => f a
zero' = zero
plus' :: forall f a b . F f => f a -> f b -> f (Plus f a b)
plus' = plus
-- This works fine
plusZero3 :: forall f a b . F f => f (Plus f a b)
plusZero3 = plus' @f @a @b zero' zero'
所以似乎我还没有理解TypeApplicationstypeclass 方法是如何工作的。如何使用一个类型的应用程序plus和zero无需定义附加功能plus'和zero'？
回答
- 推断类型不起作用？
在您的示例中，GHC 确实可以推断类型，但它不能接受您的签名。这可能看起来有悖常理，但如果您考虑一下总体情况，这确实是有道理的。
Plus f a b是一个非内射类型族。对于所有GHC知道，而类型检查，它可以被定义为Plus f a b = a所有的f，a和b。
假设我们已经定义了一个术语（forall为了清楚起见，我添加了s）
foo :: forall f a b. F f => f (Plus f a b)
我们写
bar :: forall f a b. F f => f (Plus f a b)
bar = foo
这不应该进行类型检查 (!)，因为它本质上是不明确的。作为人类的程序员可能希望编译器推断这些类型：
bar :: forall f a b. F f => f (Plus f a b)
bar = foo @f @a @b
但是，可能还有其他正确的推断类型！事实上，如果Plus定义如上所述，这也将类型检查：
bar :: forall f a b. F f => f (Plus f a b)
bar = foo @f @a @String
使用它，foo将产生f (Plus f a String)与 相同的f (Plus f a b)，所以一切类型检查。由于程序员可能打算使用除 之外的其他东西@b，我们在这里停止报告类型错误的歧义。
从技术上讲，推理过程中发生的事情是：对 poltmorphic 的调用foo链接到新的未知类型变量：
bar :: forall f a b. F f => f (Plus f a b)
bar = foo @xf @xa @xb
然后，统一发生：foo @xf @xa @xbisxf (Plus xf xa xb)和 this的类型与提供的签名统一以找到未知数：
xf (Plus xf xa xb) ~ f (Plus f a b)
从中我们应用了统一算法：
xf ~ f
Plus xf xa xb ~ Plus f a b
所以我们找到了 unknown 的类型xf，代入我们得到：
xf ~ f
Plus f xa xb ~ Plus f a b
然而，我们就此打住。我们无法推断xa ~ a，xb ~ b因为类型族不是单射的。
- 使用 TypeApplications 代替注解
问题是有一个隐藏的种类@k参数，因为它发生在类中。使用:t +v展示真实的类型与所有forallS：
> :t +v plus
plus
:: forall k (f :: k -> *) (a :: k) (b :: k).
F f =>
f a -> f b -> f (Plus f a b)
传递@k也有效：
plusZero2 :: forall k (f :: k -> Type) a b . F f => f (Plus f a b)
plusZero2 = plus @k @f @a @b zero zero
或者，让编译器推断@k：
plusZero2 :: forall f a b . F f => f (Plus f a b)
plusZero2 = plus @_ @f @a @b zero zero