Re: Axiom musings...

[Tim Daly]

I've been reading Stephen Kell's (Univ of Kent
https://www.cs.kent.ac.uk/people/staff/srk21/) on
Seven deadly sins of talking about “types”
https://www.cs.kent.ac.uk/people/staff/srk21//blog/2014/10/07/

He raised an interesting idea toward the end of the essay
that type-checking could be done outside the compiler.

I can see a way to do this in Axiom's Sane compiler.
It would be possible to run a program over the source code
to collect the information and write a stand-alone type
checker. This "unbundles" type checking and compiling.

Taken further I can think of several other kinds of checkers
(aka 'linters') that could be unbundled.

It is certainly something to explore.

Tim


On 12/8/19, Tim Daly <address@hidden> wrote:
> The Axiom Sane compiler is being "shaped by the hammer
> blows of reality", to coin a phrase.
>
> There are many goals. One of the primary goals is creating a
> compiler that can be understood, maintained, and modified.
>
> So the latest changes involved adding multiple index files.
> These are documentation (links to where terms are mentioned
> in the text), code (links to the implementation of things),
> error (links to where errors are defined), signatures (links to
> the signatures of lisp functions), figures (links to figures),
> and separate category, domain, and package indexes.
>
> The tikz package is now used to create "railroad diagrams"
> of syntax (ala, the PASCAL report). The implementation of
> those diagrams follows immediately. Collectively these will
> eventually define at least the syntax of the language. In the
> ideal, changing the diagram would change the code but I'm
> not that clever.
>
> Reality shows up with the curent constraint that the
> compiler should accept the current Spad language as
> closely as possible. Of course, plans are to include new
> constructs (e.g. hypothesis, axiom, specification, etc)
> but these are being postponed until "syntax complete".
>
> All parse information is stored in a parse object, which
> is a CLOS object (and therefore a Common Lisp type)
> Fields within the parse object, e.g. variables are also
> CLOS objects (and therefore a Common Lisp type).
> It's types all the way down.
>
> These types are being used as 'signatures' for the
> lisp functions. The goal is to be able to type-check the
> compiler implementation as well as the Sane language.
>
> The parser is designed to "wrap around" so that the
> user-level output of a parse should be the user-level
> input (albeit in a 'canonical" form). This "mirror effect"
> should make it easy to see that the parser properly
> parsed the user input.
>
> The parser is "first class" so it will be available at
> runtime as a domain allowing Spad code to construct
> Spad code.
>
> One plan, not near implementation, is to "unify" some
> CLOS types with the Axiom types (e.g. String). How
> this will happen is still in the land of design. This would
> "ground" Spad in lisp, making them co-equal.
>
> Making lisp "co-equal" is a feature, especially as Spad is
> really just a domain-specific language in lisp. Lisp
> functions (with CLOS types as signatures) would be
> avaiable for implementing Spad functions. This not
> only improves the efficiency, it would make the
> BLAS/LAPACK (see volume 10.5) code "native" to Axiom.
> .
> On the theory front I plan to attend the Formal Methods
> in Mathematics / Lean Together conference, mostly to
> know how little I know, especially that I need to know.
> http://www.andrew.cmu.edu/user/avigad/meetings/fomm2020/
>
> Tim
>
>
>
> On 11/28/19, Jacques Carette <address@hidden> wrote:
>> The underlying technology to use for building such an algebra library is
>> documented in the paper " Building on the Diamonds between Theories:
>> Theory Presentation Combinators"
>> http://www.cas.mcmaster.ca/~carette/publications/tpcj.pdf [which will
>> also be on the arxiv by Monday, and has been submitted to a journal].
>>
>> There is a rather full-fledged prototype, very well documented at
>> https://alhassy.github.io/next-700-module-systems/prototype/package-former.html
>>
>> (source at https://github.com/alhassy/next-700-module-systems). It is
>> literate source.
>>
>> The old prototype was hard to find - it is now at
>> https://github.com/JacquesCarette/MathScheme.
>>
>> There is also a third prototype in the MMT system, but it does not quite
>> function properly today, it is under repair.
>>
>> The paper "A Language Feature to Unbundle Data at Will"
>> (https://alhassy.github.io/next-700-module-systems/papers/gpce19_a_language_feature_to_unbundle_data_at_will.pdf)
>>
>> is also relevant, as it solves a problem with parametrized theories
>> (parametrized Categories in Axiom terminology) that all current systems
>> suffer from.
>>
>> Jacques
>>
>> On 2019-11-27 11:47 p.m., Tim Daly wrote:
>>> The new Sane compiler is also being tested with the Fricas
>>> algebra code. The compiler knows about the language but
>>> does not depend on the algebra library (so far). It should be
>>> possible, by design, to load different algebra towers.
>>>
>>> In particular, one idea is to support the "tiny theories"
>>> algebra from Carette and Farmer. This would allow much
>>> finer grain separation of algebra and axioms.
>>>
>>> This "flexible algebra" design would allow things like the
>>> Lean theorem prover effort in a more natural style.
>>>
>>> Tim
>>>
>>>
>>> On 11/26/19, Tim Daly <address@hidden> wrote:
>>>> The current design and code base (in bookvol15) supports
>>>> multiple back ends. One will clearly be a common lisp.
>>>>
>>>> Another possible design choice is to target the GNU
>>>> GCC intermediate representation, making Axiom "just
>>>> another front-end language" supported by GCC.
>>>>
>>>> The current intermediate representation does not (yet)
>>>> make any decision about the runtime implementation.
>>>>
>>>> Tim
>>>>
>>>>
>>>> On 11/26/19, Tim Daly <address@hidden> wrote:
>>>>> Jason Gross and Adam Chlipala ("Parsing Parses") developed
>>>>> a dependently typed general parser for context free grammar
>>>>> in Coq.
>>>>>
>>>>> They used the parser to prove its own completeness.
>>>>>
>>>>> Unfortunately Spad is not a context-free grammar.
>>>>> But it is an intersting thought exercise to consider
>>>>> an "Axiom on Coq" implementation.
>>>>>
>>>>> Tim
>>>>>
>>
>