logo标签列表

Haskell如何解决重叠实例？

haskellfunctional-dependenciestype-level-computation
16
请原谅我如果我使用了错误的术语，因为我在Haskell类型操作方面还是个新手... 我试图使用具有功能依赖的重叠实例来进行一些与HLists相关的类型级编程。
我的目标是尝试编写一个类型类 HNoNils l l'，其中 HNoNils l l' 表示对于 l 作为列表类型（例如：Int:String:EmptyNil:Int:HNil），l' 是相应的不包含特定空类型 EmptyNil 的列表类型（示例结果：Int:String:Int:HNil）。
{-# 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。
根据我所了解的，使用 OverlappingInstances 扩展，系统应始终解析为最具体的实例。
在这里：

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

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

请原谅我如果我错了，但似乎第一个实例比第二个更具体，所以它应该选择第一个实例，对吗？
我尝试添加约束条件来消除重叠，即通过向第二个实例添加单独的相反等式约束条件：
-- 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'）这样的情况，至少我认为不会。
当重新添加OverlappingInstances时，我得到了更奇怪的错误，我不理解：
 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 的工作方式是否有更具体的定义？我感觉自己缺少了什么（比如 "特定性" 参数是否仅与类型变量相关，而不是约束数量...） 编辑：所以我尝试了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'。

1
关于你的第一个问题（在文本中间），第二个实例实际上比第一个更具体，因为实例头更具体。在这种情况下，不考虑第一个实例的实例上下文更具体。 - stephen tetley
1
解决方案可以朝任何方向发展，因为它试图解决由fundeps给出的约束条件。这可能很有用，但这是一种非常不同的思考方式。这就是为什么类型族通常更受青睐的部分原因。 - C. A. McCann
1个回答
15
"能否提供更详细的信息，说明Haskell如何处理实例？有些组合看起来似乎是不可能的。即使只是一个解释机制的文档链接也会很受欢迎。"
"Haskell如何处理实例非常简单。您正在处理由GHC提供的多个实验性语言扩展，因此主要信息来源是GHC用户指南。"
"是否有更具体的定义来解释OverlappingInstances的工作原理？我感觉我遗漏了一些东西（例如“特异性”参数只适用于类型变量，而不是约束的数量...）"
你的猜测是正确的。来自用户指南部分，解释OverlappingInstances:

When GHC tries to resolve, say, the constraint C Int Bool, it tries to match every instance declaration against the constraint, by instantiating the head of the instance declaration. For example, consider these declarations:

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)

The instances (A) and (B) match the constraint C Int Bool, but (C) and (D) do not. When matching, GHC takes no account of the context of the instance declaration (context1 etc).

将其视为类似于模式和守卫的东西：
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 [] = []

当选择“模式”时，忽略“保护符”，因此可以明确地知道前两个模式是无法区分的。

But I expect you'd like to know how to make things work, not merely why they currently don't. (N.B. -- I don't have a GHC at hand right now so this is all from memory and has not been tested. I may have gotten a few details wrong.)
有几种处理这种情况的方法。可能最常见的是采用两步法，首先在通用实例的上下文中使用类型函数，然后转而使用接受额外参数的辅助类的特定实例：
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

This version仍然会在某些情况下失败，这是没有好的解决方法的。如果类型列表包含可能与EmptyNil统一的类型变量——请记住，在此时忽略约束条件，而且GHC必须考虑稍后为EmptyNil添加任意实例——前两个实例将不可避免地产生歧义。
通过确保所有相关情况都可以区分，可以在一定程度上避免最后一种歧义问题。例如，而不是删除像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实例的多态类型的情况。

1
感谢您再次回答我的问题，并提供了许多关于这些事情如何工作的见解。我尝试了您的建议之一（即直接在实例头中使用EmptyNil），但是我遇到了重叠实例错误（请参见我的问题编辑）。我也将尝试您的其他“解决方法”。 - rtpg
1
嗯，显然我有点生疏了。尝试将第二个实例更改为(HNoNils l l'，r ~ HCons e l') => HNoNils（HCons e l）r，看看是否有效？如果有效，我会更新答案并解释原因。:] - C. A. McCann
网页内容由stack overflow 提供, 点击上面的
可以查看英文原文，
原文链接