BYU - Spring 2013 - CS 630 - 5/30 - Paper

[Andrew Kent]

What is this paper about?

This paper is about introducing a system for typing Scheme and its macros, but not to the granularity of other type systems. In other words, it does more general typing that seems to preserve structure and prevent blatant errors, while leaving some of the minutia of checking each and every type against each other to the runtime environment. This is in response to the general difficulties people have expressed with macros, namely that they are extremely difficult to debug when compared with other constructs.

What does it contribute?

This paper attempts to solve some of the historical issues people have had with macros by introducing a subtle type system that does technically limit the power of the macro system to some level, but that intends to retain enough power for Scheme programmers dealing with ordinary problems.

They highlight this problem by showing some simple macro misuse cases and then analyzing what kinds of errors are reported to the programmer. Some are more useful than others, for example the “incr” example had decent error reporting, but the other was quite unhelpful, and so they set out to define the problem and a solution using types.

They first state generally that the language can be thought of as a core language and a surface language. The surface language is what the programmer has available, and then after macro transcription all that is left is the core language to be compile/run/etc. They explain that there is one complication in this converting of surface code to core code, namely having stuck terms (terms that can not be expanded/transcribed any further but are not entirely in the core language either). This is a problem they address at the end of their work.

They then proceed to describe that their system uses only two types (expr and def) and that the other descriptive item they use is the “shape” of an s-exp. The types are very simple and prevent only simple, obvious problems, and the shape system is used to correctly match s-expressions that have a desired form. For example looking at “(moo (quo rem) (div x y) (= rem 0))” we are somewhat hard pressed to identify exactly what is going on, but knowing that “moo” is a macro and that it’s shape is “((id id) expr expr) -> expr” allows us to make sense of it and move on with our analysis (otherwise, for example, it could look like quo was a function call with rem as a parameter).

One of the main restrictions that allows them to achieve type soundness is the exclusion of overlapping macro patterns. This is a very natural decision, allowing them to avoid having an arbitrary lookup order or more complicated best match tactics that could fail or further limit the system to remain sound.

The soundness of this system is proven in two parts. First, they show that (excluding stuck terms) progress is maintained, or that a typed term is either a core language term or expandable. Second, they show that a program having a certain type implies that that program expanded will have the same type. Thus the type system is sound, for any prediciton it makes for a program will be valid. The excluded cases, stuck terms, fall into two categories. First, pattern variables and keywords are simply typed as any (which, being what any type can generalize to, will cause to limitations). Second, the other problems or ways to get stuck are simply not typed by the system, so by making the typing a partial function they avoid dealing with these as far as soundness goes (and it would likely make sense for many of these to have the type checker simply complain a given expression is untypable),

They discuss some work in this area in other languages, but note that none are as expressive or powerful as Scheme. They also note some of their limitations, that this does not work yet on full Scheme and that they have not yet handled macro generating macros, and that it does not handle programmed macro systems (syntax-case).

What did I understand?

I felt like I understood most of the paper and a good chunk of the figures. I’m hoping to print this out tomorrow morning and review the other figures with the descriptions of them next to them.

What lingering questions do I still have?

Why don’t syntax-case macros fit into this system?

Is this in use at all today? Or was it just to prove a point that macros are tamable and understandable to squelch (or attempt to squelch) vocal opponents of Scheme’s powerful macros? I ask because the examples in the beginning, when I put them in DrRacket, seemed to get the same error messages described in the text.

[Noonan]

Taming Macros

Summary: The Author starts out by introducing macros and explain how they can be abused (it’s wierd though, he makes it sound like it’s the programmer’s fault that problems arise, not that the programmer wasn’t intending to cause problems.) The next section he goes on to justify the usage of macros. In the next section he goes over examples of macro abuse and also problems with error reporting in macros. The author then moves on to define a toy language for their purposes. The author then moves on to talk about shape types and problems with determining the exact shape of (a b) when it is used in a sample macro. The author then discusses how their type system determines shape before parsing by looking at the shape of the macro itself. The author then goes over some rules for determining shape based on terms in the environment. The author then moves on to do a proof of the soundness of their work and then to talk about which stuck terms can and can’t be handled. The author then moves on to discuss the difficulties with extending his toy language in order to handle more of the language, but then goes on to say that they reformulated it in order to handle R5RS syntax in an appendix. The author then briefly discusses related work in the field of macros and then concludes discussing future work involving extending the system.

Major Contributions: I actually don’t get it. I mean, the author sits down with a subset of scheme and says “hey I can type things” and I’m like “so what?” What is so novel about deriving types o a subset of what is actually allowed in the language. The author claims that his typing system helps in debugging. But my better judgment says, if your system only works on a subset, then it’s not likely very useful.

Something I Understood: I understood the idea of using recursion in order to determine types.

Things I had trouble understanding: The proof and pretty much every figure after the initial grammar describing the language.

[Yu Huang]

Title: Taming Macros

Summary: This paper presents a type system for taming Scheme-like macros. Section 1 mentions the misuse in programming construct, which may cause the generation of an incorrect program or the triggering of errors during compilation. Because of this, this paper tries to design a type system that provides powerful syntactic abstractions even though it reduces the power of the macro system. Section 2 uses an example of checking exceptions to show that macros are necessary for programmers to introduce syntactic abstractions. After that, Section 3 discusses two problems that macro system have. The first one is an error in the macro use, and the other is an error in the macro definition. There are several examples supporting the above points. Further, the paper claims that most Scheme systems do not provide strategies to debug macros thus makes the problems difficult to solve. Section 4 presents the syntax and semantics of a Scheme-like language. The type system present in this paper will be also applied to this language in the rest of paper. 4.3 presents three classes of stuck terms for which macro expansion goes awry. Section 5 gives the idea of shape type that provides a way of describing the terms that macros and primitive syntax constructors consume and produce. It is able to guide recursive type checking before macro expansion. Section 6 gives the type system based on shape type in section 5. There are several rules for type checking the language above. To prove the type is sound, section 7 proves two theorems, preservation and progress. Preservation says that the expanded program has the same type with the program before expansion. Progress says that a typed term is either a term in the core language or expandable. 7.2 discusses the types of stuck terms. For three classes of stuck terms, only the first class consisting of pattern variables and keywords is typed. 

Main contribution: design a type system that can be applied to Scheme-like language and can be further extended to Scheme.

Things I understand: The basic concepts and power of macro and the problems from the usage of macros, the idea of shape type and the type system that is applied to Scheme-like language. 

Things I have trouble understanding: The syntax of shape type and type system.

[Jay McCarthy]

This is the first type system ever for macros

>
> Something I Understood: I understood the idea of using recursion in order to
> determine types.
>
>
> Things I had trouble understanding: The proof and pretty much every figure
> after the initial grammar describing the language.

Hopefully class helped?

--
Jay McCarthy <j...@cs.byu.edu>
Assistant Professor / Brigham Young University
http://faculty.cs.byu.edu/~jay

"The glory of God is Intelligence" - D&C 93