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 <axiom...@gmail.com> 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 <care...@mcmaster.ca> 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 <axiom...@gmail.com> 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 <axiom...@gmail.com> 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 >>>>> >> >