agda - 信任我有多危险？

Question

以下是我对 Relation.Binary.PropositionalEquality.TrustMe.trustMe 的理解: 好像是任意的x和 y ， 和:

如果 x和 y真正相等，它变成refl

如果不是，它的行为类似于 postulate lie : x ≡ y .

现在，在后一种情况下，它很容易使 Agda 不一致，但这本身并不是什么大问题:它只是意味着任何使用 trustMe 的证明是诉诸权威的证明。而且，虽然你可以用这样的东西来写coerce : {A B : Set} -> A -> B , 结果是 coerce {ℕ} {Bool} 0不会减少(至少，不是根据 C-c C-n)，所以它真的不像 Haskell 的语义踩踏 unsafeCoerce .

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

Answer 1

实际上，尝试在 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

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

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

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

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

目前我可以想到两个用例，第一个是(如您所说)用于实现原语。标准库使用 trustMe在三个地方:在 Name 的可判定平等实现中s(Reflection 模块)，String s(Data.String 模块)和 Char s(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 ，编译器无法拯救你。