First, you would implement theorems as a pair of lists : a list for preconditions, one for consequences. Thus, A would be coded as '(nil . (P)) (no precondition, one consequence, i.e. a fact) and B as '((P) . (Q)) (one condition, one consequence) :

  (= A '(nil . (P)))
  (= B '((P) . (Q)))
  (modus-ponens A B)

  facts*
  ==> (P Q)

  (= A (fact 'P))
  (= B (theorem '(P) '(Q)))

  (def fact (name)
    (annotate 'theorem (cons nil (list name))))

  (def theorem (pre post)
    (annotate 'theorem (cons pre post)))

  (= A (fact 'P))
  (= B (theorem '(P) '(Q)))
  (type A)
  ==> theorem

  (modus-ponens A (cons 'x 'y))
  ==> Type error

  (rep A)
  ==> '(nil . (P))

  (def theorem (f)
    (if (check-that-f-is-valid-theorem f)
        (annotate 'theorem
          (fn (cmd)
            (case cmd
              get
                f
              something-else
                (do-something-on f))))
        (error "Not a valid theorem")))

In practice, most users are too busy working on stuff to bother doing something as stupid as (annotate 'theorem something_which_is_not_a_theorem) anyway.

> "Arc will not allow anything that limits what the user can do"

Which is an admitted problem in current Arc: it forces you to explore well-explored areas sometimes.

> I have to wrap some kind of protective layer around it, which would probably hinder lots of the exploring!

Standard answer: macros.

If you really want a stronger encapsulation, there is only one solution (I think) : using closures to keep a list of known, certified theorems.

  (def theorems-factory ()
    (let known* nil
      (def mk-theorem (pre post)
        (let result (annotate 'theorem (cons pre post))
          (push result known*)
          result))
      (def is-valid (theorem)
        (mem theorem known*))
      (def modus-ponens (a b)
        (unless (and (is-valid a) (is-valid b))
           (err "Type error"))
        (do-the-work-with a b))))

  (theorems-factory)
  (= A (mk-theorem nil '(P)))
  (= B (mk-theorem '(P) '(Q)))

- the list of certified theorems is made (and empty)

- a bunch of functions (the only ones authorized to deal with your type) are defined.

Then, you can call the theorem constructor 'mk-theorem and other functions on these built constructors.

Yes, you can: (annotate 'int #\newline). It won't be useful, but yes, you can.

> The above solution would surely work in principle, but in practice I create millions of intermediate theorems, I do not want to store all of them!

Standard answer: Garbage collection

What are you trying to prevent ? If you're trying to prevent the use of malicious data into one of your functions (e.g. a theorem object you got from an untrusted network) you could use some kind of cryptographic mark in your objects (something that proves they have been made by your constructor function, e.g. implement theorems as closures whose actual data can only be decyphered when called with a given private key), but Arc is certainly not the language you should uyse in this case (better use Java in such situations).

If, and that's what I guess you want, you just want to protect the user from blowing his own leg off by providing wrong data to functions, almkglor's wrapper solution, with macros to simplify coding, is the way to go. You can end up with a very transparent solution if you do it right. Of course, a determined user will eventually be able to break it down if he really wants to, but that's the philosophy of the language.

http://arcfn.com/doc/table.html#obj http://arcfn.com/doc/template.html

macros are pretty good for language-type thingies since they let you parse the raw input. this could be done as an interface layer on top of the actual mechanisms so you could write things like:

  (logic A -> B
         A)

Why not introduce a safe type definition mechanism as follows:

(def_opaque_type MYTYPE mytype_operation_definition_1 mytype_operation_definition_2 .... mytype_operation_definition_n)

  (redef annotate (type obj)
    (if (mem type locked*)
      (err "This type is locked")
      (old type obj)))

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)))))

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

  (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)))))))

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.