Насколько опасен TrustMe?

Вот что я понимаю о 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? С другой стороны, есть ли причина использовать его вне реализации примитивов?


agda
person Ben Millwood    schedule 16.12.2013    source источник

Ответы (1)


arrow_upward
5
arrow_downward

Действительно, попытка сопоставления с образцом для 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) и запустив полученный исполняемый файл, мы получим... как вы правильно догадались - segfault.

Если мы вместо этого используем постулат, мы получим:

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, компилятор не сможет вас спасти.

person Vitus    schedule 16.12.2013