47

この最近の私の回答では、たまたまこの古い栗を割って開けました (非常に古いプログラムで、その半分は 17 世紀にライプニッツによって書かれ、70 年代に私の父によってコンピューター上で書かれました)。スペースを節約するために、最新のビットは省略します。

class Differentiable f where
  type D f :: * -> *

newtype K a     x  = K a
newtype I       x  = I x
data (f :+: g)  x  = L (f x)
                   | R (g x)
data (f :*: g)  x  = f x :&: g x

instance Differentiable (K a) where
  type D (K a) = K Void
instance Differentiable I where
  type D I = K ()
instance (Differentiable f, Differentiable g) => Differentiable (f :+: g) where
  type D (f :+: g) = D f :+: D g
instance (Differentiable f, Differentiable g) => Differentiable (f :*: g) where
  type D (f :*: g) = (D f :*: g) :+: (f :*: D g)

さて、ここでイライラすることがあります。それ自体が微分可能でD fなければならないことを規定する方法がわかりません。確かに、これらのインスタンスはその性質を尊重しており、ファンクタを微分し続け、より多くの場所で穴をあける機能を利用する楽しいプログラムを作成できる可能性があります: テイラー展開など。

みたいなことが言えるようになりたいです

class Differentiable f where
  type D f
  instance Differentiable (D f)

インスタンス宣言typeに、必要なインスタンスが存在する定義があることを確認する必要があります。

多分もっとありふれたもの

class SortContainer c where
  type WhatsIn c
  instance Ord (WhatsIn c)
  ...

もいいでしょう。もちろん、それにはfundepの回避策があります

class Ord w => SortContainer c w | c -> w where ...

しかし、同じトリックを試みるのDifferentiableは...まあ...面倒です。

それで、再現可能な微分可能性を得る気の利いた回避策はありますか？(表現GADT and and and and ...を構築できると思いますが、クラスで機能する方法はありますか?)

また、宣言時に型 (およびおそらくデータ) ファミリに対して制約を要求し、インスタンスがそれらを満たすことを確認できるようにする必要があるという提案に、明らかな障害はありますか?

4

4 に答える 4

49

確かに、明らかなことは、単純に目的の制約を直接記述することです。

class (Differentiable (D f)) => Differentiable (f :: * -> *) where

悲しいかな、GHC はそれについて大騒ぎし、一緒にプレイすることを拒否します。

ConstrainTF.hs:17:1:
    Cycle in class declaration (via superclasses):
      Differentiable -> Differentiable
    In the class declaration for `Differentiable'

そのため、型制約を GHC の反抗的なままにしてしまうほど派手に記述しようとする場合によくあることですが、何らかの不正な策略に頼らなければなりません。

型ハッカーが関与する GHC のいくつかの関連機能を思い出してください。

  • それがユーザーにもたらす実際の不便さとはかけ離れた、型レベルの非終了について偏執的です。
  • 利用可能なすべての情報を考慮する前に、クラスとインスタンスに関する決定に喜んでコミットします。
  • だましてコミットさせたものはすべて、忠実にチェックしようとします。

(~)これらは、特定の型ハッカー構造の型推論動作を改善するために型が事後的に統合される、おなじみの古い偽ジェネリック インスタンスの根底にあるよこしまな原則です。

しかし、この場合、型情報を GHC の前に忍び込ませるのではなく、 GHC がクラス制約に気付かないようにする必要があります。

import GHC.Prim

type family DiffConstraint (f :: * -> *) :: Constraint
type instance DiffConstraint f = Differentiable f

class (DiffConstraint (D f)) => Differentiable (f :: * -> *) where
  type D f :: * -> *

独自の爆竹で巻き上げる！

それも本当の取引です。あなたが望むように、これらは受け入れられます：

instance Differentiable (K a) where
  type D (K a) = K Void
instance Differentiable I where
  type D I = K ()

しかし、代わりにナンセンスを提供すると、次のようになります。

instance Differentiable I where
  type D I = []

GHC は、まさに私たちが見たいと思っているエラー メッセージを表示します。

ConstrainTF.hs:29:10:
    No instance for (Differentiable [])
      arising from the superclasses of an instance declaration
    Possible fix: add an instance declaration for (Differentiable [])
    In the instance declaration for `Differentiable I'

もちろん、小さな問題が 1 つあります。つまり、次のことです。

instance (Differentiable f, Differentiable g) => Differentiable (f :+: g) where
  type D (f :+: g) = D f :+: D g

...は十分に根拠がないことが判明しました.GHCにそれをチェックするように指示したので, is はいつでも(f :+: g), Differentiableso is (D f :+: D g), これはうまく終わらない (またはまったく).

これを回避する最も簡単な方法は、通常、明示的な基本ケースの山をボイラープレートにすることですが、ここで GHC はDifferentiableインスタンス コンテキストに制約が現れるたびに発散することを意図しているようです。どうにかしてインスタンスの制約をチェックするのに不必要に熱中していて、おそらく別の策略の層で十分に気が散っている可能性があると思いますが、どこから始めればいいのかすぐにはわかりません。

#haskell に関する IRC の議論で、GHC がクラス コンテキスト制約を処理する方法について少し記憶がよみがえりました。これを使用して：

type family DiffConstraint (f :: * -> *) :: Constraint
type instance DiffConstraint (K a) = Differentiable (K a)
type instance DiffConstraint I = Differentiable I
type instance DiffConstraint (f :+: g) = (Differentiable f, Differentiable g)

これで、合計に対してより適切に動作する再帰が得られました。

instance (Differentiable (D f), Differentiable (D g)) => Differentiable (f :+: g) where
  type D (f :+: g) = D f :+: D g

ただし、再帰的なケースは、製品に対してそれほど簡単に分割することはできません。同じ変更を適用すると、単純に無限ループにぶら下がるのではなく、コンテキスト削減スタック オーバーフローを受け取った場合にのみ問題が改善されます。

于 2013-01-03T05:33:09.030 に答える
19

あなたの最善の策は、constraintsパッケージを使用して何かを定義することかもしれません:

import Data.Constraint

class Differentiable (f :: * -> *) where
  type D f :: * -> *
  witness :: p f -> Dict (Differentiable (D f))

その後、再帰が必要なときはいつでも辞書を手動で開くことができます。

これにより、ケーシーの回答でソリューションの一般的な形状を採用できますが、誘導時にコンパイラー (またはランタイム) を永久にスピンさせることはできません。

于 2013-01-04T00:37:28.963 に答える