haskell - Agda “Strictly positive”

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

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

在阿格达，直接翻译是；

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

但是我收到一个与FunVal有关的错误，因为；



这是什么意思？我可以在Agda中编码吗？我会以错误的方式处理吗？

谢谢。

最佳答案

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的原因，它使用共归性偏爱类型来完成此任务。

关于haskell - Agda “Strictly positive”，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/2583337/