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.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Agda 1/Alfa

IIRC, the Alfa interface for Agda 1 used the type system to guide structural editing, which is what you suggest here.

Alfa also included support for natural language editing, using Grammatical Framework. This natural language feature could use the type system for disambiguation. For instance, the input "for all numbers x, x is even or x is odd" would be disambiguated to "∀ x: nat. (even x ∨ odd x)", rejecting the ill-typed parse "(∀ x: nat. even x) ∨ odd x".

I've thought about this

I've thought about this topic, but not yet read anything at all (so I'm pleased to learn the standard term for it). However, when I've thought a little deeper about the issue, I've tended to the view that the real productivity gains would come from something that has semantics in the generative structure. So I'm wondering if you have read anything along those lines.

Intermediate states needed

The real value of free-form entry over syntax-directed entry is that when modifying exist code, the easiest path between two syntactically correct states may require going through syntactically incorrect states. Your hyptothetical editor will need to take this into account, allowing automation of as many common transformations as possible.

Definitely modifications are

Definitely modifications are an issue, both for syntax and semantics, though I'm also not quite sure how to handle modifications on a tablet even without the problem of intermediate states.

Related

18 months ago, Thomas Lord argues for use of gestures in programming.

3 months ago, Sean McDirmid asks about programming with touch, noting Conal Elliott's tangible programming and Scratch.

Johnathon Edwards has been working on this problem via Subtext and UI programming languages. He posits that syntax must die and has done some interesting work on what he calls 'schematic tables' for resolving the expression problem in a visual language.

Edwards references work on gradual typing as of possible interest to visual language design. Gradual typing has been discussed several times on LtU [1][2][3].

I at one point was pursuing using types to direct a parse, similar as mentioned by vrijz above. I eventually decided against this because the very notion of bootstrapping an extensible syntax that is type-sensitive was tying my mind in knots, which seemed to violate simplicity goals.

Today, I would favor use of pluggable types and zero-button testing, integrating with the IDE and visual cues to let developers know about type-errors and broken tests just as easily as syntax highlighting helps developers discover syntax-errors today.

So I focus on language features that would help achieve continuous testing and analysis while we edit and (if we wish it) even during runtime: Object capability language makes it easy to confine unit tests and even many integration tests. Reactive languages allows tests to exist as 'continuous' programs during the whole edit cycle and even during runtime, though I feel we really need to capture most conditional branching and conditional binding within the reactive expressions (unlike Bling).

I was specifically inquiring

I was specifically inquiring about a type system for type choosing rather than type checking code (choosy type system..hey)? My earlier posts were more general interest, I'm now beyond the prototype process and I'm trying to figure out how to write a paper on this (maybe submit Onward if they ever get their CFP out). Conal's TV work is definitely relevant as it leverages Haskell's type system, I should have made that connection faster. Subtext is not so related since I don't think it deals with typing (related in the visual sense, not in the type sense). Scratch, AppInventor, etc...seem to have pretty weak type systems.

Type-sensitive parsing seems a bad path to go down, but then I don't have to parse.

When I was at EPFL, I wrote up a Scala Live proposal to push the limits of what an IDE could do. This was when we still had the bleeding edge (and very risky) IDE with fully incremental parsing type checking. The next risky step was to start memo-izing the execution so that we could continuously repair program executions while the user was editing. Now I'm settling for live programming in a structured declarative language, that makes the problem somewhat easier of course!

In the same vein as TV, you

In the same vein as TV, you could add naked objects and object browsers.

I look forward to seeing your paper.

Challenge

It seems to me the great challenge with this goal would be that it is quite difficult to limit expressions based upon types. For example, take the simple conditional expression: if _ then _ else _ :: Bool -> a -> a -> a.

This expression could be 'meaningful' in any context, since its output type is a function of its body. To ensure safety-by-construction will require ensuring that both the 'then' branch and 'else' branch produce a type compatible with both the context and one another (which raises a related challenge: how do you ensure the types on both branches are compatible continuously during edit, without overly hindering productivity?)

In the more expressive programming languages, this sort of 'option' seems to be very common - almost every aspect of glue-code has some sort of generic type. How many 'options' can be presented to the user before searching and selecting among them becomes less productive than writing out a little code and correcting for the occasional safety error?

If you are working

If you are working backwards, which makes sense when doing construction, then you select if/else first from its receiving context, you know the desired return type, so you automatically get the type required for the else and then branch! This means that the type system should infer based on the desired return type rather than the provided parameter types. But you also have to work top-down when writing your expression, sort of like writing S-expressions!

You could also treat construction as iteratively narrowing constraints, but I'm not at that point yet, nor am I sure I'll need to be. Trying to keep it simple :)