阿格达的"严格积极"

Question

我正在尝试根据我在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有关的错误,因为;

值并非严格为正,因为它出现在Value定义中构造函数FunVal类型中箭头的左侧.

这是什么意思？我可以用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需要所有函数总计. 以下是 @gallais使用coinductive偏好类型来实现此目的的示例.