haskell如何解决重叠实例？

Question

如果我使用错误的术语,请原谅我,我是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

我不明白第二场比赛.毕竟,在这个决议中,我们等于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工作方式有更具体的定义吗？我觉得我错过了一些东西(比如说"特异性"参数可能只适用于j型变量,而不是约束数...)

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

Answer 1

是否有可能获得有关Haskell如何与实例一起工作的更详细信息？其中一些组合似乎不可能.即使只是一个解释机制的文档的链接将不胜感激

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

是否有更具体的定义OverlappingInstances如何工作？我觉得我错过了一些东西(比如说"特异性"参数可能只适用于j型变量,而不是约束数...)

你的猜测是正确的.从用户指南部分解释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不考虑实例声明(context1etc)的上下文.

把它看作模式与守卫之类的东西:

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实例的多态类型的情况.