Re: [Axiom-developer] [EXTERNAL] Re: Axiom's Sane redesign musings

[Tim Daly]

Temptation...

I would like to remain faithful to Axiom's syntax for signatures

foo: (%,%) -> %

but the world seems to have converged on

foo: % -> % -> %

This shows up everywhere in logic, in haskell, etc.
It allows for a primitive kind of currying, the "right curry"
(Some form of scheme allows currying anywhere in the
argument list, including multiple currying)

I need to logic-style signatures for the axioms so the
tempation is to rewrite the Axiom signatures using the
logic notation.

I can do both but it might be clearer to follow the world
rather than follow our own, given the user base.

Tim


On 7/9/19, Tim Daly <address@hidden> wrote:
> ---------- Forwarded message ----------
> From: Tim Daly <address@hidden>
> Date: Tue, 9 Jul 2019 22:56:24 -0400
> Subject: Re: [EXTERNAL] Re: [Axiom-developer] Axiom's Sane redesign musings
> To: Martin Baker <address@hidden>
>
> Progress is being made. Axiom was written long before Common
> Lisp existed. A lot of the code is due to translations from Maclisp
> and LispVM.
>
> I'm moving the Axiom hierarchy to Common Lisp CLOS code.
> This has several advantages.
>
> It eliminates the databases. They were created because there
> was not enough memory (at 16 megabytes).
>
> It uses native code to do dispatch.
>
> CLOS defclass creates Common Lisp types so all of the code
> is well-typed at the lisp level.
>
> CLOS is lisp so ordinary lisp code can use Axiom functions
> directly. This makes Axiom into an "embeddable library".
>
> CLOS is the target language for the Axiom compiler. The
> compiler is being re-architected to use nano passes [0] for
> compiling. This will make it much easier to maintain in
> the long term and much easier to extend.
>
> This technique allows building the compiler in stages from
> running code to running code at every step.
>
> The new interpreter is much simpler as it just runs the CLOS
> code directly.
>
> The choice of logic and specification languages are still unclear.
> These will also be created first at the lisp level and then covered
> by the compiler with additional nano-passes.
>
> Anyway, coding has begun.
>
> Tim
>
> [0]  Sarker, Dipanwita and Waddell, Oscar and Kybvig, R. Kent
> "A Nanopass Framework for Compiler Education" (2004)
>
>
> On 6/30/19, Tim Daly <address@hidden> wrote:
>> There are thousands of hours of expertise and thousands of
>> functions embedded in Spad code. An important design goal
>> is to ensure that code continues to function. The Sane compiler
>> will output code that runs in the interpreter. It is important that
>> "nothing breaks".
>>
>> That said, the Sane compiler is "layered". The core of the design
>> is that Axiom categories, domains, and packages are represnted
>> as lisp classes and instances. This "core" is essentially what the
>> compiler people call an Abstract Syntax Tree (AST). But in this
>> case it is much more than syntax.
>>
>> Given this "core" there are several tasks.
>>
>> 1) compile spad code to the core. The "front end" should
>> accept and understand current Spad code, unwinding it
>> into the core class structure.
>>
>> 2) compile core classes to Axiom data structures. Thi
>> "back end" generates current Axiom data structures from
>> the core data structures.
>>
>> Now the compiler generates working code yet is in a state
>> to accept enhancements, essentially by extending the core
>> class objects.
>>
>> 3) In the interpreter, modify the getdatabase function to
>> extract data from the core rather than the databases. So
>> the databases go away but the interpreter continues to work.
>>
>> So now the interpreter has been "lifted" onto the core classes
>> but continues to function.
>>
>> 4) enhance the core to support the axioms / specifications /
>> proofs /etc. This involves adding fields to the lisp classes.
>> This core work gives additional fields to hold information.
>>
>> 5) extend the Spad language (Spad 2.0?) to handle the
>> additional axioms / specifications / proofs / etc. This
>> involves adding syntax to the Spad language to support
>> the new fields.
>>
>> 6) build back-end targets to proof systems, spec systems,
>> etc. Compilers like GCC have multiple back ends. The Sane
>> compiler targets the interpreter, a specification checker, a
>> proof system, etc. as separate back ends, all from the same
>> core structures.
>>
>> The Compiler Design
>>
>> A separate but parallel design goal is to build the compiler so
>> it can be type-checked. Each function has typed input and
>> typed output and is, for the most part, purely functional. So,
>> for example, a "Filename" is an instance of a "File" object.
>> A "Line" is an instance of "String". The "FileReader" is
>>
>> FileReader : Filename -> List Line
>>
>> Careful design of the language used to construct hte compiler
>> (as opposed to the Spad language it accepts) makes it easier
>> to type check the compiler itself.
>>
>> By REALLY careful design, the types are build on a layered
>> subset of lisp, like Milawa
>> https://www.cl.cam.ac.uk/~mom22/soundness.pdf
>> which is sound all the way down to the metal.
>>
>> It all goes in stages. Build the new core class structure in a
>> strongly typed fashion. Accept the Spad language. Generate
>> Interpreter code. Enhance the core to support proofs / specs.
>> Enhance the language to support proofs / specs. Accept the
>> new language. Generate back ends to target the interpreter
>> and a proof / spec system. Build it all on a sound base so
>> the compiler can be checked.
>>
>> To the initial end user, the Sane version is the same as the
>> current system. But in the long term all of the Axiom code
>> could be called from any Lisp function. The Sane version
>> can also be used as an "Oracle" for proof systems, since
>> the code has been proven correct.
>>
>> This is a huge project but it can be done in small steps.
>> In particular, the goal is to build a "thin thread" all the way
>> through the system to handle only the GCD algorithms.
>> Once that proof happens "the real work begins".
>>
>> Tim
>>
>>
>>
>>
>> On 6/30/19, Martin Baker <address@hidden> wrote:
>>> Tim,
>>>
>>> This all seems to be about the lisp layer, obviously thats what
>>> interests you.
>>>
>>> It seems to me that if SPAD code is complicated and not aligned to type
>>> theory then, when SPAD is complied to Lisp, the List code will be
>>> complicated and hard to work with. Your previous remarks, about not
>>> seeing the whole elephant, suggest to me that you are drowning in
>>> complexity. Most languages, in their lifetime, acquire some messiness
>>> that needs to be cleared out occasionally.
>>>
>>> Don't you think its time for SPAD 2.0 ?
>>>
>>> Martin
>>>
>>> On 30/06/2019 02:17, Tim Daly wrote:
>>>> One major Sane design decision is the use of CLOS,
>>>> the Common Lisp Object System.
>>>>
>>>> First, since each CLOS object is a type it is possible to
>>>> create strong types everywhere. This helps with the ultimate
>>>> need to typecheck the compiler and the generated code.
>>>>
>>>> Second, CLOS is an integral part of common lisp. One of
>>>> the Sane design goals is to make it possible to use Axiom's
>>>> domains in ordinary lisp programs. Since Axiom is nothing
>>>> more than a domain specific language on common lisp it
>>>> makes sense to construct it so users can freely intermix
>>>> polynomials with non-algebraic code.
>>>>
>>>> Third, CLOS is designed for large program development,
>>>> hiding most of the implementation details and exposing
>>>> a well-defined API. This will make future maintenance and
>>>> documentation of Axiom easier, contributing to its longer
>>>> intended life.
>>>>
>>>> So for a traditional Axiom user nothing seems to have
>>>> changed. But for future users it will be easy to compute
>>>> an integral in the middle of regular programs.
>>>>
>>>> Tim
>>>>
>>>> On 6/27/19, Tim Daly <address@hidden> wrote:
>>>>> Another thought....
>>>>>
>>>>> There has been a "step change" in computer science in the last few
>>>>> years.
>>>>>
>>>>> Guy Steele did a survey of the use of logic notation in conference
>>>>> papers.
>>>>> More than 50% of the papers in some conferences use logic notation
>>>>> (from one of the many logics).
>>>>>
>>>>> CMU teaches their CS courses all based on and requiring the use of
>>>>> logic and the associated notation. My college mathematics covered
>>>>> the use of truth tables. The graduate course covered the use of
>>>>> Karnaugh maps.
>>>>>
>>>>> Reading current papers, I have found several papers with multiple
>>>>> pages containing nothing but "judgements", pages of greek notation.
>>>>> If you think Axiom's learning curve is steep, you should look at
>>>>> Homotopy Type Theory (HoTT).
>>>>>
>>>>> I taught a compiler course at Vassar in the previous century but
>>>>> the Dragon book didn't cover CIC in any detail and I would not
>>>>> have understood it if it did.
>>>>>
>>>>> The original Axiom software predates most of the published logic
>>>>> papers, at least as they applied to software. Haskell Curry wrote
>>>>> from the logic side in 1934 and William Howard published in 1969
>>>>> but I only heard of the Curry-Howard correspondence in 1998.
>>>>>
>>>>> Writing a compiler these days requires the use of this approach.
>>>>> In all, that's a good thing as it makes it clear how to handle types
>>>>> and how to construct software that is marginally more correct.
>>>>>
>>>>> The new Sane compiler is building on these logic foundations,
>>>>> based on the Calculus of Inductive Construction and Dependent
>>>>> Type theory. The compiler itself is strongly typed as is the
>>>>> language it supports.
>>>>>
>>>>> Since dependent types are not decidable there will always be
>>>>> heuristics at runtime to try to disambiguate types, only now we
>>>>> will have to write the code in greek :-)
>>>>>
>>>>> Tim
>>>
>>
>