如何在 => 处实例化类型类？答案

【问题标题】：How can I instantiate a typeclass at =>?如何在 => 处实例化类型类？
【发布时间】：2018-11-13 08:50:49
【问题描述】：

我正在尝试使用 Isabelle/Pure 作为逻辑框架来实现新逻辑的证明助手（因此 Isabelle/HOL 除了作为动机之外无关紧要）。

有没有办法为函数 type => 定义一个类型类实例化，比如

instantiation "=>" :: (foo,foo)foo

所以只要A 和B 是foo 的实例化，那么A => B 也会自动成为？不接受上述语法；看来我需要一个函数类型构造函数的名称（不仅仅是一个符号），但如果存在这样的名称，我不知道它是什么或在哪里找到它。

我是 Isabelle 的新手，所以如果我尝试做的事情出于某种原因是错误的，请务必告诉我。

【问题讨论】：

标签： isabelle

【解决方案1】：

是的，您可以为函数定义类实例化。如果你对函数使用类型构造器的名称fun，而不是中缀运算符=>，这没有问题。

例如：

class foo = 
  fixes bar :: 'a

instantiation "fun" :: (foo,foo) foo
begin
definition "(bar :: 'a ⇒ 'b) = (λ x. bar)" 
instance ..
end

两个备注：

fun 用双引号括起来，否则它会与定义函数的外部关键字fun 发生冲突。
在这个例子中，你也可以写成instantiation "fun" :: (type,foo) foo，因为bar对于函数的定义不依赖于 bar 'a 类型的常量。

【讨论】：

谢谢！为了将来参考，我怎么会发现函数的类型构造函数称为fun？它在文档中的某个地方吗？是否有对 Isabelle 显示中缀运算符含义的自省命令？
另外，您提议的(type,foo)foo 在 Pure 中对我不起作用；它说Undeclared class: "??.type". Failed to parse sort。我是否必须声明 default_sort 才能做这样的事情？
如果您在 Pure 中，请尝试使用 "{}" 而不是 type。
@MikeShulman，要自己找到类型构造函数的名称，您可以在 Isabelle/jEdit 缓冲区中键入 term ‹λx. x›。这将在输出窗格中显示恒等函数的类型。然后，按住 Ctrl 并将鼠标悬停在函数空间箭头上。应该会出现一个弹出窗口，告诉您类型构造函数被称为“有趣”。或者，Ctrl-右键单击功能空间箭头将带您到定义点。