28

我正在尝试根据我在 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 不是严格正数，因为它出现在 Value 定义中构造函数 FunVal 类型中箭头的左侧。

这是什么意思？我可以在 Agda 中编码吗？我是不是走错了路？

谢谢。

4

1 回答 1

34

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 需要所有函数是完全的。 这是@gallais 的一个示例，它使用了一种共归纳偏性类型来实现这一点。

于 2010-04-06T09:04:40.577 回答