按照这种方法，我尝试基于 Haskell 中的实现，在 Coq 中使用效果处理程序对函数式程序进行建模。论文中提出了两种方法：
data Prog sig a = Return a | Op (sig (Prog sig a))
由于终止检查不喜欢非严格肯定的定义，因此无法直接定义此数据类型。但是，容器可用于表示严格正函子，如本文所述。这种方法有效，但由于我需要对需要显式作用域语法的作用域效果进行建模，因此可能会出现不匹配的开始/结束标记。对于程序的推理，这并不理想。
data Prog sig a = Return a | Op (sig (Prog sig) a)
现在 sig 的类型为 (* -> *) -> * -> *。由于与之前相同的原因，无法在 Coq 中定义数据类型。我正在寻找对这种数据类型进行建模的方法，以便我可以在没有显式作用域标记的情况下实现作用域效果。
我为高阶函子定义容器的尝试没有取得成果，我找不到关于这个主题的任何信息。我很感谢您提供正确方向的指示和有用的评论。
编辑：我想表示的论文中作用域语法的一个示例是以下异常数据类型。
data HExc e m a = Throw? e | forall x. Catch? (m x) (e -> m x) (x -> m a)
Edit2：我已将建议的想法与我的方法合并。
Inductive Ext …我目前正在尝试共享部分应用的功能。为了使共享可见，我使用了描摹效果。为了说明我的问题，我首先展示一个简化的例子。
f1, f2, f3, f4 :: Int -> Int
f1 = \x -> trace "f1" 0 + x
f2 x = trace "f2" 0 + x
f3 = (trace "f3" 0 +)
f4 = (+) (trace "f4" 0)
我在以下场景中比较了这些函数，其中f1由不同的函数代替。
apply :: (Int -> Int) -> (Int -> Int) -> Int
apply f g = f 42 + g 42
result = let f = f1
in apply f f
输出（未经优化编译）如下。
f1 f1 f2 f2 f3 f4 …