このトピックについて多くの質問があることは知っていますが、私が使用しているライブラリには、エラーを引き起こしている特定の何かがあると感じています。
module Test where
import Clash.Prelude
init' :: Vec (n + 1) a -> Vec n a
init' (_ :> Nil) = Nil
init' (x :> (xs:>ys)) = x :> (init' (xs:>ys))
私が得ているエラーは、
Test.hs:28:14: error:
• Couldn't match type ‘n’ with ‘n0 + 1’
‘n’ is a rigid type variable bound by
the type signature for:
init' :: forall (n :: Nat) a. Vec (n + 1) a -> Vec n a
at Test.hs:26:1-33
Expected type: Vec n a
Actual type: Vec (n0 + 1) a
• In the pattern: xs :> ys
In the pattern: x :> (xs :> ys)
In an equation for ‘init'’:
init' (x :> (xs :> ys)) = x :> (init' (xs :> ys))
• Relevant bindings include
init' :: Vec (n + 1) a -> Vec n a (bound at Test.hs:27:1)
|
28 | init' (x :> (xs:>ys)) = x :> (init' (xs:>ys))
|
Clash.Preludeライブラリの定義は次のとおりです。
data Vec :: Nat -> * -> * where
Nil :: Vec 0 a
Cons :: a -> Vec n a -> Vec (n + 1) a
pattern (:>) :: a -> Vec n a -> Vec (n + 1) a
pattern (:>) x xs <- ((\ys -> (head ys,tail ys)) -> (x,xs))
where
(:>) x xs = Cons x xs
これはClashライブラリのバグ/制限です。次のような単純なものを定義することすらできないことがわかります。
safeHead :: Vec n a -> Maybe a
safeHead Nil = Nothing
safeHead (x :> _) = Just x
問題は、(:>)パターンの定義です。
pattern (:>) :: a -> Vec n a -> Vec (n + 1) a
pattern (:>) x xs <- ((\ys -> (head ys,tail ys)) -> (x,xs))
where
(:>) x xs = Cons x xs
初登場にもかかわらず、その署名は間違っています！代わりに、はるかに単純な（そして本質的に同等の）定義が与えられていたとしたら：
pattern (:>) x xs = Cons x xs
推測される型シグネチャは次のようになります。
pattern (:>) :: () => (n ~ n1 + 1) => a -> Vec n1 a -> Vec n a
（これも明示的に指定できます）、コードは正常に機能します（のCons代わりに直接使用できる場合と同じように(:>）。
2セットの制約があるこのシグニチャの異常な形式は、パターンシノニムに固有です。制約の最初のセットは、「必須」制約のセットを提供します。これは、パターンを使用するコードがタイプが正しいと見なすために満たす必要がある制約です。2つ目は、「提供された」制約のセットを示します。これらの制約は、実行時にパターンを実際に照合することにより、ケースブランチのスコープに組み込まれます。これについて詳しくは、GHCドキュメントのパターンシノニムの入力をご覧ください。
残念ながら、ライブラリで使用されている明示的な署名は次のとおりです。
pattern (:>) :: a -> Vec n a -> Vec (n + 1) a
と同等です：
pattern (:>) :: (n ~ n1 + 1) => () => Vec n1 a -> Vec n a
どこの制約nとn1「必要」の代わりに「提供」の制約セットに表示されます。これは大きな問題です！
の定義のこの部分ではinit'：
init' (x :> (xs:>ys)) = x :> (init' (xs:>ys))
1つ目:> は、式全体で一致する引数がいくつかのx :> (xs :> ys)aVec (n + 1) aである必要がありますn。幸いなことに、これはの型シグネチャによるものinit'です。残念ながら、2番目の引数では、型チェックを行うために、引数（型であることがわかっている）が一部の引数である:> 必要があります。そのような制約はありません！このような制約を提供するのは、（前の行のようにによる一致とは対照的に）この秒による一致です。Vec n aVec (m + 1) am:>Nil
最終的に、我々は提供するために、制約ループの一種で立ち往生しているn ~ m + 1いくつかのためにm、我々はすでに持っている必要がありますn ~ m + 1いくつかのためにm。
それで、あなたは何ができますか？言うのが難しい。CHANGELOGforClashによると、この奇妙なパターン定義は意図的に追加されたため、「パターンマッチング:>はCLaSHコンパイラで合成できるようになりました」。これが何を意味するのかわかりませんが、Clashメンテナはおそらくそうしています。私は彼または彼女にメールを送り、のパターン定義は(:>)あなたが定義safeHeadやなどの単純なことをするのを妨げることを指摘し、init'彼または彼女がパターンを書き直して適切なパターンマッチングを可能にし、これを「合成可能」に保つことができるかどうかを確認しますビジネス作業。
この記事はインターネットから収集されたものであり、転載の際にはソースを示してください。
侵害の場合は、連絡してください[email protected]
コメントを追加