次のコードは、です。TypeCheckていない部分のマップ

Question

と注文ロケールを使用：なぜそんなに

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 

：

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 

イザベルは補題で次のエラーで文句を言いますか？私は解釈を使用するために何かを逃したのですか？ここに新しいタイプのラッパーのようなものが必要だと思われます...

Answer 1

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

あなたはNone未満Some xことでオプションの種類の型クラスorderをインスタンス化した場合の機能スペースが点別順位でorderインスタンス化するので、あなたは、マップのためmonoを使用することができます。しかし、マップ上の<=の順序は、構文的にではなく、⊆⇩mと意味的にしか等しくないので、⊆⇩mについての既存の定理のいずれも<=に対しては機能せず、その逆もありません。さらに、あなたの理論はoptionのためにorderをインスタンス化する他の人とは互換性がありません。

したがって、私はタイプクラスなしで行くことをお勧めします。述語monotoneは、明示的に使用する順序をとります。これはもう少し書くことですが、結局は型クラスよりも柔軟性があります。たとえば、monotone (op ⊆⇩m) (op ⊆⇩m) fと書くと、fは環境のモノトーン変換です。