On 10 Jul 2022, at 14:28, Waldek Hebisch <[email protected]> wrote: > > ... > > However, 'showSummary' really expects a Spad type. In > my example type expression works because arguments > are evaluated by Boot before calling 'showSummary'. > 'showSummary' will work with many unevaluated type > expressions but using it in such way really is abuse > and will fail in corner cases. > > At Spad level one could do: > > show_imp_summary(t : Type) : Void == showSummary(t)$Lisp > > (wrapping it in appropriate package).
Okay, looks like the SPAD route is the most robust route and so should be the route I take. It’s a bit annoying because I was hoping to use Boot/Lisp, but only because I can then do “background” queries from Frimacs without upsetting the prompt number in the REPL. I don’t suppose there’s an easy way to freeze the prompt number for a single SPAD evaluation? > Big (and still not full resolved) trouble with type > expressions is that there may be type errors inside > type expression. So we can not depend on type > expression being well-formed and we can not use > normal type rules to exclude wrong stuff. > Related trouble is that Boot code in several > places passes junk to various routines. Due > to small number of checks junk goes trough > and in simple cases look "working". But there > a lot of work to make our type machinery > really robust. For me the Boot codebase is difficult to understand because it looks like a big, amorphous collection of functions. I get lost, not knowing which way is up, or down. Maybe it would benefit by introducing some kind of module structure, with well-defined interfaces to limit cross-module linkage? Just something as simple as Common Lisp’s package system perhaps? > Anyway, once you have type, it passed all checks > that we have so you can be resonably confident > that type is correct (there are known bugs in > corner cases). With type expression all this > work to check type is before you. You could > probably cop out and use interpreter to evaluate > types, but ATM there are some traps, interpreter > is handling types slightly different than Spad > compiler (and our runtime system). I’ve seen you mention before that you are trying to bring together interpreter and compiler behaviours, which is a very worthy goal, but I imagine is an awful lot of work :-( Paul -- You received this message because you are subscribed to the Google Groups "FriCAS - computer algebra system" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/fricas-devel/60EBEE3E-11E7-4ACC-BEEE-8C7358A49039%40gmail.com.
