trustMe有多危险？

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并没有减少(至少不是根据Cc Cn),所以它实际上并不像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在三个地方使用:实现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,编译器无法保存.