我最近问过这个问题: 该类型中使用的agda命题 - 它是什么意思？ 并收到了一个非常深思熟虑的答案,关于如何使类型隐式并获得真正的编译时错误.
但是,我仍然不清楚如何使用依赖类型创建值.
考虑:
div : (n : N) -> even n -> N
div zero p = zero
div (succ (succ n)) p= succ (div n p)
div (succ zero) ()
其中N是自然数,甚至是以下命题.
even : N -> Set
even zero = \top
even (succ zero) = \bot
even (succ (succ n)) = even n
data \bot : Set where
record \top : Set where
假设我想写一个函数如下:
f : N -> N
f n = if even n then …已经说明了所有agda程序终止的几个地方.但是我可以构造一个这样的函数:
stall : ? n ? ?
stall 0 = 0
stall x = stall x
语法高亮显示器似乎不喜欢它,但没有编译错误.
计算stall 0结果的正常形式0.计算结果stall 1导致Emacs挂起看起来很像非终止循环.
这是一个错误吗？或者Agda有时会永远运行？或者是更微妙的事情？