haskell - Agda 中的"Strictly positive"

Question

我正在尝试根据我用 Haskell 编写的程序将一些指称语义编码到 Agda 中。

data Value = FunVal (Value -> Value)
           | PriVal Int
           | ConVal Id [Value]
           | Error  String

在 Agda 中，直接翻译为:

data Value : Set where
    FunVal : (Value -> Value) -> Value
    PriVal : ℕ -> Value
    ConVal : String -> List Value -> Value
    Error  : String -> Value

但我收到与 FunVal 相关的错误，因为；

Value is not strictly positive, because it occurs to the left of an arrow in the type of the constructor FunVal in the definition of Value.

这是什么意思？我可以用 Agda 对其进行编码吗？我的处理方式是否错误？

谢谢。

Answer 1

HOAS在 Agda 中不起作用，因为:

apply : Value -> Value -> Value
apply (FunVal f) x = f x
apply _ x = Error "Applying non-function"

w : Value
w = FunVal (\x -> apply x x)

现在，请注意，计算 apply w w 会让您再次 apply w w 回来。术语 apply w w 没有范式，这在 agda 中是禁忌。使用这个想法和类型:

data P : Set where
    MkP : (P -> Set) -> P

我们可以得出一个矛盾。

摆脱这些悖论的方法之一是只允许严格的正递归类型，这就是 Agda 和 Coq 所选择的。这意味着如果您声明:

data X : Set where
    MkX : F X -> X

F 必须是严格正仿函数，这意味着 X 永远不会出现在任何箭头的左侧。所以这些类型在 X 中是严格正数的:

X * X
Nat -> X
X * (Nat -> X)

但这些不是:

X -> Bool
(X -> Nat) -> Nat  -- this one is "positive", but not strictly
(X * Nat) -> X

所以简而言之，不，你不能在 Agda 中表示你的数据类型。您可以使用 de Bruijn 编码来获取可以使用的术语类型，但通常评估函数需要某种“超时”(通常称为“燃料”)，例如评估的最大步骤数，因为 Agda 要求所有函数都是总计的。 Here is an example由于@gallais 使用共归纳偏爱类型来完成此操作。