Arc Forumnew | comments | leaders | submitlogin
ASK: Axioms of Arc?
3 points by kinnard 2931 days ago | 9 comments
PG variously describes arc as a language built up from axioms. But it is not clear to me from any of the implementations(anarki, arcadia, et cetera) or what I've read of PG's writing what precisely the axioms of arc are(they don't appear to be enumerated anywhere).

"The idea of axiomatizing a programming language is not of course a new one. It's almost as old as the idea of a programming language. In his famous 1960 paper, John McCarthy showed how to do this by defining a language he called Lisp. You may be familiar with it. If you have seven primitive operators (quote, atom, eq, car, cdr, cons, and cond) then you can define in terms of them another function, eval, that acts as a Lisp interpreter . . .

Lately I've been trying to continue where McCarthy's 1960 paper left off. I have long suspected that the main reason Lisp is such a good programming language is that it wasn't designed to be a programming language. It is, rather, a theoretical result. If you try to answer the question, what is the smallest number of operators you need in order to write an interpreter for a language in itself, Lisp is what you get. (At least, it's one thing you get; that is not a very precise question, so there is probably more than one answer.)

. . . Of course, as soon as McCarthy's spec fell into the hands of hackers, all this theorizing was cut short. In Lisp 1.5, read and print were not written in Lisp. Given the hardware available at the time, there is no way they could have been. But things are different now. With present-day hardware you can continue till you have a runnable spec for a complete programming language. So that's what I've been doing.

The question I'm trying to answer at the moment is, what operators do you have to add to the original seven in order to be able to write an eval for a complete programming language?

Well, that of course depends on what you mean by a complete programming language. But I think there are some features everyone would agree were necessary. We need to have I/O, for example, for our programs even to get into the computer to be evaluated. We need to have some plan for dealing with errors. (McCarthy's original eval assumes its argument is a correct program. If you refer to an unbound variable, it goes into an infinite loop.) And we need to have more data types than symbols and conses. We'll probably want numbers, for example.

I'm not finished yet with this exercise, but so far I've been surprised by how few primitives you need to add to the core in order to make these things work. I think all you need to define new types is three new primitives (plus assignment and lexical scope). One of the new primitives replaces the original atom, so you still only end up with nine total."

So, what are the axioms of arc?



4 points by Pauan 2931 days ago | link

I took a look through ac.scm, and here are the axioms I found:

* These built-in types: cons sym fn char string int num table output input socket exception thread

* Function calls

* First class lexically scoped functions, including closures (this one has a very complex implementation)

* Required function arguments, optional function arguments, rest function arguments, list destructuring

* Tail call elimination

* Macros (which are just functions annotated with a type of 'mac)

* First-class undelimited continuations (this one has a very complex implementation)

* These special forms: quote quasiquote if fn assign

* Special compiler optimizations for these functions: compose complement andf

* Ssyntax ~ : & (which expands to complement, compose, andf)

* Ssyntax . ! (which expands to function call, function call + quote)

* [ _ ] partial application

* Racket S-expression syntax () [] . ' ` , @ " ; #\ #| |#

* If enabled, you can use atstrings like "foo@bar" which is equivalent to (+ "foo" bar)

* These built-in functions: is < > + - * / mod expt sqrt apply cons car cdr err len annotate type rep uniq ccc infile outfile instring outstring inside stdout stdin stderr call-w/stdin call-w/stdout readc readb peekc writec writeb write disp sread coerce open-socket socket-accept setuid new-thread kill-thread break-thread current-thread sleep pipe-from table maptable protect rand dir file-exists dir-exists rmfile mvfile macex macex1 eval on-err details scar scdr sref bound newstring trunc exact msec current-process-milliseconds current-gc-milliseconds seconds client-ip atomic-invoke dead flushout ssyntax ssexpand quit close force-close memory declare timedate sin cos tan asin acos atan log

* These built-in variables: sig nil t

* Threads and atomics

* Sockets and file I/O

* Exception handling (err and on-error)

I might have missed a few things, but that covers most of it.

-----

1 point by kinnard 2931 days ago | link

Very thorough. That's 19 though, and some of them don't seem very axiomatic.

-----

2 points by Pauan 2931 days ago | link

It's far more than 19.

13 types + 5 special forms + 1 global variable + 92 built-in functions.

And that's not including things such as first-class functions, lexical scope, first-class continuations, tail call elimination, or macros. I don't even know how to count those.

The fact is that practical programming languages need a lot of axioms. If you look at the list of built-in functions, they are all useful, and most of them are for I/O, which cannot be written in an axiomatic way.

I think it would be interesting to write an "eval" function in Arc, and see how few functions it needs in order to accomplish it. But I don't see much practical benefit to it.

-----

2 points by kinnard 2930 days ago | link

I thought that was the whole thing that pg was arguing/exploring. 'What's the least number of axioms necessary for a practical programming language?' And that arc was the product of that exercise.

"Of course, as soon as McCarthy's spec fell into the hands of hackers, all this theorizing was cut short. In Lisp 1.5, read and print were not written in Lisp. Given the hardware available at the time, there is no way they could have been. But things are different now. With present-day hardware you can continue till you have a runnable spec for a complete programming language. So that's what I've been doing.

The question I'm trying to answer at the moment is, what operators do you have to add to the original seven in order to be able to write an eval for a complete programming language? I'm not finished yet with this exercise, but so far I've been surprised by how few primitives you need to add to the core in order to make these things work. I think all you need to define new types is three new primitives (plus assignment and lexical scope). One of the new primitives replaces the original atom, so you still only end up with nine total."

-----

3 points by Pauan 2930 days ago | link

There are two questions here:

1) What is the least number of axioms needed for a practical language?

2) What is the least number of axioms needed to write an evaluator for the language in the language itself?

As I demonstrated, you need a lot of axioms to support practical programming, because practical programming involves I/O, threads, sockets, exceptions, etc.

Trying to find the smallest axioms necessary for I/O is a cool idea. But any I/O axioms will be intimately tied to the hardware, and the hardware is currently more C based than Lisp based. So the result won't be very elegant.

If you ignore practical programming and I/O, and only care about mathematical elegance, then McCarthy's original Lisp is already a quite good answer for question number 2.

Arc is quite a bit more elegant than most other programming languages, but at the end of the day it is still a practical language.

So my question to you is: what are you looking for?

-----

2 points by kinnard 2930 days ago | link

I'm wondering first, exactly what axioms pg settled on. And I'm also curious as you've described it, if the hardware were built for the language and rather than the language being built for the hardware, "what is the least number of axioms need for a practical language".

-----

3 points by Pauan 2930 days ago | link

I can't really answer that. Somebody would need to write an "eval" function in Arc. That would give you a pretty good starting point for figuring out how many axioms you need.

-----

2 points by rocketnia 2930 days ago | link

Well... the axioms of Arc are enumerated in the source code. But that might not be satisfying unless you think Racket is a simple metatheory. :)

Even mathematical axiom systems are always in terms of some metatheory, and the metatheory itself might be in doubt. There's no right answer.

That said, Arc's implementation in terms of Racket is rather large and ad-hoc, and Racket's own implementation is rather large and ad-hoc. There are nicer foundations than these already, like Martin-Löf type theory.

-----

4 points by kinnard 2926 days ago | link

By the way: pg responded via email saying: "I'm not sure yet. Give me another year or so."

-----