Haskell如何解决重叠实例

Question

如果我使用错误的术语，请原谅我是Haskell类型操作的初学者...我试图使用具有功能依赖性的重叠实例来执行某些类型级别的编程与hlists。

在这里我的目标是尝试编写类型HNoNils l l'，其中HNoNils l l'表示，对于l是列表类型（例如：Int : String : EmptyNil : Int : HNil），l'是相应的列表类型，没有特定的空类型EmptyNil（示例的结果：Int:String:Int:HNil的结果：CC_7）：

{-# LANGUAGE ExistentialQuantification,
  FunctionalDependencies,
  FlexibleInstances,
  UndecidableInstances,
  OverlappingInstances,
  TypeFamilies #-}
import Data.HList 
import Data.TypeLevel.Bool
--Type Equality operators
--usedto check if a type is equal to another
class TtEq a b eq | a b -> eq
instance     TtEq a a True
instance eq~False => TtEq a b eq 

data EmptyNil = EmptyNil deriving (Show) --class representing empty channel
--class intended to generate a list type with no type of EmptyNil
-- Example: HCons Int $ HCons EmptyNil HNil should give HCons Int HNil
class (HList list, HList out) => HNoNils list out | list -> out 
    where  hNoNils :: list -> out 
-- l gives l' means (HCons EmptyNil l) gives l'
instance (HNoNils l l',TtEq e EmptyNil True ) => HNoNils (HCons e l) l'
    where hNoNils (HCons e l) = hNoNils l
-- l gives l' means (HCons e l) gives (HCons e l') for all e 
instance (HNoNils l l') => HNoNils (HCons e l) (HCons e l')
    where hNoNils (HCons e l) = hCons e $ hNoNils l
--base case
instance  HNoNils HNil HNil
    where hNoNils _ = hNil
testList  = HCons EmptyNil $ HCons EmptyNil HNil
testList1 = HCons "Hello"  $ HCons EmptyNil HNil 
testList2 = HCons EmptyNil $ HCons "World"  HNil
testList3 = HCons "Hello"  $ HCons "World"  HNil
main:: IO ()
main = do
    print $ hNoNils testList  -- should get HNil
    print $ hNoNils testList1 -- should get HCons "Hello" HNil
    print $ hNoNils testList2 -- should get HCons "World" HNil
    print $ hNoNils testList3 -- should get HCons "Hello" (HCons "World" HNil)

但是，当我运行此代码时，我所有的hNoNils调用似乎都可以通过最少特定的，第二个，实例声明，含义（至少似乎是）解决，即对于所有l，我都有HNoNils l l。p>基于我所阅读的内容，随着OverlappingInstances扩展，该系统应该始终解析为最特定的实例。

在这里

• 第一个实例具有约束(HNoNils l l',TtEq e EmptyNil True )

• 第二个实例具有约束HNoNils l l'

如果我错了，请原谅我，但似乎第一个实例比第二个更具体，所以应该这样做，对吗？

我尝试添加约束来尝试摆脱重叠，即通过将单独的，oposite的平等约束添加到第二个实例中：

-- l gives l' means (HCons EmptyNil l) gives l'
instance (HNoNils l l',TtEq e EmptyNil True ) => HNoNils (HCons e l) l'
    where hNoNils (HCons e l) = hNoNils l
-- l gives l' means (HCons e l) gives (HCons e l') for all e 
-- added constraint of TtEq e EmptyNil False
instance (HNoNils l l',TtEq e EmptyNil False) => HNoNils (HCons e l) (HCons e l')
    where hNoNils (HCons e l) = hCons e $ hNoNils l

我尝试在此处删除重叠的实例扩展名，并且我遇到了重叠错误。

Overlapping instances for HNoNils
                                (HCons EmptyNil (HCons [Char] HNil)) (HCons EmptyNil l')
Matching instances:
      instance (HNoNils l l', TtEq e EmptyNil True) =>
               HNoNils (HCons e l) l'
        -- Defined at /home/raphael/Dropbox/IST/AFRP/arrow.hs:32:10
      instance (HNoNils l l', TtEq e EmptyNil False) =>
               HNoNils (HCons e l) (HCons e l')
        -- Defined at /home/raphael/Dropbox/IST/AFRP/arrow.hs:36:10

我不明白第二场比赛。毕竟，在该决议中，我们的E等于emptynil，所以TtEq e EmptyNil True ...对吗？为此，类型系统如何甚至到达提出这个问题的情况，毕竟您永远不应该有 HNoNils (Hcons EmptyNil l) (HCons EmptyNil l'))的情况，至少我不这么认为。

添加返回重叠的词，我甚至会得到我不明白的怪异错误：

 Couldn't match type `True' with `False'
    When using functional dependencies to combine
      TtEq a a True,
        arising from the dependency `a b -> eq'
        in the instance declaration at /home/raphael/Dropbox/IST/AFRP/arrow.hs:23:14
      TtEq EmptyNil EmptyNil False,
        arising from a use of `hNoNils'
        at /home/raphael/Dropbox/IST/AFRP/arrow.hs:53:13-19
    In the second argument of `($)', namely `hNoNils testList2'
    In a stmt of a 'do' block: print $ hNoNils testList2

第二个语句TtEq EmptyNil EmptyNil False似乎说一个实例是由函数调用生成的...？我对它的来源有些困惑。

因此，在试图弄清楚这一点时，我想知道：

• 是否可以获取有关Haskell如何使用实例的更多详细信息？其中一些组合似乎不可能。即使只是指向解释机制的文档的链接也将不胜感激

• OverlappingInstances的工作方式有更具体的定义吗？我觉得我缺少某些东西（例如，"特殊性"参数仅适用于j the类型变量，而不是约束的数量...）

编辑：所以我尝试了C.A.的建议之一。McCann（删除一些约束）对以下内容：

instance (HNoNils l l') => HNoNils (HCons EmptyNil l) l'
instance (HNoNils l l') => HNoNils (HCons e l) (HCons e l')
instance  HNoNils HNil HNil

这样做给我一些令人讨厌的重叠实例错误：

Overlapping instances for HNoNils
                                (HCons EmptyNil (HCons [Char] HNil)) (HCons EmptyNil l')
      arising from a use of `hNoNils'
    Matching instances:
      instance [overlap ok] HNoNils l l' => HNoNils (HCons EmptyNil l) l'
        -- Defined at /Users/raphael/Dropbox/IST/AFRP/arrow.hs:33:10
      instance [overlap ok] HNoNils l l' =>
                            HNoNils (HCons e l) (HCons e l')
        -- Defined at /Users/raphael/Dropbox/IST/AFRP/arrow.hs:37:10

我觉得分辨率方法是自上而下的，而不是自下而上（系统永远不会尝试找到这样的实例）。

编辑2 ：通过在第二个条件中添加一个小的约束，我得到了预期的行为（请参阅McCann对他的答案的评论）：

-- l gives l' means (HCons EmptyNil l) gives l'
instance (HNoNils l l') => HNoNils (HCons EmptyNil l) l'
    where hNoNils (HCons EmptyNil l) = hNoNils l
-- l gives l' means (HCons e l) gives (HCons e l') for all e 
instance (HNoNils l l',r~ HCons e l' ) => HNoNils (HCons e l) r
    where hNoNils (HCons e l) = hCons e $ hNoNils l

这里添加的内容是第二个实例上的r~HCons e l'约束。

Answer 1

是否可以获取有关Haskell如何使用实例的更多详细信息？其中一些组合似乎不可能。即使只是指向解释该机制的文档的链接也将不胜感激

haskell 与实例一起工作非常简单。您正在处理GHC提供的多种实验语言扩展，因此信息的主要来源是GHC用户指南。

对重叠的工作方式有更具体的定义吗？我觉得我缺少某些东西（例如，"特殊性"参数仅适用于j the类型变量，而不是与约束的数量一起工作...）

您的猜测是正确的。从用户指南部分说明OverlappingInstances：

当GHC试图解决约束C Int Bool时，它试图通过实例化实例声明的头部来匹配每个实例声明与约束。例如，考虑以下声明：

instance context1 => C Int a     where ...  -- (A)
instance context2 => C a   Bool  where ...  -- (B)
instance context3 => C Int [a]   where ...  -- (C)
instance context4 => C Int [Int] where ...  -- (D)

实例（a）和（b）匹配约束C Int Bool，但是（c）和（d）不。匹配时，GHC不考虑实例声明的上下文（context1等）。

将其视为类似模式与警卫的东西：

instanceOfC Int a | context1 Int a = ...
instanceOfC a Bool | context2 a Bool = ...

由于类型类是"打开"的，因此没有明确定义的匹配顺序，这就是为什么对"模式"匹配相同参数的限制的原因。我进一步阐述了先前答案中与模式和警卫的类比。

如果我们通过上述类比将您的实例转化为伪功能，则结果是这样：

hNoNils (e:l) | e == EmptyNil = hNoNils l
hNoNils (e:l) = e : hNoNils l
hNoNils [] = []

知道"守卫"在选择"模式"时被忽略，很明显，前两个模式无法区分。

---

，但我希望您想知道如何使事情起作用，而不仅仅是为什么他们当前不行。（N.B.-我现在没有GHC，所以这全是从内存中进行的，没有经过测试。我可能遇到了一些细节。）

有几种处理这种事情的方法。最通用的是在通用实例的上下文中首先使用类型函数的两步过程，然后将其延迟到辅助类的特定实例，该实例接受了额外的参数：

class FooConstraint a b r | a b -> r  -- some sort of type predicate

-- the "actual" type function we want
class (FooConstraint a b result, FooAux a b result c) => Foo a b c | a b -> c
-- a single maximally generic instance
instance (FooConstraint a b result, FooAux a b result c) => Foo a b c 

-- this class receives the original a and b as arguments, but also the 
-- output of the predicate FooConstraint
class FooAux a b result c | a b result -> c
-- which lets us indirectly choose instances based on a constraint
instance ( ... ) => FooAux a b True c 
-- more instances, &c.

您可以看到这是一个巨大的麻烦，但有时就是您所拥有的。

幸运的是，您的情况要容易得多。回想一下上面的伪功能的翻译 - 您实际上是这样写的吗？当然不是，因为这样会更清楚：

hNoNils (EmptyNil:l) = hNoNils l
hNoNils (e:l) = e : hNoNils l
hNoNils [] = []

由于EmptyNil是一个构造函数，您可以在其上进行模式匹配，简化代码并避免了多余的Eq约束。

同样适用于类型级别的等价：替换类型等于谓词，仅在实例头中使用EmptyNil：

instance (HNoNils l l') => HNoNils (HCons EmptyNil l) l'
instance (HNoNils l l') => HNoNils (HCons e l) (HCons e l')
instance  HNoNils HNil HNil

这个版本仍然会在一种情况下失败，这确实没有好的方法。如果类型列表包含可能与EmptyNil统一的类型变量 - 请记住，此时忽略了约束，并且GHC必须考虑稍后为EmptyNil添加任意实例，那么前两个实例不可避免地是模棱两可的。

可以通过确保可以区分所有相关案例来部分避免这种最后类型的歧义问题。例如，您可以使用类型的构造函数，例如：

data Some a
data None

然后编写catMaybes的类型级版本：

class CatOptions l l'
instance (CatOptions l l') => CatOptions (HCons None l) l'
instance (CatOptions l l') => CatOptions (HCons (Some e) l) (HCons e l')
instance CatOptions HNil HNil

这将歧义问题限制在真正模棱两可的情况下，而不是列表包含例如代表任意Num实例的多态性类型。