5

这就是我所理解的Relation.Binary.PropositionalEquality.TrustMe.trustMe：它似乎需要一个任意的xandy和：

  • 如果x和y真正相等，则变为refl
  • 如果不是，它的行为就像postulate lie : x ≡ y.

现在，在后一种情况下，它很容易使 Agda 不一致，但这本身并不是一个问题：它只是意味着任何使用trustMe的证明都是诉诸权威的证明。而且，虽然你可以用这样的东西来写coerce : {A B : Set} -> A -> B，但事实证明，情况coerce {ℕ} {Bool} 0并没有减少（至少，不是根据 Cc Cn），所以它真的不像 Haskell 的语义跺脚unsafeCoerce。

那我有什么好害怕的trustMe？另一方面，有没有理由在实现原语之外使用它？

4

1 回答 1

6

实际上，尝试在trustMe其上进行不评估的模式匹配会refl导致术语卡住。看到（部分）定义后面的原始操作的代码，也许是有启发性trustMe的primTrustMe：

(u', v') <- normalise (u, v)
if (u' == v') then redReturn (refl $ unArg u) else
  return (NoReduction $ map notReduced [a, t, u, v])

在这里，u和分别v代表术语x和y。其余代码可以在模块中找到Agda.TypeChecking.Primitive。

所以是的，如果x和y在定义上不相等，那么primTrustMe（并且通过扩展trustMe）在评估只是卡住的意义上表现为一个假设。然而，在将 Agda 编译为 Haskell 时，有一个关键的区别。看一下模块Agda.Compiler.MAlonzo.Primitives，我们发现这段代码：

("primTrustMe"       , Right <$> do
       refl <- primRefl
       flip runReaderT 0 $
         term $ lam "a" (lam "A" (lam "x" (lam "y" refl))))

这看起来很可疑：refl无论如何x它总是会返回y。让我们有一个测试模块：

module DontTrustMe where

open import Data.Nat
open import Data.String
open import Function
open import IO
open import Relation.Binary.PropositionalEquality
open import Relation.Binary.PropositionalEquality.TrustMe

postulate
  trustMe′ : ∀ {a} {A : Set a} {x y : A} → x ≡ y

transport : ℕ → String
transport = subst id (trustMe {x = ℕ} {y = String})

main = run ∘ putStrLn $ transport 42

使用trustMeinside transport，编译模块 ( C-c C-x C-c) 并运行生成的可执行文件，我们得到......你猜对了 - 一个段错误。

如果我们改为使用假设，我们最终会得到：

DontTrustMe.exe: MAlonzo Runtime Error:
    postulate evaluated: DontTrustMe.trustMe′

如果您不打算编译您的程序（至少使用 MAlonzo），那么您唯一需要担心的是不一致（另一方面，如果您只对程序进行类型检查，那么不一致通常是个大问题）。

目前我可以想到两个用例，第一个是（如您所说）用于实现原语。标准库trustMe在三个地方使用：在实现Names（Reflection模块）、Strings（Data.String模块）和Chars（Data.Char模块）的可判定相等性中。

第二个很像第一个，除了你自己提供数据类型和等式函数，然后使用trustMe它跳过证明，只使用等式函数来定义一个可判定的等式。就像是：

open import Data.Bool
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary

data X : Set where
  a b : X

eq : X → X → Bool
eq a a = true
eq b b = true
eq _ _ = false

dec-eq : Decidable {A = X} _≡_
dec-eq x y with eq x y
... | true  = yes trustMe
... | false = no whatever
  where postulate whatever : _

但是，如果你搞砸了eq，编译器也救不了你。

于 2013-12-16T03:20:27.433 回答