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.
