类型系列的难以理解的错误消息

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在错误信息中所说,类型系列确实不需要是单射的.

注入意味着什么？

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 :: *

并使可逆性成为类型类的超类约束:

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,它可以应用超约束推断

S ~ UnUnit (Unit S) ~ UnUnit T

如果我们现在想尝试定义坏情况下的上面Object Int和Object Char这两个地图Unit Int和Unit Char这两个是Int,那就没办法了,因为我们不得不决定是否UnObject Int应该Int或Char,但不能兼得？