タイプレベルナチュラルのクラス制約の回避

GHC.TypeLitsモジュールのNatタイプを使用しています。これはプログラマインターフェイスを別のライブラリに定義する必要があると言います。いずれにしても、GHC.TypeLitsは、コンパイル時間NatをランタイムIntegerに変換するクラス機能natValを有するクラスKnownNatを有する。また、コンパイル時間Natを追加する型関数(+)があります。タイプレベルナチュラルのクラス制約の回避

問題は(KnownNat n1, KnownNat n2)と指定されているため、GHCはKnownNat (n1 + n2)を派生できません。

これは、タイプレベルのナチュラルを追加するたびに追加する必要がある爆発の爆発をもたらします。

data Nat = Zero | Succ Nat

それともtype-naturalのようなライブラリを使用します。

1つの選択肢はそうのような自然数を自分で定義することです。しかし、それは代わりに定義するのでも、あなたがうまく種類のリテラル番号を使用できるようにするGHCに組み込まれたNats、（すなわち0、1）を使用しないように愚かなようだ：

N0 = Zero 
N1 = Succ N0 
etc...

は、この問題を回避とにかくありGHC KnownNatの問題が全面的に要求されていますか？または、問題のためにモジュールGHC.TypeLitsを無視するだけですか？「型チェッカープラグインは」威圧少し聞こえる場合は、（それが最初に私にやった）https://hackage.haskell.org/package/ghc-typelits-knownnat

：

出典

2017-01-10 Clinton

[この質問]（https://stackoverflow.com/questions/41492754/could-not-deduce-knownnat-in-two-existentials-with-respect-to-the-singletons-lib/41496362）とそれに対応する答え。 – gallais

このGHCの型チェッカープラグインない、まさにそれは（すでに利用可能な他のものから、「複合体」KnownNat制約を導出します）実際に使用するのは非常に簡単です。単にあなたのパッケージファイル内の依存関係として追加します（またはカバルそれをインストール）、その後、他のパッケージのようにいずれかの追加：

{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}

を（ずっとLANGUAGEプラグマなどの）ソースファイルの先頭に、またはそれを追加パッケージファイル内のオプションとしてグローバルに使用します。

同じ著者の別のプラグインもあります。このプラグインは、typelit Nats：https://hackage.haskell.org/package/ghc-typelits-natnormaliseでの作業にも非常に便利です。これは、GHCが「期待」と「実際」の型が一致していることを証明しようとしているときに常に現れるn + (m + 1) ~ (n + 1) + mのようなもので、GHCが諦めるNat型の式の平等を推論することができます。

出典

2017-01-10 05:39:35 Ben

タイプレベルナチュラルのクラス制約の回避

答えて

関連する問題