5

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

首先，我使用了所有厨房水槽，除了OverlappingInstances.

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

我还使用了多Proxy类型和类型级别或:||:.

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 xor实例，就会为其定义一个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 xorA y实例。Bool（我们可以使用与for不同的类型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)

然后，就像高级重叠示例一样，我定义了一个与Aexcept 相同的类，为选项添加一个额外的类型变量，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)

4

1 回答 1

2

要了解实际情况，请查看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 统一。那么约束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)

现在你想“哦，不，我必须重写我所有的代码来使用类型族。” 情况并非如此，因为您始终可以将类型族“降低”到具有函数依赖关系的 Class 谓词：

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"
于 2014-12-13T01:21:19.397 回答