如何在Isabelle的typeclass定义中支持多种任意类型？

问题核心原因 #

你遇到的错误来自两个问题：

1. Isabelle 默认的单参数类型类不支持声明额外的多态返回类型变量，你需要用多参数类型类来承载name和params的返回类型约束
2. instantiation语法使用错误：Isabelle 的类实例是给类型构造器声明的，不能直接给填充了具体类型的复合类型声明实例

解决方案1：使用多参数类型类（符合你原来的typeclass使用习惯） #

首先定义多参数类型类，三个类型参数分别对应动作类型、name返回类型、params返回类型：

class action 'a 'b 'p =
  fixes name :: "'a ⇒ 'b"
    and params :: "'a ⇒ 'p"

然后给你的actionT1类型构造器声明实例，注意语法要传入类型变量而非具体类型：

datatype ('b, 'c, 'd) actionT1 = Act 'b 'c 'd

instantiation ('b, 'c, 'd) actionT1 :: (type, type, type) action
begin
definition name_actionT1 :: "('b, 'c, 'd) actionT1 ⇒ 'b" where
  "name_actionT1 (Act n _ _) = n"
definition params_actionT1 :: "('b, 'c, 'd) actionT1 ⇒ 'c × 'd" where
  "params_actionT1 (Act _ c d) = (c, d)"
instance proof qed (* 验证类约束满足 *)
end

之后你就可以正常定义依赖action类的函数：

fun equalParams :: "('a :: action 'b 'p) ⇒ 'a ⇒ bool" where
  "equalParams a b = (params a = params b)"

如果需要对具体类型(string, int, int) actionT1使用，直接调用即可，不需要额外声明实例：

value "equalParams (Act ''test'' 1 2) (Act ''test2'' 1 2)" (* 输出True *)

解决方案2：使用Locale（更灵活的接口抽象） #

如果你不需要用到类型类的排序约束，用Locale封装接口会更简单，不需要处理多参数类的类型标注：

(* 定义接口Locale *)
locale action =
  fixes name :: "'a ⇒ 'b"
    and params :: "'a ⇒ 'p"
begin
  (* 所有通用函数都可以定义在Locale内部 *)
  fun equalParams :: "'a ⇒ 'a ⇒ bool" where
    "equalParams a b ⟷ params a = params b"
end

(* 给actionT1实现接口 *)
datatype ('b, 'c, 'd) actionT1 = Act 'b 'c 'd
interpretation actionT1_action: action 
  "λ(Act n _ _). n" 
  "λ(Act _ c d). (c, d)" 
by auto

(* 调用示例 *)
value "actionT1_action.equalParams (Act ''test'' 1 2) (Act ''test2'' 1 2)"

内容的提问来源于stack exchange，提问作者Kookie