有关非内射型函数的简单类型族示例错误

本文介绍了有关非内射型函数的简单类型族示例错误的处理方法，对大家解决问题具有一定的参考价值，需要的朋友们下面随着小编来一起学习吧！

问题描述

我试图了解类型家庭，但没有太大的成功.这是一个最小的示例:

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?

注入性是什么意思?

如果F x ~ F y暗示x ~ y，则将类型函数F称为内射式.如果F是通过data定义的普通类型构造函数，则始终为true.但是，对于类型家族，它不成立.

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 definethe 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 ...

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

determine