Re: [stack] fundamental type system problems + possible solutions

Before I start: http://citeseer.ist.psu.edu/dornan98typesecure.html
seems to possibly have something to do with this (maybe?). It's about
using dynamic types in a static system (which is nice for a soft type
system), and also about a static typechecked metaprogramming system.

John Nowak <[email protected]> wrote:
>  That is what I mean. Say you give a macro a quotation. That quotation
>  type checks. Now say the macro tears the quotation apart, and one of
>  the individual parts of the quotation doesn't check (which is very
>  possible). How would you annotate the fragment of the quotation that
>  failed to check?

You're right -- I'm so used to reasoning about my experimental 01
language I'd forgotten that in the real world quotations can be torn
apart. I don't have a good answer to that. I was thinking of providing
tools that would cut quotations on boundaries of known types, but that
won't work if you're cutting the quotations on the results of string
searches (which is what a lambda-substitution macro has to do).

It would make sense to make quotations impossible to cut, but possible
to disassemble -- when you cut a quotation on a symbol, you get back
the quotation before the symbol, the quotation after the symbol, and a
program which when concatenated after those two correctly concatenates
them together. Simplest case:

[yadda x yadda] cut(x) ==
[yadda] [yadda] [concat]

All of the words that cut, concat, or insert quotations would, of
course, recompute and alter the quotations type signature.

I haven't figured out a heuristic to guess where a type error message
should direct the programmer's attention, though. Perhaps that's
something that should go in the annotations that metaprogrammers could
use... "If check fail in here, blame my macro code", versus "if checks
fail in here, trace it back to the user's annotations".

No, I don't see that one working. Oh well.

>  In any case, I have another approach for a type system I want to try
>  that more heavily depends on the algebraic properties of the language.
>  Initial results are encouraging, but I'll need another couple of
>  months to implement it as it's rather complex and I'm guessing my way
>  through it.

Whew! Good luck.

>  - John

-Wm