3

首先，在对类型类了解不多的情况下，似乎类型类是重载类型符号的最佳方式，除非我不能使用类型类，或者不知道如何使用。我没有使用类型类。

其次，我很确定我不想覆盖对所有类型都有意义的运算符的符号，例如\<in>, \<times>, *,\<union>等。

但是，诸如此类的运算符+对我的 type 没有任何意义sT，尽管这与我的第一点有关。我最终希望+type 有多种含义sT => sT => sT，我认为这不会发生。

示例的四个版本

为了使我的问题具体化并表明我不是唯一一个有问题的人，我从Klein 的课程中​​举了一个简单的例子，文件是Demo14.thy。

在示例的四个版本之后，我问：“对于第四个示例，我可以摆脱警告吗？”

他从一个没有警告或错误的简单示例开始：

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

他使用\<cdot>, 这代表了我到目前为止所做的事情，而不是使用 Isabelle/HOL 已经声称的符号。

我将他的更改\<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)"

我真正关心的是第四个版本，它给出了一个警告，即使我已经插入(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. 正因为如此，证明者做了​​很多工作，在最终弄清楚 mysemi4是唯一+为 type 定义的地方之后sT => sT => sT，它让我使用它。

我不知道我的摘要，但我可以修复semi4它不给我警告吗？

*（注意：给定示例，从数学上讲，使用符号代替会更有意义+，但这*是我不想覆盖的符号。）

4

1 回答 1

1

我想我已经弄清楚了大部分。

假设你有一个函数

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

并且您想使用加号+作为符号。

关键是定义的上下文+。在全球层面，至少有两种方式。一种是简单的方法

myFun (infixl "+" 70)

另一种方法是+在类型类定义中定义。特别是，在Groups.thy中，第 136 行是两行

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

+因此，有了前言，简短的回答是，在全局级别，只有一种方法可以在尝试使用for时摆脱警告myFun :: "myT => myT => myT"，那就是将 type 实例化为functionmyT的类型类。plusmyFun

这样做非常简单，我将在其中展示如何做到这一点，并且它独立于 Groups.thy 中使用plus.

但是，在myT全局级别定义类型后，无论是通过简单的方式还是通过类型类，尝试+再次为 type定义(myT => myT => myT)都会导致全局级别和语言环境的错误。

现在说得通了。重载语法的使用都是基于类型推断的，因此特定类型的特定语法只能分配给一个函数。

对于语言环境，+在不同语言环境中的使用是独立的。警告的原因是类型类定义plus。您无法摆脱 locales 的警告，因为plus已被定义为类型类 for ('a => 'a => 'a)，这是一个全局定义。

这是一些带有一些注释的代码。实例化plusformyT需要所有 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 回答