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

Question

行.这里的问题非常抽象.忍受我.

我有一堆"单位",每个单位都有一定的属性.这些属性在Seq类中定义,如下所示:

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

从概念上讲,a类型是重要类型,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 ()

(实施细节编辑,详见此处)

和一个良好的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.一种方法是使用功能依赖.

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

这取决于你想要的语义究竟是什么.或者,您可以使用类型族扩展来使用稍微更优雅的"关联类型同义词"方法.

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.在类型级编程时,您应尽可能使用函数而不是关系.三个原因:

1. 您可以从函数到约束,但反之亦然
2. Haskell不是序幕.大多数Haskell程序员发现函数更容易推理.如果您不了解Prolog(或其他逻辑语言),那么坚持功能是非常重要的,因为关系和函数编程之间的差异几乎与功能和命令式编程之间的差异一样大.
3. 尽管有相似之处,但Haskell的约束求解器并不是Prolog(直觉上所有的子句都会在头部之后立即切换,如果您不知道这意味着什么,请不要担心).关系类型编程比使用完全回溯的语言编码要困难得多.

我的建议是了解功能依赖和type功能.类型函数与语言的其余部分相比更好一些,但有时功能依赖性是工作的最佳工具.