Lambda the Ultimate: The AST Typing Problem(lambda-the-ultimate.org)
lambda-the-ultimate.org
Lambda the Ultimate: The AST Typing Problem
http://lambda-the-ultimate.org/node/4170
2 comments
The problem in ASTs is worse because it's not just the functions that have types getting rippled through them, but it's the types themselves; some processing function f maps AST_0 to AST_1, then g maps AST_1 to AST_2, but the vast majority of the nodes in AST_0..AST_2 are the same, only augmented; but you want to verify that the right nodes got eliminated / transformed. I've ended up taking (a) dynamic, explicitly checked approaches to the type safety issue of making sure only the right nodes turn up in the right ASTs, and (b) writing code generators to deal with the type repetition that ends up being needed in languages that don't have the right amount of expressiveness in the type system.
Even when the type system is expressive enough, carrying around all the type arguments can be painful, even if you have higher kinded types. It makes one want a statically typed Lisp with a macro preprocessing step, or something.
Even when the type system is expressive enough, carrying around all the type arguments can be painful, even if you have higher kinded types. It makes one want a statically typed Lisp with a macro preprocessing step, or something.
It makes one want a statically typed Lisp with a macro preprocessing step, or something.
You want s-expressions, like Ocaml and GCC use.
You want s-expressions, like Ocaml and GCC use.
I'm sorry, are you suggesting that GCC is written in sexprs? For OCaml, a more relevant suggestion might be Camlp4. What I'm describing is the need for a language in which to write the compiler for the compiler's source code, so that the compiler's source code can be both high-level enough, and statically typed.
Simple sexprs describing a tree aren't strongly typed enough.
Simple sexprs describing a tree aren't strongly typed enough.
No, GCC is not written in s-expressions, but GNU RTL is.
You can write an RTL processor in Lisp and have macros both for input and processor itself.
If you want to explore macros for infix algolish languages, look into Jonathan Bachrach's D-Expressions for Dylan. Some of the people who first implemented it are here on HN as well.
You can write an RTL processor in Lisp and have macros both for input and processor itself.
If you want to explore macros for infix algolish languages, look into Jonathan Bachrach's D-Expressions for Dylan. Some of the people who first implemented it are here on HN as well.
Lisp isn't good enough; both the structures and the functions are to be statically typed, that's the point. If we didn't care about static typing, this whole debate would be moot, and one could write the compiler in C with tag-discriminated unions if you like (which is in fact the AST format for the Delphi compiler).
Although this is the first time I've heard this problem expressed I always imagined it existed as type inference always seemed to be a little bit 'magic'. I'm a little bit relieved to know that it IS magic (no clean solution exists).