Well, this is Lisp, so the solution is probably to use a list :)
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)
After that, a list called facts* would contain the elements P and Q :
facts*
==> (P Q)
That's how you would do while prototyping. Of course, you will eventually want to encapsulate everything, with dedicated functions, for example :
(= A (fact 'P))
(= B (theorem '(P) '(Q)))
But now, you want to add a kind of strong typing, since you don't want to mistake a theorem from another list. To achieve this you can define a new type with the 'annotate function :
(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
You now have opaque 'theorem objects. To access their implementation, just use the 'rep function :
It seems to me that anyone can now create theorem's, even if they are not theorems! What I had in mind is more like, ok, I have these 5 operations here on theorems, only these can modify and build new theorems. Then I can somehow close up the type of theorems, and if someone later wants to create a theorem, he has to go through these 5 operations. Here it seems to me that later one can just call (annotate 'theorem something_which_is_not_a_theorem) and get away with it.
What you could do is, you could create an "opaque" function which gives access to your theorem data. Then wrap that function in an 'annotate form.
(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")))
For that matter, since Arc is around "exploratory programming", in principle Arc will not allow anything that limits what the user can do.
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.
lol
Exploratory programming is fine, but I don't need to explore anymore what a theorem is :-)
> "Arc will not allow anything that limits what the user can do"
Obviously this is not true, as Arc limits me such that I cannot create a safe theorem type. What this means is that I cannot let the user directly interact with Arc when building an interactive theorem prover; I have to wrap some kind of protective layer around it, which would probably hinder lots of the exploring!
Well, that's not really the spirit of the language. almkglor's solution with checks in the functions with 'check-that-f-is-valid-theorem is what you should eventually do.
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)))
Now, once you call (theorems-factory), two things happen :
- 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.
The trick here is that you can still create bogus theorem objects (for example by doing (annotate 'theorem 'bogus)), but as they are not added to the 'known* list, they are refused by all your functions. And the user cannot access the 'known* list, so he cannot cheat this way either.
Hmmh, I don't really think it is against the spirit of the language. After all, I think you cannot just annotate arbitrary things to be of type integer (or can you?).
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!
> Hmmh, I don't really think it is against the spirit of the language. After all, I think you cannot just annotate arbitrary things to be of type integer (or can you?).
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
In any case: you can always destructure the annotation wrapper and work with the raw data (probably by using some sort of higher-order function, like combinators), only wrapping it in the annotation type. Sort of like explicit monads.
Garbage collection does not work here if you keep a track of all the defined theorems in a list as 'known*. We would need weak references to achieve this.
You're right. It creates lots of never-freed objects, so that's obviously not a viable solution.
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.
Look at the way macros are implemented : they are nothing more than functions annotated with the 'mac symbol. You can access to the underlying function if you want, by doing (rep while) or do (= mymac (annotate 'mac #\space)) and try to call (mymac). Sure, and then bad things can happen. But nobody does it, because this is senseless, and noone ever got trapped because of this. And having access to this is great because it makes the language simple and hackable.
