Arc Forumnew | comments | leaders | submitlogin
2 points by almkglor 6241 days ago | link | parent

And how do you unlock it for the constructors that are supposed to do the proper locking?

Hmm.

  (let real-annotate annotate
    (def theorem (f)
      (if (check-f-is-valid-theorem f)
          (real-annotate 'theorem f)
          (err "Not a valid theorem")))
    (= annotate 
       (fn (type obj)
         (if (is type 'theorem)
             (err "Spank!  Spank!  Under the boots of your master!!")
             (real-annotate tpye obj)))))
It does have the drawback that you can't, say, reload the file, but hey, you did say you didn't want anyone else to create theorems except by that method, so even redefining that method won't work!


2 points by almkglor 6241 days ago | link

Okay, here's a better way of presenting it:

  (def-B&D-type theorem create-theorem (f)
    (if (check-f-is-valid-theorem f)
        (annotate 'theorem f)
        (err "Not a valid theorem")))
Where def-B&D-type is:

  (mac def-B&D-type (type constructor . body)
    (w/uniq real-annotate
      `(let ,real-annotate annotate
         (let annotate ,real-annotate
           (def ,constructor ,@body))
         (= annotate
            (fn (type obj)
              (if (is type ',type)
                  (err "Spank!  Spank!  Under the boots of your master!!")
                  (,real-annotate type obj)))))))
Note however that even under this, it's still possible to redefine 'check-f-is-valid-theorem.

For that matter, it's still possible to defeat "safety" in language X: just implement a version of language X which doesn't have that safety.

In practice, nobody will bother to do (annotate 'foo something-which-is-not-a-foo) anyway.

-----