haskell - 关联类型族提示 `pred::T a -> Bool` ，其中 "NB: ‘T’ 是一个类型函数，并且可能不是单射的”

Question

这段代码:

{-# LANGUAGE TypeFamilies #-}

module Study where

class C a where
    type T a :: *
    pred :: T a -> Bool

— 出现此错误:

.../Study.hs:7:5: error:
    • Couldn't match type ‘T a’ with ‘T a0’
      Expected type: T a -> Bool
        Actual type: T a0 -> Bool
      NB: ‘T’ is a type function, and may not be injective
      The type variable ‘a0’ is ambiguous
    • In the ambiguity check for ‘Study.pred’
      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
      When checking the class method:
        Study.pred :: forall a. A a => T a -> Bool
      In the class declaration for ‘A’
  |
7 |     pred :: T a -> Bool
  |     ^^^^^^^^^^^^^^^^^^^

用 data 修复替换 type 关键字。

• 为什么一个是错误的，另一个是正确的？
• “可能不是单射的”是什么意思？如果连一对一都不允许那算什么功能？这与 pred 的类型有何关系？

Answer 1

instance C Int where
  type T Int = ()
  pred () = False

instance C Char where
  type T Char = ()
  pred () = True

现在你有 pred 的两个定义。因为类型族只是分配类型同义词，所以这两个定义具有签名

pred :: () -> Bool

和

pred :: () -> Bool

嗯，看起来很相似，不是吗？类型检查器无法区分它们。那么，什么是

pred ()

应该是？ True或False ？

要解决此问题，您需要某种明确的方式来提供特定 pred 的实例的信息。在某些用例中应该属于。正如您自己发现的那样，实现此目的的一种方法是更改​​为关联的 data家庭:data T Int = TInt和data T Char = TChar将是两种可区分的新类型，而不是类型的同义词，后者无法确保它们实际上不同。 IE。数据族总是单射的；类型的家庭有时不是。在没有其他提示的情况下，编译器假定没有类型族是单射的。

您可以使用另一种语言扩展来声明类型族单射:

{-# LANGUAGE TypeFamilyDependencies #-}
class C a where
  type T a = (r :: *) | r -> a
  pred :: T a -> a

=只需绑定(bind) r T的结果到一个名称，因此它在单射性注释的范围内，r -> a ，读起来像函数依赖: r T的结果足以确定a论点。上述情况现已违法； type T Int = ()和type T Char = ()一起违反单射性。仅允许一项。

或者，您可以按照编译器的提示进行操作； -XAllowAmbiguousTypes使原始代码编译。但是，您将需要 -XTypeApplications解析使用站点的实例:

pred @Int () == False
pred @Char () == True