haskell - 说服编译器存在有效的实例链

Question

好的。这里的问题非常抽象。忍受我。

我有一堆“单位”，每个单位都有特定的属性。这些属性在 Seq 中定义类，像这样:

class Seq a x y where
    break :: x -> (a, y)
    build :: a -> y -> x

从概念上讲， a type 是重要的类型， x是用于生成 a 的上下文, 和 y是用于生成任何进一步的上下文 Seq实例。 break打破 Seq下来， build允许您重建它。

关于个人 Seq实例，这工作正常。但是，我还有一个如下所示的数据构造函数:

data a :/: b = a :/: b deriving (Eq, Ord)
infixr :/:

这整个操作的目标是能够编写 Seq实例。

例如，如果我有 a , b , 和 c Seq 的所有实例使得 a的上下文馈入 b和 b的馈入 c ，那么我应该自动有一个 Seq a :/: b :/: c 的实例.通过递归数据类型进行设置的类非常简单:

instance (Seq a x y, Seq b y z) => Seq (a :/: b) x z where
    break x = let
        (a, y) = break x :: (a, y)
        (b, z) = break y :: (b, z)
        in (a :/: b, z)

    build (a :/: b) z = let
        y = build b z :: y
        x = build a y :: x
        in x

问题是我似乎无法使用它。如果我定义以下三个 Seq实例:

data Foo
instance Seq Foo Integer Bool

data Bar
instance Seq Bar Bool Bar

data Baz
instance Seq Baz Bar ()

(编辑了实现细节，更多信息见 here)

和一个类型良好的 break功能:

myBreak :: Integer -> (Foo :/: Bar :/: Baz)
myBreak = fst . break' where
    break' = break :: Integer -> (Foo :/: Bar :/: Baz, ())

然后我什至无法编译:

No instances for (Seq Foo Integer y, Seq Bar y y1, Seq Baz y1 ())
  arising from a use of `break'
Possible fix:
  add instance declarations for
  (Seq Foo Integer y, Seq Bar y y1, Seq Baz y1 ())
In the expression: break :: Integer -> (Foo :/: (Bar :/: Baz), ())
In an equation for break':
    break' = break :: Integer -> (Foo :/: (Bar :/: Baz), ())
In an equation for `myBreak':
    myBreak
      = fst . break'
      where
          break' = break :: Integer -> (Foo :/: (Bar :/: Baz), ())

它看起来像 myBreak无法确定 Foo → Bar → Baz 中是否存在上下文的“工作线程”。我如何说服编译器这是类型良好的？

这是我第一次接触类型编程，所以我无疑打破了一些既定的规则。我很好奇我在这里做错了什么，但我也愿意接受关于如何更好地实现我的目标的建议。

Answer 1

您可能需要另一种或两种语言扩展来完成这项工作。一般问题是多参数类型类需要对开放世界假设进行编码，因此，假设有人出现并添加

instance Seq Bar Integer Float

instance Seq Baz Float ()

编译器无法知道要使用哪一组实例。这可能会导致未定义的行为。如果编译器只是“发现”没有其他实例可用，那么您一定是指这些实例，那么您将处于尴尬的境地，因为有人添加了一个实例，代码可能会中断。

解决方案是使用某种类型级别的函数。所以，如果 a是重要的类型，那么也许只有一种组合 x和 y随之而来的 a .一种方法是使用 functional dependencies .

class Seq a x y | a -> x, a -> y where
   break :: x -> (a, y)
   build :: a -> y -> x

函数依赖相当普遍，可以使用两个编码双射类型函数

class Seq a x y | a -> x, a -> y, x y -> a where
   break :: x -> (a, y)
   build :: a -> y -> x

这取决于您想要的语义到底是什么。或者，您可以使用 type families 使用稍微优雅的“关联类型同义词”方法。延期。

class Seq a where
   type X a
   type Y a
   break :: X a -> (a, Y a)
   build :: a -> Y a -> X a

instance Seq Bar where
   type X Bar = Bool 
   type Y Bar = Bar

这个版本目前被认为是最惯用的，并且比功能依赖版本有一些优势(尽管你不能用这种方式编码双射)。为了完整起见，这相当于

type family X a
type instance X Bar = Bool

type family Y a
type instance Y Bar = Bar

class Seq a where
   break :: X a -> (a, Y a)
   build :: a -> Y a -> X a

instance Seq Bar

编辑:具有多参数类型类的 Haskell 约束求解机制是一种逻辑语言，有点像 prolog。你应该尽可能多地使用 功能 而不是类型级编程时的关系。三个原因:

您可以从函数到约束，但反之则不行

Haskell 不是序言。大多数 Haskell 程序员发现函数更容易推理。如果您不了解 Prolog(或其他逻辑语言)，那么坚持使用函数尤为重要，因为关系编程和函数式编程之间的差异几乎与函数式编程和命令式编程之间的差异一样大。

尽管有相似之处，但 Haskell 的约束求解器不是 Prolog(直觉上所有子句在头部后面都有一个切割，如果你不知道这意味着什么，不要担心)。关系类型编程比用完全回溯的语言编码要困难得多。

我的建议是了解函数依赖和 type职能。类型函数更适合语言的其余部分，但有时函数依赖是完成这项工作的最佳工具。