3

まず、型クラスについてよく知らなくても、型クラスを使用できない場合や方法を理解していない場合を除き、型クラスは型の表記法をオーバーロードするための最良の方法のようです。私は型クラスを使用していません。

\<in>第二に、\<times>、*、\<union>、 など、すべての型に意味を持つ演算子の表記法をオーバーライドしたくないと確信しています。

ただし、このような演算子+は type には意味がありませんがsT、これは最初のポイントにつながります。最終的には+、 type に複数の意味を持たsT => sT => sTせたいと考えていますが、それは実現しないと思います。

例の 4 つのバージョン

私の質問を具体的にし、問題を抱えているのは私だけではないことを示すために、クラインのコースから簡単な例を取り上げます。ファイルはDemo14.thyです。

例の 4 つのバージョンの後、「4 番目の例では、警告を取り除くことができますか?」と尋ねます。

彼は、警告もエラーも出さない単純な例から始めます。

locale semi =
  fixes prod :: "['a, 'a] => 'a" (infixl "\<cdot>" 70)
  assumes assoc: "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"

彼は\<cdot>.

\<cdot>彼をに変更する+と、エラーが発生します。

locale semi2 =
  fixes prod :: "['a, 'a] => 'a" (infixl "+" 70)
  assumes assoc: "(x + y) + z = x + (y + z)"

HOL ソースを調べたところ、 type 、特に特定の型クラスに対して+が定義されていることがわかりました。('a => 'a => 'a)

semi2単独に固有のものではないことを確認するために変更する'aと、警告のみが表示されます。

locale semi3 =
  fixes prod :: "('a => 'a) => ('a => 'a) => 'a" (infixl "+" 70)
  assumes assoc: "(x + y) + z = x + (y + z)"

私が本当に気にかけているのは、この 4 番目のバージョンです。挿入したにもかかわらず、警告が表示され(x::sT)ます。

locale semi4 =
  fixes prod :: "sT => sT => sT" (infixl "+" 70)
  assumes assoc: "((x::sT) + y) + z = x + (y + z)"

警告は次のとおりです。

Ambiguous input
produces 16 parse trees (10 displayed):
[...]
Fortunately, only one parse tree is type correct,
but you may still want to disambiguate your grammar or your input.

まとめと質問

私自身は、次のように要約しています。 演算子+は多くの場所で定義されており、特に type に対して定義されており'a => 'a => 'a、これは一般に に対しても定義されていsT => sT => sTます。そのため、証明者は多くの作業を行い、 my がtype に対して定義されているsemi4唯一の場所であることを最終的に把握した後、それを使用させてくれます。+sT => sT => sT

サマリーがわかりませsemi4んが、警告が表示されないように修正できますか?

(注: 例を考えると、数学的には の*代わりに記号を使用する方が理にかなっています+が、*オーバーライドしたくない表記になります。)

4

1 に答える 1

1

ほとんどのことはわかったと思います。

関数があるとします

myFun :: "myT => myT => myT",

+プラス記号を表記として使用したい場合。

+キーは、が定義されているコンテキストです。グローバルレベルでは、少なくとも 2 つの方法があります。ひとつは簡単な方法

myFun (infixl "+" 70)

別の方法は+、型クラス定義で定義することです。特にGroups.thyでは、136 行目に 2 つの行があります。

class plus =
  fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "+" 65)

+したがって、その序文で、簡単な答えは、グローバル レベルでforを使用しようとしたときに警告を取り除く唯一の方法があるということです。それは、 type をfunction の型クラスとしてmyFun :: "myT => myT => myT"インスタンス化することです。myTplusmyFun

これを行うのは非常に簡単です。ここでその方法を示します。これは、 plus.

ただし、myTグローバル レベルで型を定義した後、単純な方法または型クラスを介して型を定義+し直そうとする(myT => myT => myT)と、グローバル レベルとロケールの両方でエラーが発生します。

今では理にかなっています。オーバーロードされた構文の使用はすべて型推論に基づいているため、特定の型の特定の構文は 1 つの関数にしか割り当てることができません。

ロケールの場合、異なるロケールでの の使用+は独立しています。警告の原因は、型クラス定義によるものplusです。グローバル定義であるplusの型クラスとして定義されているため、ロケールの警告を取り除くことはできません。('a => 'a => 'a)

いくつかのコメントを含むコードを次に示します。plusfor のインスタンス化にmyTは 5 行すべてが必要です。

  typedecl myT

--"Two locales can both use '+'. The warning is because '+' has been defined
   in a type class for 'a. If anything defines '+' globally for type myT, these
   locales will give an error for trying to use it."
locale semi1 =
  fixes plus :: "myT => myT => myT" (infixl "+" 70)
  assumes assoc: "((x::myT) + y) + z = x + (y + z)"
locale semi2 =
  fixes plus :: "myT => myT => myT" (infixl "+" 70)
  assumes assoc: "((x::myT) + y) + z = x + (y + z)"


--"DEFINING PLUS HERE GLOBALLY FOR (myT => myT => myT) RESERVES IT EXCLUSIVELY"

definition myFun :: "myT => myT => myT" (infixl "+" 70) where
  "myFun x y = x"
--"Use of 'value' will give a warning if '+' is instantiated globablly prior
   to this point."
value "(x::myT) + y"


--"PLUS HAS BEEN DEFINED ALREADY. SWITCH THIS NEXT SECTION WITH THAT ABOVE AND
    myFun THEN GETS THE ERROR. DELETE myFun AND THE ERROR GOES AWAY."

definition myT_plus_f :: "myT => myT => myT" where
  "myT_plus_f x y = x"

instantiation myT :: plus
begin
  definition plus_myT:
    "x + y = myT_plus_f x y"  --"Error here if '+' globally defined prior to this for type myT."
  instance ..
end
--"No warning here if '+' instantiated for myT; error if '+' defined globablly for
   type myT."
value "(x::myT) + y"


--"ERRORS HERE FOR LOCALES BECAUSE '+' IS DEFINED GLOBALLY"

locale semi3 =
  fixes plus :: "sT => sT => sT" (infixl "+" 70)
  assumes assoc: "((x::sT) + y) + z = x + (y + z)"
locale semi4 =
  fixes plus :: "sT => sT => sT" (infixl "+" 70)
  assumes assoc: "((x::sT) + y) + z = x + (y + z)"
于 2013-05-03T19:55:08.147 に答える