GADTを使用して型クラス制約を自動的に派生させる

Question

私は、遅延評価を使用して無限シーケンスを処理するライブラリを作成しています。簡潔にするために、シーケンスの各用語のインデックスにOrdという制約をアサーションするために、一般化された代数データ型（GADT）を使用しています。したがって、次の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という制約で処理されます。

ただし、下位ブロックのコメントを外すと、add関数はエラーNo instance for (Ord ix) arising from the use of ``<''で型チェックに失敗します。 Sequenceの定義に表示されるTerm ix cffの(Ord ix)を把握できませんか？

Answer 1

Haskell98はランク1の多型をサポートし、多型の引数は関数をランク2の多型にするため、関数の引数にバインドされる用語は、デフォルトでは単相（別名ランク0多型）です。

したがって、Seq (addAlong (<) tms1 tms2)では、コンパイラは剛性タイプixの単相比較として<としか考えられません。単相関数として<を考えると、コンパイラはOrdインスタンスを解決する必要があります。ただし、その時点でTermから照合できるため、Ord ixインスタンスは使用できません！

あなたの元のコードに最も近いのソリューションは、明示的に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) = []