Agda的“严格正面”
我试图根据我在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定义中的构造函数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 ww会让您再次apply ww 。 术语apply ww没有标准格式，这在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编码也不起作用。 你不能将无类型的lambda微积分嵌入到Agda中，因为它具有没有正常形式的术语，并且Agda要求所有程序正常化。
链接地址: http://www.djcxy.com/p/43339.html