Arc Forumnew | comments | leaders | submitlogin
1 point by sacado 6183 days ago | link | parent

Actually, you could probably do that (if you really want to) by overriding the 'annotate function and using a 'locked* list, so that you can only annotate an object with a type name that is not already in the locked* list :

  (redef annotate (type obj)
    (if (mem type locked*)
      (err "This type is locked")
      (old type obj)))
Here, 'old is a "keyword" of 'redef that calls the old version of 'annotate (the unprotected one, that cannot be accessed from outside anymore).


2 points by almkglor 6182 days ago | link

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 6182 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.

-----

1 point by thefifthman 6183 days ago | link

That sounds exactly like what I need. Thanks a lot!

-----