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

Question

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

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

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

我也在使用 poly-kinded 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 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))'

当我试图插入编译器做它设计不做的事情时，任何对正在发生的事情的洞察都会有所帮助。

编辑 - 简化

基于来自 this answer 的观察，我们可以去掉 Chooses完全写

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

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

Answer 1

要了解实际情况，请查看 Chooses类(class)。特别注意，False 中的它不是懒惰的情况(即，当它不能立即确定它的值应该为真时):

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"