Isabelle中如何定义支持任意类型的assn存在量词构造子

问题背景 #

现有assn数据类型定义如下：

datatype assn = 
    Aemp                                           (* Empty heap *)
  | Apointsto exp exp    (infixl "⟼" 200)        (* Singleton heap *)
  | Astar assn assn      (infixl "**" 100)         (* Separating conjunction *)
  | Awand assn assn                                (* Separating implication *)
  | Apure bexp                                     (* Pure assertion *)
  | Aconj assn assn                                (* Conjunction *)
  | Adisj assn assn                                (* Disjunction *)
  | Aex "(nat ⇒ assn)"                            (* Existential quantification *)

尝试将最后一行修改为Aex "('a ⇒ assn)"以支持任意类型的存在性定义时，IDE提示错误：Extra type variables on right-hand side: "'a"。已知在Coq中可通过Aex (A: Type) (pp: A -> assn)实现类似功能，询问Isabelle中的实现方法。

解决方案 #

方法1：给构造器显式添加多态类型量化 #

Isabelle默认要求datatype构造器的类型变量需在全局声明或显式量化。给Aex构造器前添加∀'a.，明确其支持任意类型'a的函数参数：

datatype assn = 
    Aemp                                           (* Empty heap *)
  | Apointsto exp exp    (infixl "⟼" 200)        (* Singleton heap *)
  | Astar assn assn      (infixl "**" 100)         (* Separating conjunction *)
  | Awand assn assn                                (* Separating implication *)
  | Apure bexp                                     (* Pure assertion *)
  | Aconj assn assn                                (* Conjunction *)
  | Adisj assn assn                                (* Disjunction *)
  | ∀'a. Aex "('a ⇒ assn)"                            (* Existential quantification *)

修改后，Aex可接受任意类型到assn的函数，例如Aex (λx::nat. x ⟼ 0)或Aex (λs::string. Apure (s = ""))，不会再触发类型变量错误。

方法2：将assn定义为参数化多态类型 #

若需要整个assn类型支持多态（比如后续其他构造器也需类型参数），可将assn声明为参数化类型'a assn，同时调整所有构造器的类型标注：

datatype 'a assn = 
    Aemp                                           (* Empty heap *)
  | Apointsto exp exp    (infixl "⟼" 200)        (* Singleton heap *)
  | Astar "'a assn" "'a assn"      (infixl "**" 100)         (* Separating conjunction *)
  | Awand "'a assn" "'a assn"                                (* Separating implication *)
  | Apure bexp                                     (* Pure assertion *)
  | Aconj "'a assn" "'a assn"                                (* Conjunction *)
  | Adisj "'a assn" "'a assn"                                (* Disjunction *)
  | Aex "('a ⇒ 'a assn)"                            (* Existential quantification *)

这种方式适合全局多态场景，若仅Aex需要灵活类型，方法1更轻量。

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