问题描述
总结
我有一个类型类,我想为其编写一些“通用术语”。我有两个问题:
- 使用
: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。推断类型不起作用?
我想构造一个类型类 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'
所以我似乎还没有理解 TypeApplications
是如何与类型类方法一起工作的。
如何在无需定义附加函数 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
之外的其他内容,因此我们在此报告类型错误的歧义。
从技术上讲,在推理过程中发生的事情是:对多态 foo
的调用链接到新的未知类型变量:
bar :: forall f a b. F f => f (Plus f a b)
bar = foo @xf @xa @xb
然后,统一发生:foo @xf @xa @xb
的类型是 xf (Plus xf xa xb)
,这与提供的签名统一以找到未知数:
xf (Plus xf xa xb) ~ f (Plus f a b)
由此我们应用了统一算法:
xf ~ f
Plus xf xa xb ~ Plus f a b
所以我们找到未知 xf
的类型,并代入我们得到:
xf ~ f
Plus f xa xb ~ Plus f a b
然而,我们到此为止。我们无法推断 xa ~ a
和 xb ~ b
,因为类型系列不是单射的。
- 使用 TypeApplications 而不是注解
问题是有一个隐藏的 @k
参数,因为它发生在类中。使用 :t +v
显示带有所有 forall
的真实类型:
> :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