haskell - 关于非单射类型函数的简单类型族示例错误

Question

我试图理解类型家庭，但没有取得多大成功。这是一个最小的例子:

{-# LANGUAGE TypeFamilies #-}

class Object obj where
  type Unit obj :: *
  unit :: Unit obj

instance (Object obj, Object obj') => Object (obj, obj') where
  type Unit (obj, obj') = (Unit obj, Unit obj')
  unit = (unit, unit)

我认为意图是相当透明的(试图定义一个产品类别)。

这给了我:

objs.hs:10:10:
    Could not deduce (Unit obj' ~ Unit obj1)
    from the context (Object obj, Object obj')
      bound by the instance declaration at objs.hs:8:10-56
    NB: `Unit' is a type function, and may not be injective
    The type variable `obj1' is ambiguous
    Possible fix: add a type signature that fixes these type variable(s)
    Expected type: Unit (obj, obj')
      Actual type: (Unit obj0, Unit obj1)
    In the expression: (unit, unit)
    In an equation for `unit': unit = (unit, unit)
    In the instance declaration for `Object (obj, obj')'

我试图添加类型签名:

unit = (unit :: Unit obj, unit :: Unit obj') 

但这只会让事情变得更糟。

以下修改编译:

{-# LANGUAGE TypeFamilies #-}

class Object obj where
  type Unit obj :: *
  unit :: obj -> Unit obj

instance (Object obj, Object obj') => Object (obj, obj') where
  type Unit (obj, obj') = (Unit obj, Unit obj')
  unit (o, o') = (unit o, unit o')

但我不喜欢 unit 的多余论点.

是否可以定义无参数 unit ?

Answer 1

您尝试做的事情对于 GHC 来说很棘手，因为正如 GHC 在错误消息中所说，类型族确实不需要是单射的。

内射是什么意思？

A型函数F如果 F x ~ F y 则称为单射暗示 x ~ y .如果 F是一个普通类型的构造函数，通过 data 定义，那么这总是正确的。但是，对于类型族，它不成立。

例如，根据您对 Object 的定义，定义以下实例没有问题:

instance Object Int where
  type Unit Int = Int
  unit = 0

instance Object Char where
  type Unit Char = Int
  unit = 1

现在如果你写 unit :: Int ，那么 GHC 怎么可能确定它是否应该评估为 0或 1 ?甚至不写 unit :: Unit Int让它变得更加清晰，因为

Unit Int ~ Int ~ Unit Char

所以这三种类型都应该是可以互换的。如 Unit不保证是单射的，根本没有办法从 Unit x的知识中得出唯一的结论。知识 x ...

结果是 unit可以定义，但不能使用。

解决方案 1:虚拟或代理参数

您已经列出了解决此问题的最常用方法。添加一个参数，帮助 GHC 实际确定有问题的类型参数，方法是将类型签名更改为

unit :: obj -> Unit obj

或者

unit :: Proxy obj -> Unit obj

Proxy 的合适定义，例如简单地

data Proxy a

解决方案 2:手动证明可逆性

一个可能鲜为人知的选项是，您实际上可以向 GHC 证明您的类型函数是可逆的。

这样做的方法是定义一个逆类型族

type family UnUnit obj :: *

并使可逆性成为类型类的父类(super class)约束:

class (UnUnit (Unit obj) ~ obj) => Object obj where
  type Unit obj :: *
  unit :: Unit obj

现在你必须做额外的工作。对于类的每个实例，您必须定义 Unit 的实际倒数正确。例如，

instance (Object obj, Object obj') => Object (obj, obj') where
  type Unit (obj, obj') = (Unit obj, Unit obj')
  unit = (unit, unit)

type instance UnUnit (obj, obj') = (UnUnit obj, UnUnit obj')

但鉴于此修改，定义类型检查。现在，如果 GHC 遇到调用 unit在某些特定类型 T并想确定一个类型 S这样 Unit S ~ T ，它可以应用父类(super class)约束来推断

S ~ UnUnit (Unit S) ~ UnUnit T

如果我们现在尝试为 Object Int 定义上述错误实例和 Object Char这两个 map Unit Int和 Unit Char两者都是 Int ，这是行不通的，因为我们必须决定是否 UnObject Int应该是 Int或 Char ，但不能两者兼得……