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有多危險？

回答

相關問題