使用GADT自动派生类型类约束

Question

我正在编写一个库来处理使用延迟评估的无限序列.为简洁起见,我使用广义代数数据类型(GADT)来断言Ord对序列中每个术语的索引的约束.因此,以下类型检查:

{-# LANGUAGE GADTs #-}

data Term ix cff where
  Term :: (Ord ix) => ix -> cff -> Term ix cff

data Sequence ix cff where
  Seq :: [Term ix cff] -> Sequence ix cff

f (Seq (Term i x:_)) (Seq (Term j y:_)) = i < j

{-
add :: Sequence ix cff -> Sequence ix cff -> Sequence ix cff
add (Seq tms1) (Seq tms2) = Seq (addAlong (<) tms1 tms2)
    where addAlong :: (ix -> ix -> Bool) ->
                      [Term ix cff] -> [Term ix cff] -> [Term ix cff]
          addAlong ord (Term i x : tms1) (Term j y : tms2) = []
-}

正如所料,GHCi告诉我f :: Sequence t t1 -> Sequence t t2 -> Bool.进行比较i < j需要一个Ord实例,但是由(Ord ix)定义中的约束来处理Term.

但是,当取消注释下部块时,该add函数无法检查错误No instance for (Ord ix) arising from the use of ``<''.难道它不能(Ord ix)从Term ix cff出现在定义中的那个中找出答案Sequence吗？

Answer 1

绑定到函数参数的术语默认是单态的(也就是rank-0多态),因为Haskell98仅支持rank-1多态,而多态参数使函数rank-2为多态.

因此,在Seq (addAlong (<) tms1 tms2)编译器中,编译器只能将其<视为刚性类型的单形比较ix.要将<编译器视为单态函数,需要解析该Ord实例.但是,此时Ord ix实例不可用,因为它只能匹配Term!

与原始代码最接近的解决方案是明确地使addAlongrank-2多态:

{-# LANGUAGE RankNTypes, UnicodeSyntax #-}

add :: Sequence ix cff -> Sequence ix cff -> Sequence ix cff
add (Seq tms1) (Seq tms2) = Seq (addAlong (<) tms1 tms2)
    where addAlong :: (? ix' . Ord ix' -> ix' -> Bool) ->
                      [Term ix cff] -> [Term ix cff] -> [Term ix cff]
          addAlong ord (Term i x : tms1) (Term j y : tms2) = []

这样,<只是按原样传递(作为多态Ord => ...方法),因此编译器不需要在实例中提供实例,Seq (addAlong (<) tms1 tms2)但可以在以后可用时解析它Term.

你当然应该考虑你是否真的需要它.Ord在每个字典中保留一本字典Term对我来说似乎相当浪费 - 如果你保持约束,问题就不会出现Seq:

data Term ix cff where Term :: ix -> cff -> Term ix cff

data Sequence ix cff where
  Seq :: Ord ix => [Term ix cff] -> Sequence ix cff

add :: Sequence ix cff -> Sequence ix cff -> Sequence ix cff
add (Seq tms1) (Seq tms2) = Seq (addAlong (<) tms1 tms2)
    where addAlong :: (ix -> ix -> Bool) ->
                      [Term ix cff] -> [Term ix cff] -> [Term ix cff]
          addAlong ord (Term i x : tms1) (Term j y : tms2) = []