尝试写回退实例时重叠实例错误

Question

我正在尝试做类似于高级重叠技巧的事情来定义具有重叠行为的实例.我正在尝试为元组派生一个实例,fst如果存在,将使用该snd字段的实例,否则使用该字段的实例(如果存在).这最终导致关于重叠实例的看似错误的错误.

首先,我正在使用所有的厨房水槽,除了OverlappingInstances.

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}

我也使用poly-kinded Proxy和type level或者:||:.

import Data.Proxy

type family (:||:) (a :: Bool) (b :: Bool) :: Bool
type instance (:||:) False a = a
type instance (:||:) True a = True

A是一个非常简单的课程.ThingA有一个A例子; ThingB没有.

class A x where
    traceA :: x -> String

data ThingA = ThingA
data ThingB = ThingB

instance A ThingA where
    traceA = const "ThingA"

下一部分的目标是编写一个A实例,(x, y)只要有一个A x或一个实例,就会定义一个A y实例.如果有一个A x实例,它将返回("fst " ++) . traceA . fst.如果没有一个A x实例,但有一种B x情况下它会返回("snd " ++) . traceA . fst.

第一步是创建一个函数依赖项,A通过匹配实例头来测试是否存在实例.这是高级重叠文章的普通方法.

class APred (flag :: Bool) x | x -> flag

instance APred 'True ThingA
instance (flag ~ 'False) => APred flag x

如果我们能够确定x以及y都有A的情况下,我们可以判断,如果(x, y)都将有一个.

instance (APred xflag x, APred yflag y, t ~ (xflag :||: yflag)) => APred t (x, y)

现在,我将脱离高级重叠中的简单示例,并引入第二个函数依赖项来选择是否使用A x或A y实例.(我们可以使用不同类型的比Bool对Chooses,并SwitchA避免混淆APred.)

class Chooses (flag :: Bool) x | x -> flag

如果有一个A x实例我们将永远选择'True,否则'False.

instance (APred 'True x) => Chooses 'True (x, y) 
instance (flag ~ 'False) => Chooses flag (x, y)

然后,像高级重叠示例一样,我定义了一个相同的类,A除了为选择提供额外的类型变量,Proxy为每个成员定义一个参数.

class SwitchA (flag :: Bool) x where
    switchA :: Proxy flag -> x -> String

这很容易定义实例

instance (A x) => SwitchA 'True (x, y) where
    switchA _ = ("fst " ++) . traceA . fst

instance (A y) => SwitchA 'False (x, y) where
    switchA _ = ("snd " ++) . traceA . snd

最后,如果存在SwitchA相同类型(x, y) Chooses的A (x, y)实例,我们可以定义一个实例.

instance (Chooses flag (x, y), SwitchA flag (x, y)) => A (x, y) where
    traceA = switchA (Proxy :: Proxy flag)

到这里的一切都汇集得很漂亮.但是,如果我尝试添加

traceA (ThingA, ThingB)

我收到以下错误.

    Overlapping instances for Chooses 'True (ThingA, ThingB)
      arising from a use of `traceA'
    Matching instances:
      instance APred 'True x => Chooses 'True (x, y)
        -- Defined at defaultOverlap.hs:46:10
      instance flag ~ 'False => Chooses flag (x, y)
        -- Defined at defaultOverlap.hs:47:10
    In the first argument of `print', namely
      `(traceA (ThingA, ThingA))'

这里发生了什么？为什么在查找实例时这些实例会重叠Chooses 'True ...; instance flag ~ 'False => Chooses flag ...当flag已知的情况下,实例不应该匹配'True吗？

相反,如果我尝试

traceA (ThingB, ThingA)

我收到了错误

    No instance for (A ThingB) arising from a use of `traceA'
    In the first argument of `print', namely
      `(traceA (ThingB, ThingA))'

当我试图推动编译器执行它不设计的操作时,对任何事情的了解都会有所帮助.

编辑 - 简化

根据这个答案的观察,我们可以Chooses完全摆脱并写出来

instance (APred choice x, SwitchA choice (x, y)) => A (x, y) where
    traceA = switchA (Proxy :: Proxy choice)

这解决了问题 traceA (ThingB, ThingA)

Answer 1

要了解到底发生了什么，请查看班级Chooses。具体来说，请注意它在这种情况下并不懒惰False（即，当它无法立即确定它应该具有值 true 时）：

chooses :: Chooses b x =>  x -> Proxy b 
chooses _ = Proxy

>:t chooses (ThingA, ())
chooses (ThingA, ()) :: Proxy 'True
>:t chooses (ThingB, ())

<interactive>:1:1: Warning:
    Couldn't match type 'True with 'False
    In the expression: chooses (ThingB, ())

它不懒惰的原因并不那么简单。最具体的例子就是

instance (APred 'True x) => Chooses 'True (x, y)

首先尝试。要验证是否如此，编译器必须检查APred. 在这里，instance APred 'True ThingA不匹配，因为你有ThingB. 因此它会进入第二个实例并flag与 False 统一（在 Chooses 中）。那么约束就APred 'True x不能成立！所以类型检查失败。您得到的类型错误有点奇怪，但我认为这是因为您没有启用 OverlappingInstances。当我用你的代码打开它时，我得到以下信息：

>traceA (ThingA, ThingA)
"fst ThingA"
>traceA (ThingB, ThingA)

<interactive>:43:1:
    Couldn't match type 'True with 'False
    In the expression: traceA (ThingB, ThingA)
    In an equation for `it': it = traceA (ThingB, ThingA)

正如预期的那样 - True 和 False 类型无法统一。

修复方法非常简单。将您的类转换为类型函数。类型函数本质上是等价的，但“更懒惰”。这是非常手波状的 - 抱歉我没有更好的解释为什么它有效。

type family APred' x :: Bool where 
  APred' ThingA = True
  APred' x = False 

type family Chooses' x :: Bool where 
  Chooses' (x, y) = APred' x 

instance (Chooses' (x,y) ~ flag, SwitchA flag (x, y)) => A (x, y) where
    traceA = switchA (Proxy :: Proxy flag)

现在您会想“哦，不，我必须重写所有代码才能使用类型系列。” 事实并非如此，因为您始终可以将类型族“降低”为具有函数依赖性的类谓词：

instance Chooses' x ~ b => Chooses b x 

现在您的原始实例instance (Chooses flag (x, y), SwitchA flag (x, y)) => A (x, y) where ...将按预期工作。

>traceA (ThingA, ThingA)
"fst ThingA"
>traceA (ThingB, ThingA)
"snd ThingA"