5

これが私が理解していることです：それは任意のandRelation.Binary.PropositionalEquality.TrustMe.trustMeを取るようです、そして：xy

  • xとyが真に等しい場合、refl
  • そうでない場合は、 のように動作しpostulate lie : x ≡ yます。

さて、後者の場合、Agda を簡単に矛盾させる可能性がありますが、これ自体はそれほど問題ではありません。これtrustMeは、使用する証明が権威への訴えによる証明であることを意味するだけです。さらに、そのようなものを使用して を書くことはできますが、(少なくとも Cc Cn によれば) 還元されないcoerce : {A B : Set} -> A -> Bケースであることが判明するため、Haskell のセマンティック ストンピングとは実際には類似していません。coerce {ℕ} {Bool} 0unsafeCoerce

それで、私は何を恐れなければなりませんtrustMeか？一方、プリミティブの実装以外で使用する理由はありますか?

4

1 に答える 1

6

実際に、trustMewhich で評価されないパターン マッチを試みると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 にコンパイルする場合、決定的な違いが 1 つあります。module を見ると、次の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) をコンパイルし、結果の実行可能ファイルを実行すると、... ご想像のとおり、segfault が発生します。

代わりに仮定を使用すると、次のようになります。

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

(少なくとも MAlonzo を使用して) プログラムをコンパイルするつもりがない場合は、矛盾が唯一の懸念事項です (一方、プログラムのタイプチェックのみを行う場合、通常、矛盾は一種の大きな問題です)。

現時点で考えられるユースケースは 2 つあります。1 つ目は (おっしゃる通り) プリミティブを実装する場合です。標準ライブラリは3 つの場所で使用します: s (モジュール)、s (モジュール)、およびs (モジュール) のtrustMe決定可能な等価性の実装。NameReflectionStringData.StringCharData.Char

2 つ目は最初のものとよく似ていますが、データ型と等値関数を自分で指定し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 に答える