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

John Nowak <[email protected]> wrote:
>  William Tanksley, Jr wrote:
>  > Perhaps some more thought could be put into integrating the macro
>  > system and the type system. It seems to me that there are a few ways
>  > it could be done.

>  > Every parameter of the macro has a type; if inferring the type is too
>  > hard (and it probably is) you can require type signatures as part of
>  > the macro definition.

>  The problem is not typing the arguments to the macro; it's dealing
>  with the situation where the expansion of the macro is not inferable
>  and there's no way to provide annotations to quotations within the
>  expansion because the expansion is obviously not in the source code.

I can read this okay up until the phrase "obviously not in the source
code." Then I get completely lost. I'm going to reduce the argument to
a logical form as I understand it...

"It's impossible to X when condition Y holds."
   X = "provide annotations to quotations within the expansion"
   Y = "the expansion is obviously not in the source code"

I don't see how this could be _possibly_ true. Why should it ever be
impossible to annotate a quotation generated by a macro? Why is
"obviousness" part of the criteria for impossibility? How can code
generated by a macro not be part of the source code (unless you mean
not part of the original source code pre-generation, but again, I
don't see how it makes a difference whether the code was typed out by
hand or generated by a macro).

>  There are also issues with macros becoming much more tedious due to
>  the need to shuffle data in and out of some AST sum type in the macro
>  procedure itself.

I think I see your point here... I don't know what AST means (abstract
syntax tree can't be right, can it?), but I can imagine a macro being
able to dynamically generate code AND also dynamically generate the
code's type signature. Yes, that would be both powerful and very
annoying.

>  > Obviously, a typechecked macro system would exclude some obvious
>  > macros... But can we get things done with a subset of all possible
>  > macros? I think so...

>  Maybe. It's not just that though; if the facility becomes too much of
>  a pain to use for useful things, it might as well not be there at all.

That's what I mean -- break "macros" down into different classes and
subclasses, and only implement the classes that can currently be
reasonably accomplished, possibly using distinct syntax (or better,
distinct defining words) for each type.

The big problem with doing things this way is that someday you'll find
a sensible way to accomplish something new, and you'll have to add on
a new subclass of macros to express that. Your language will want to
change, but legacy will hold it back.

>  Concatenative languages have a huge benefit in terms of macros because
>  there are no hygiene issues to worry about. Ignoring types, macros are
>  beyond trivial. Ideally, it would be nice to keep this property.

Agreed. This is a hard problem with types in general.

>  A soft type system makes this easy.

Check out "hybrid typing",
http://www.cs.ucsc.edu/~cormac/papers/popl06-hybrid.pdf; I don't know
if it's any good, but it claims to be :-).

> Not being able to prove that the
>  macro evaluation itself will not have a type error is of little
>  concern to me provided that the expansion can be checked in the vast
>  majority of cases. A dynamic failure during a compile time expansion
>  isn't a big deal.

But a dynamic failure "during a compile time expansion" is actually a
static failure during the definition of the word using the macro, and
you've got all the same problems you wanted to solve as far as
printing out a readable error message that the person trying to use
the macro will be able to figure out.

>  Right now, I'm leaning towards a soft intersection type system that
>  will be robust with respect to transformations and infer most any
>  reasonable program. Even if the type system never gets in your way,
>  there are benefits to soft types. For example, being able to run a
>  program to discover what's wrong with it when the type errors are
>  undecipherable is a very nice feature, especially for programmers new
>  to the language. I'll probably write up something about my approach
>  soon once I've filled in the details.

I'm interested and curious. I think I get your point... Perhaps such a
type system could interact with the contract and test case
specifications to see what possibilities are ruled out or explicitly
required (respectively); and a type error could imply that you need to
correct one of your specifications or add a new specification, and
(even better) the error could hint what that specification would look
like.

>  - John

-Wm