关于非单射类型函数的简单类型族示例错误 [英] Simple type family example errors about non injective type function

问题描述

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

I'm trying to understand type families without much success. Here's a minimal example:

{-# 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)

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

The intent is fairly transparent I think (trying to define a product category).

这给了我:

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') 

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

but this only makes things worse.

以下修改编译:

{-# 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 的多余参数.

but I don't like the superfluous argument for unit.

是否可以定义无参数的unit?

Is it possible to define the argument-less unit?

推荐答案

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

What you're trying to do is tricky for GHC, because as GHC says in the error message, type families do indeed not need to be injective.

>

注入性是什么意思?

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

A type function F is called injective if F x ~ F y implies x ~ y. If F is a normal type constructor, defined via data, then this is always true. For type families, however, it does not hold.

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

For example, there's no problem in defining the following instances, given your definition of 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 就更清楚了，因为

Now if you write unit :: Int, then how could GHC possibly determine if it should evaluate to 0 or 1? Not even writing unit :: Unit Int makes it really more clear, because

Unit Int ~ Int ~ Unit Char

所以这三种类型都应该是可以互换的.由于 Unit 不能保证是单射的，所以根本无法从 Unit x 的知识中唯一地得出 x 的知识..

so all three types are supposed to be interchangeable. As Unit isn't guaranteed to be injective, there's simply no way to uniquely conclude from the knowledge of Unit x the knowledge of x ...

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

The consequence is that unit can be defined, but not used.

您已经列出了解决此问题的最常用方法.添加一个参数，通过将类型签名更改为

You have listed the most common way of fixing this problem already. Add an argument that helps GHC to actually determine the type argument in question, by changing the type signature to

unit :: obj -> Unit obj

或

unit :: Proxy obj -> Unit obj

对于Proxy的合适定义，例如简单的

for a suitable definition of Proxy, for example simply

data Proxy a

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

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

Solution 2: Manually proving invertibility

A perhaps lesser known option is that you can actually prove to GHC that your type function is invertible.

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

The way to do that is to define an inverse type family

type family UnUnit obj :: *

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

and make the invertibility a superclass constraint of the type class:

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

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

Now you have to do extra work. For every instance of the class, you have to define the actual inverse of Unit correctly. For example,

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 在某个特定类型 T 上遇到 unit 调用，并且想要确定一个类型 S 使得 Unit S ~ T，它可以应用超类约束来推断

But given this modification, the definition typechecks. Now if GHC encounters a call the unit at some specific type T and wants to determine a type S such that Unit S ~ T, it can apply the superclass constraint to infer that

S ~ UnUnit (Unit S) ~ UnUnit T

如果我们现在尝试为 Object Int 和 Object Char 定义坏实例，它们都映射 Unit Int 和 >Unit Char 都为 Int，那是行不通的，因为我们必须决定 UnObject Int 是否应该是 Int 或 Char，但不能同时具有 ...

If we'd now try to define bad instances as above for Object Int and Object Char which both map Unit Int and Unit Char to both be Int, that wouldn't work, because we'd have to decide whether UnObject Int should be Int or Char, but couldn't have both ...

这篇关于关于非单射类型函数的简单类型族示例错误的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！