haskell - haskell 如何解决重叠实例？

Question

如果我使用了错误的术语，请原谅，我是haskell 类型操作的初学者......我正在尝试使用具有功能依赖关系的重叠实例来使用HLists 进行一些类型级编程。

在这里，我的目标是尝试编写一个 typeclass 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对如何工作有更具体的定义吗？我觉得我错过了一些东西（比如“特异性”参数可能只适用于类型变量，而不适用于约束的数量......）

编辑：所以我尝试了 CA 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'对第二个实例的约束。

score 15 · Accepted Answer

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

Haskell如何处理实例非常简单。您正在处理 GHC 提供的多种实验性语言扩展，因此主要信息来源是GHC 用户指南。

OverlappingInstances 的工作方式是否有更具体的定义？我觉得我错过了一些东西（比如“特异性”参数可能只适用于类型变量，而不适用于约束的数量......）

你的猜测是正确的。从用户指南部分解释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 [] = []

知道在选择“模式”时会忽略“守卫”，很明显前两种模式无法区分。

但我希望你想知道如何让事情发挥作用，而不仅仅是为什么他们目前不这样做。（注意——我现在手头没有 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-- 前两个实例不可避免地是模棱两可的。

通过确保可以区分所有相关案例，可以部分避免最后一类歧义问题。例如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实例的多态类型的情况。

haskell - haskell 如何解决重叠实例？

1 回答 1

Related

Reference