archives

Type systems for structured languages

While I've read a lot about syntax-directed editors, I haven't found much material on the type systems that go with them.

Background: with a syntax-directed editor, the editor guides the user into creating syntactically-correct programs: in this case a parser is not used to construct a tree, rather the grammar of the language is used by the UI to create a UI that allows the user to build the tree directly. Now most existing languages are designed for free form editing, and so syntax-directed editing is considered annoying. However, we could design a language that is optimized specifically for syntax-directed editing, and perhaps obtain different results. This perhaps has advantages on platforms where keyboard input is inconvenient, like an iPad.

I think the syntax problem is easily solved and experiences with syntax-directed editing is well covered in the literature. However, it seems that the type system for such languages is interesting also: the editor can ensure that your program is always type correct by only providing options in the editor that are meaningful type-wise. As with syntax, we could optimize such a type system for construction rather than verification.

Is anyone aware of any projects or papers on the subject? My literature review didn't turn up much, but I could have been looking in the wrong places. I'm not even sure what this would be called if someone explored it already.