0

次のコードは型チェックを行いません:

type_synonym env = "char list ⇀ val"

interpretation map: order "op ⊆⇩m :: (env ⇒ env ⇒ bool)" "(λa b. a ≠ b ∧ a ⊆⇩m b)"
by unfold_locales (auto intro: map_le_trans simp: map_le_antisym)

lemma
  assumes "mono (f :: env ⇒ env)"
  shows "True"
by simp

Isabelle は補題で次のエラーを訴えます。

Type unification failed: No type arity option :: order

Type error in application: incompatible operand type

Operator:  mono :: (??'a ⇒ ??'b) ⇒ bool
Operand:   f :: (char list ⇒ val option) ⇒ char list ⇒ val option

なんでそうなの？解釈を使用するために何かを逃しましたか？ここには newtype ラッパーのようなものが必要だと思います...

4

1 に答える 1

1

型クラスに対応するようにロケールを解釈すると、ロケールorderのコンテキスト内で証明された定理しか得られません。ただし、定数monoは型クラスでのみ定義されます。その理由は、monoの型には 2 つの型変数が含まれているのに対し、型クラスのロケール内では 1 つしか使用できないためです。map.monoあなたの解釈に由来するものがないため、これに気付くことができます。

より小さいorderオプション タイプの型クラスをインスタンス化する場合、関数空間が点ごとの順序でインスタンス化されるため、マップに使用できます。ただし、マップ上の順序付けは、構文的にではなく、意味的にのみ と同等であるため、 についての既存の定理はいずれも機能しません。さらに、あなたの理論は、別の方法でインスタンス化する他の人々の理論と互換性がありません。NoneSome xmonoorder<=⊆⇩m⊆⇩m<=orderoption

したがって、型クラスを使用しないことをお勧めします。述語monotoneは、使用される順序を明示的に取ります。これはもう少し書きますが、結局のところ、型クラスよりも柔軟です。たとえば、環境の単調な変換であるmonotone (op ⊆⇩m) (op ⊆⇩m) f表現を書くことができます。f

于 2016-06-24T15:44:36.343 に答える