COMP 617 Proposal, Fall 2008

Ronald Garcia


Topic:  Type-directed Syntactic Abstractions


Research Problem:  

Macros are one of the most touted features of languages like Lisp and
Scheme.  They allow programmers to construct expressive high-level
abstractions and to support the construction of domain-specific embedded
languages.  Some efforts have been made toward adding macro-like
features to statically typed programming languages, focusing on
different aspects of the problem and with varying degrees of success.

In recent years, some typed programming language designs have included
a static semantic component that involves transforming one statically
typed language to another by type-directed transformation.  This model
is suggests a novel approach to adding support for "meta-type-safe"
(in the terminology of Zook, et. al)  syntactic abstractions to a
programming language.  

The heart of the idea is that the transformation rules of a
syntactic abstraction  (cf. "syntax-rules" from R5RS Scheme)
should be accompanied by two type-theoretic components:  

1) A typing rule for the syntactic form being defined.  
2) A proof that the transformation rules preserves well-typing.


A single syntactic abstraction might be transformed based on one of
several transformation cases, distinguished by syntax (as in Scheme
syntax-rules macros) or by the type structure of subterms.  In order
for the latter case to be sound, cases must be shown to not overlap.
In type systems and "translation systems" alike, an inversion lemma
often serves to guide the implementation of a type checker or
translator.  A type-directed macro system could also be founded on
adding inductive cases for each syntactic abstraction to a proof of
inversion.



Semester Readings:

1. Macros as multi-stage computations: Type safe generative binding
macros in MacroML.

2. Staged Notational Definitions

The approach behind MacroML seems a good starting point for developing
a semantical metalanguage that can support type-directed syntactic
abstractions.  


3. Nominal rewriting.  Maribel Fernandez and Murdoch J. Gabbay
(doi: http://dx.doi.org/10.1016/j.ic.2006.12.002)

Type system formalisms in the literature invariably assume variable
conventions in order to simplify their presentations.  If such macros
are to respect hygiene, the underlying framework must be equipped to
handle binders both native to the language and introduced by macros.
Given that macros essentially perform rewriting steps, and nominal
rewriting is meant to address term rewriting with binders, this paper
seems relevant (though more background reading may be necessary before
it is accessible).