5 ms·
Macros are an important part of lisps, and it's hard (as in impossible in the general case) to verify that they are type-preserving.
by emillon 14y ago
Macros are an important part of lisps, and it's hard (as in impossible in the general case) to verify that they are type-preserving.
- samth 14y agoFortunately, you can write a sound type system for a Lisp without needing to verify individual macros. That's what Typed Racket does, described in this paper: http://www.ccs.neu.edu/racket/pubs/pldi11-thacff.pdf http://www.ccs.neu.edu/racket/pubs/pldi11-thacff.pdf The basic idea is to first expand the whole program (really the whole module) and then to type check the fully expanded code, which doesn't have macros.