▲ | JonChesterfield 2 days ago | |||||||
What's the objection to putting type annotations on the macro, and refusing to compile code where the arguments to the macro don't match the type? | ||||||||
▲ | kscarlet 2 days ago | parent | next [-] | |||||||
There's no objection, but I think this solves a different problem than above described, and is possibly a more complicate matter in itself than it may look like. First, are you describing a way to typecheck macro so that it doesn't generate ill-typed code? The type system that does this is active research (I think requires modal typing?). Also this does not increase the expressive power of untyped Lisp macro -- just making them safer, while I was proposing their expressive power is unsatisfactory and should be enhanced via a sort of reflection. That would only makes them even harder to type! | ||||||||
▲ | reikonomusha 2 days ago | parent | prev [-] | |||||||
Since a macro is a definition of syntax, I think you'd essentially need something like typing judgments to show how the typed elements of the syntax relate to one another, so that the type checker (e.g., a typical Hindley-Milner unifier) can use those rules. These are usually written as the fraction-looking things that show up in PLT papers. This is, as GP says, essentially extending the type system, which is a task fraught with peril (people write entire papers about type system extensions and their soundness, confluence, etc.). | ||||||||
|