Re: Axiom musings...

[Tim Daly]

The Axiom SANE compiler / interpreter has a few design points.

1) It needs to mix interpreted and compiled code in the same function.
SANE allows dynamic construction of code as well as dynamic type
construction at runtime. Both of these can occur in a runtime object.
So there is potentially a mixture of interpreted and compiled code.

2) It needs to perform type resolution at compile time without overhead
where possible. Since this is not always possible there needs to be
a "prefix thunk" that will perform the resolution. Trivially, for example,
if we have a + function we need to type-resolve the arguments.

However, if we can prove at compile time that the types are both
bounded-NNI and the result is bounded-NNI (i.e. fixnum in lisp)
then we can inline a call to + at runtime. If not, we might have
+ applied to NNI and POLY(FLOAT), which requires a thunk to
resolve types. The thunk could even "specialize and compile"
the code before executing it.

It turns out that the Forth implementation of "threaded-interpreted"
languages model provides an efficient and effective way to do this.[0]
Type resolution can be "inserted" in intermediate thunks.
The model also supports dynamic overloading and tail recursion.

Combining high-level CLOS code with low-level threading gives an
easy to understand and robust design.

Tim

[0] Loeliger, R.G. "Threaded Interpretive Languages" (1981)
ISBN 0-07-038360-X




On 2/5/21, Tim Daly <axiomcas@gmail.com> wrote:
> I've worked hard to make Axiom depend on almost no other
> tools so that it would not get caught by "code rot" of libraries.
>
> However, I'm also trying to make the new SANE version much
> easier to understand and debug.To that end I've been experimenting
> with some ideas.
>
> It should be possible to view source code, of course. But the source
> code is not the only, nor possibly the best, representation of the ideas.
> In particular, source code gets compiled into data structures. In Axiom
> these data structures really are a graph of related structures.
>
> For example, looking at the gcd function from NNI, there is the
> representation of the gcd function itself. But there is also a structure
> that is the REP (and, in the new system, is separate from the domain).
>
> Further, there are associated specification and proof structures. Even
> further, the domain inherits the category structures, and from those it
> inherits logical axioms and definitions through the proof structure.
>
> Clearly the gcd function is a node in a much larger graph structure.
>
> When trying to decide why code won't compile it would be useful to
> be able to see and walk these structures. I've thought about using the
> browser but browsers are too weak. Either everything has to be "in a
> single tab to show the graph" or "the nodes of the graph are in different
> tabs". Plus, constructing dynamic graphs that change as the software
> changes (e.g. by loading a new spad file or creating a new function)
> represents the huge problem of keeping the browser "in sync with the
> Axiom workspace". So something more dynamic and embedded is needed.
>
> Axiom source gets compiled into CLOS data structures. Each of these
> new SANE structures has an associated surface representation, so they
> can be presented in user-friendly form.
>
> Also, since Axiom is literate software, it should be possible to look at
> the code in its literate form with the surrounding explanation.
>
> Essentially we'd like to have the ability to "deep dive" into the Axiom
> workspace, not only for debugging, but also for understanding what
> functions are used, where they come from, what they inherit, and
> how they are used in a computation.
>
> To that end I'm looking at using McClim, a lisp windowing system.
> Since the McClim windows would be part of the lisp image, they have
> access to display (and modify) the Axiom workspace at all times.
>
> The only hesitation is that McClim uses quicklisp and drags in a lot
> of other subsystems. It's all lisp, of course.
>
> These ideas aren't new. They were available on Symbolics machines,
> a truly productive platform and one I sorely miss.
>
> Tim
>
>
>
> On 1/19/21, Tim Daly <axiomcas@gmail.com> wrote:
>> Also of interest is the talk
>> "The Unreasonable Effectiveness of Dynamic Typing for Practical Programs"
>> https://vimeo.com/74354480
>> which questions whether static typing really has any benefit.
>>
>> Tim
>>
>>
>> On 1/19/21, Tim Daly <axiomcas@gmail.com> wrote:
>>> Peter Naur wrote an article of interest:
>>> http://pages.cs.wisc.edu/~remzi/Naur.pdf
>>>
>>> In particular, it mirrors my notion that Axiom needs
>>> to embrace literate programming so that the "theory
>>> of the problem" is presented as well as the "theory
>>> of the solution". I quote the introduction:
>>>
>>>
>>>
>>> This article is, to my mind, the most accurate account
>>> of what goes on in designing and coding a program.
>>> I refer to it regularly when discussing how much
>>> documentation to create, how to pass along tacit
>>> knowledge, and the value of the XP's metaphor-setting
>>> exercise. It also provides a way to examine a methodolgy's
>>> economic structure.
>>>
>>> In the article, which follows, note that the quality of the
>>> designing programmer's work is related to the quality of
>>> the match between his theory of the problem and his theory
>>> of the solution. Note that the quality of a later programmer's
>>> work is related to the match between his theories and the
>>> previous programmer's theories.
>>>
>>> Using Naur's ideas, the designer's job is not to pass along
>>> "the design" but to pass along "the theories" driving the design.
>>> The latter goal is more useful and more appropriate. It also
>>> highlights that knowledge of the theory is tacit in the owning, and
>>> so passing along the thoery requires passing along both explicit
>>> and tacit knowledge.
>>>
>>> Tim
>>>
>>
>