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 <axiom...@gmail.com> wrote: > ---------- Forwarded message ---------- > From: Tim Daly <axiom...@gmail.com> > Date: Tue, 9 Jul 2019 22:56:24 -0400 > Subject: Re: [EXTERNAL] Re: [Axiom-developer] Axiom's Sane redesign musings > To: Martin Baker <ax87...@martinb.com> > > 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 <axiom...@gmail.com> 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 <ax87...@martinb.com> 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 <axiom...@gmail.com> 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 >>> >> > _______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-developer