[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

From: Martin Baker
Subject: Re: [Axiom-developer] [EXTERNAL] Re: Axiom's Sane redesign musings
Date: Sun, 30 Jun 2019 08:11:57 +0100
User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:60.0) Gecko/20100101 Thunderbird/60.7.2


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 ?


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.


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 :-)


reply via email to

[Prev in Thread] Current Thread [Next in Thread]