One of the struggles of working with first-class dependent types is that they can be created "on the fly". Ideally, when used, the type information can be "factored out" to yield a specialized version that is more efficient. The idea is best described in a book, called Partial Evaluation, which used the type information to collapse and specialize a function.
Jones, Gomard, and Sestoft "Partial Evaluation and Automatic Program Generation" (1993) Prentice Hall On 12/31/20, Tim Daly <axiom...@gmail.com> wrote: > It's been a long, slow effort to "get up to speed" (or more > accurately "a slow crawl") on the various subjects one needs > to know to work on "computational mathematics" aka SANE. > > A reading knowledge of a lot of areas is needed, including > things like > > abstract algebra (to understand Axiom's category/domain) > type theory (to understand first-order dependent types) > proof theory (to understand Gentzen, sequents, etc.) > category theory (to understand catamorphs, functors, etc.) > metaobject protocol (to understand CLOS extensions) > number theory (to understand finite fields) > calculus (to understand field extensions for integration) > programming (to understand typeclasses, CLOS, etc) > philosophy (to understand polymorphic sets, etc) > CPU hardware (to understand "down to the metal", FPGA, etc.) > Specification (to understand consistancy, completness, etc) > Verification (to understand decision procedures, etc) > Proof tools (like Coq, Lean, etc.) > > and a few other subjects that won't come to mind at the > moment. > > The usual academic approach, that creates a special > "course of study", requiring classes in areas is probably > best. There are a lot of good online courses, such as > the UOregon summer school, that introduce the basic > ideas clearly. There are some good introductory books > like Troelstra and Schwichtenberg's "Basic Proof Theory" > that cover Gentsen, Hilbert, and Natural Deduction ideas. > > It seems worthwhile to put together a full course of study > with links to videos and books, so one can get up to speed > on required knowledge. I'll start an outline with links to > these on the axiom-developer.org website in the coming > weeks. It's sort-of an "Axiom University" major in > computational mathematics. > > (There are no degrees :-) But one does mathematics and > programming for the joy of it anyway so who cares?) > > I welcome suggestions and online links. > > Tim >