使用GADT自动推导类型约束

Question

我正在写一个库来处理使用懒惰评估的无限序列。为简洁起见，我使用广义代数数据类型（GADT）来声明序列中每个项的索引的Ord约束。因此，以下typechecks：

{-# 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实例，但这由Term的定义中的约束(Ord ix)来处理。

但是，当下块没有注释时，add函数无法检测到错误No instance for (Ord ix) arising from the use of ``<''。它不应该能够从Term ix cff中找出出现在Sequence的定义中的(Ord ix)吗？

Answer 1

由于Haskell98仅支持rank-1多态性，并且多态参数使得函数rank-2多态，所以绑定到函数参数的术语默认为单形态（又名rank-0多态）。

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

这是最接近原始的代码是明确地让addAlong等级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可用时稍后解决。

你当然应该考虑你是否真的需要这个。在每个Term保持一个Ord字典似乎相当浪费我 - 如果你在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) = []