You can also download Anarki, an unofficial improvement of arc2 (mostly bug fixes, a few experimental ideas and a few more libraries), available here http://github.com/nex3/arc/tarball/master .

Personally, I think you really should use Anarki as it is more mature, but is still compatible with the official arc2 (and most people here would tell you so), but it's up to you.

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.

2- is a good starting point. For exn:fail, that the same as for 1- : not a top priority, particularily as it is not yet implemented in canonical arc.

- PUSH the closure to be called

- PUSH the list of args

- call the APPLY() function, which just POPs the two elements, PUSHes all the elements of the arg list one after one, then call the closure (maybe after changing the continuation argument of that closure by hand, at runtime) ?

That's a runtime behavior, for sure, and probably a few cases should be hard-coded in the generated C file. E.g., (apply + '(1 2)) should be translated to (+ 1 2), then to 3, if nothing bad (redefinition of '+ or 'apply by the user) happened. But in the general case, you can't know.

> - PUSH the closure to be called

> - PUSH the list of args

> - call the APPLY() function, which just POPs the two elements, PUSHes all the elements of the arg list one after one, then call the closure (maybe after changing the continuation argument of that closure by hand, at runtime) ?

Which continuation argument do you pass?

Suppose it's like this:

  (%car (%apply foo bar))

  (set foo
    (fn (a b)
      (ccc
        (fn (k)
          (a k b)))))

Remember, calling a function consists of the following steps:

1. Push the closure

2. Push the continuation

3. Push the arguments

The problem is step 2: continuation.

Possibly we need to insert the default 'apply during the same step as inserting the default 'ccc ? Then we could define '%apply as accepting the function, the continuation, and a plain list of arguments.

> Anyway, we will eventually have to implement an interpreter in the generated code, to deal with dynamic stuff. Maybe closures should be made available through a hashtable mapping their name(s) to actual code, and not only through a hard-coded array as it is now ?

s/closure/global variable/, maybe?

I don't know if interning strings would really kill performance. Lua does it if I remember well, and it is quite performant. Anyway, mutable strings are a real performance killer, since you must compare them with scheme's 'equal? instead of 'eq?.

Now, you are right too, they don't represent exactly the same thing, so simply removing one of them would quite feel bad, but sometimes you have to make both worlds communicate. That's a matter of syntax too. After all, "Hello, Arc world" could be a special syntax meaning : the quotation of the symbol |Hello,\ Arc\ world|. A triple-quote syntax could be added, too.

It can be said the other way around : every time you need a string and are provided with a symbol (or the opposite), an automatic coercion could be performed.

As an aside: maybe it's better to make the primitives really, really primitive?

Basically we define separate %n+ for adding two fixnums, %f+ for adding two flonums, %fn+ for adding a flonum and a fixnum (in that order) and, %nf+ for adding a fixnum and a flonum (in that order).

Then we can write + in lib-ac.scm.arc as:

  (set +
    (fn rest
      ($+ rest)))
  (set $+
    (fn (args)
      (if args
          (if (%cdr args)
              ($sub+ (%car args) (%cdr args))
              (%car args))
          0)))
  (set $sub+
    (fn (accum rest)
      (if rest
          ((fn (val rest)
             (if (%is (%type accum) 'int)
                 (if (%is (%type val) 'int)
                     ($sub+ (%n+ accum val) rest)
                     (if (%is (%type val) 'num)
                         ($sub+ (%nf+ accum val) rest)
                         ; raise exception
                         ()))
                 (if (%is (%type accum) 'num)
                     (if (%is (%type val) 'int)
                         ($sub+ (%fn+ accum val) rest)
                         (if (%is (%type val) 'num)
                             ($sub+ (%f+ accum val) rest)
                             ; raise exception
                             ()))
                     ; raise exception
                     ())))
            (%car rest) (%cdr rest))
          accum)))

Now, macros. I tried to think about it yesterday, and I don't really understand why you need this protected mode. I mean, macros have to be defined (globally) before they are called and treated as such. Since you can already identify all the globals (and since a macro is a global thing annotated by 'mac), it should be easy to

- make a list of all the symbols holding a macro at a given moment in the code

- explore all the sexprs to see if one of those symbols is the first element of any sublist

- if it is to, make the transformation

- do it again until nothing changes anymore

  (do
    (= xe 0)
    (mac somethingstupid ()
      (= xe (+ xe 1))
      `(prn "something stupid" ,xe)))

If I understand well, we have to interpret the code as we compile it (as a macro's body is executed when a function is defined/compiled, not when executed) ? To me, macros were something translating a piece of code into another one, period. But that's not always the case as your example shows. If someone writes

  (mac foo
    (prn "blah"))

  (def bar (n)
    (foo) (* n 2))

The global environment is shadowed by a table; when this table is accessed, if a table entry does not exist, we look it up in the real environment using 'eval (!!) and retain a copy. This allows the macro to use stuff like 'map.

Edit: Also, it might be useful to organize the primitives as "functions", like what I did with cons_fun().

So:

  #define CONS() {obj d = POP(); TOS() = cons_fun(TOS(), d);}

  (%cons foo (%car bar))
  ==>
  PUSH(cons_fun(foo, car_fun(bar)));

  QUOTE_CONSTANT[0] = cons_fun(FIX2OBJ(1),cons_fun(FIX2OBJ(2),NILOBJ))

Called the "Arc stack", maybe? ^^

Currently this is what is done:

  QUOTE_CONSTANTS[0] = cons_fun(FIX2OBJ(1),cons_fun(FIX2OBJ(2),NILOBJ))

  PUSH(FIX2OBJ(1));
  PUSH(FIX2OBJ(2));
  PUSH(NILOBJ);
  CONS();
  CONS();
  QUOTE_CONSTANTS[0] = POP();

  (car (cdr foo))

  PUSH(car_fun(cdr_fun(LOCAL(3)/*foo@42*/)));

  #define car_fun(o) (((pair *)(o))->car)

  (= sum 0 count 0)

  (def strn (length str (o before t))
    (let result str
      (while (< (len result) length)
        (= result (if before (+ " " result) (+ result " "))))
      result))

  (strn 4 "10") ==> "  10"
  (strn 4 "10" t) ==> "10  "

  (* "=" 5) ==> "====="

  (redef * args
    (if (and (is (len args) 2) (isa args.0 'string) (isa args.1 'int))
      (let result ""
        (for i 1 args.1
          (= result (+ result args.0)))
        result)
      (apply old args)))

  (def action (index user score)
    (prn (strn 2 index) ". " (strn 15 user nil) " = " (strn 4 score))
    (++ sum (coerce score 'int))
    (++ count))

  (w/infile f "arcleaders.html"
    (pmatch "(\\d\\d?)\\..*?.+?<u>(.+?)<\\/u>.+?(\\d+)" action))
  (prn (* "=" 26))
  (prn "Total   = " (strn 4 (coerce sum 'string)))
  (prn "Average = " (strn 4 (coerce (/ sum count) 'string)))

Also, I think you may have forgotten to read the file. w/infile only opens the file, right?

  (w/infile f "arcleaders.html"
      (while (< count 10) (pmatch f "(\\d\\d?)\\..*?.+?<u>(.+?)<\\/u>.+?(\\d+)" action)))

With the Ruby example, the scan function invokes the supplied block repeatedly, but the break statement within the block will exit the scan function which is the desired behavior.