trustMe有多危险？

这里是我了解Relation.Binary.PropositionalEquality.TrustMe.trustMe：它似乎采取任意x和y，并且：trustMe有多危险？

如果x和y是真正平等的，它成为refl
如果他们不，它像postulate lie : x ≡ y 。

现在，在后一种情况下，它可以很容易地阿格达不一致，但是这本身是没有这么多的问题：它只是意味着使用trustMe任何证明是诉诸权威证明。此外，尽管你可以用这样的东西来写coerce : {A B : Set} -> A -> B，但事实证明coerce {ℕ} {Bool} 0并没有减少（至少，不是根据Cc Cn），所以它和Haskell的语义跺。

那么我需要从trustMe恐惧什么？另一方面，是否有理由在实现原语之外使用它？

来源

2013-12-16 Ben Millwood

事实上，试图在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不definitionally相等，则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，编译器不能保存你。

来源

2013-12-16 03:20:27 Vitus

trustMe有多危险？

回答

相关问题