Type Class 实例中的定点函数

Question

我正在尝试在类型 class 实例的上下文中使用定点样式函数，但它似乎不起作用。为了完成这项工作，我还需要做些什么吗？目前，我使用了一种技巧，将函数移到 class 类型之外，并明确声明它为 Fixpoint。然而，这似乎很糟糕。

这是一个简短的例子：

Inductive cexp : Type :=
| CAnd :  cexp -> cexp -> cexp
| COr  :  cexp -> cexp -> cexp
| CProp : bool -> cexp.  

Class Propable ( A : Type ) := { compile : A -> Prop }.

Instance: Propable cexp :=
  { compile c :=
      match c with
      | CAnd x y => (compile x) /\ (compile y)
      | COr x y => (compile x) \/ (compile y)
      | CProp _ => False
      end
  }.

这失败了：

Error: Unable to satisfy the following constraints:
In environment:
c, x, y : cexp

?Propable : "Propable cexp"

要完成这项工作需要做什么？

Answer 1

您可以使用 fix 来做到这一点：

Instance: Propable cexp :=
  { compile := fix compile c :=
      match c with
      | CAnd x y => (compile x) /\ (compile y)
      | COr x y => (compile x) \/ (compile y)
      | CProp _ => False
      end
  }.

让我来说明如何想出它。让我们来看下面的一段代码：

Fixpoint silly n :=
  match n with
  | 0 => 0
  | S n => silly n
  end.

Fixpoint 这是一个白话命令，它使定义看起来更容易一些，但它隐藏了这里发生的事情。事实证明，Coq 实际做的事情是这样的：

Definition silly' :=
  fix self n :=
    match n with
    | 0 => 0
    | S n => self n
    end.

可以在定义后使用Print silly.来验证

Type Class 实例中的定点函数

Fixpoint functions in Type Class Instances

typeclass

coq