Inaccuracies in the depiction of Lamdu

[yairchu]

This paper was brought to my attention in one of our LIVE Workshop submission's review comments, and while reading it I noticed that it contains some misleading descriptions of how things worked in Lamdu.

The following paragraph describes Lamdu's solution for type-errors as either selectively disabling editor services or as an ad hoc heuristic:

Researchers have also designed syntactic structure editors for more sophisticated languages with non-trivial static type systems. Contemporary examples include ... and Lamdu, a structure editor for a functional language similar to Haskell [33]. ... Each of these editors presents an innovative user interface, but the non-trivial type and binding structure of the underlying language complicates its design. The problem is that syntactic structure editors do not assign static meaning to every edit state – they guarantee only that every edit state corresponds to a syntactically well-formed tree. These editors must also either selectively disable editor services that require an understanding of the semantics of the program being written, or deploy ad hoc heuristics.

However, Lamdu's solution to the problem was (and still is) the very same principled solution described in the paper:

Hazelnut leaves newly constructed expressions inside a hole if the expression’s type is inconsistent with the expected type.

Note that while in 2013-2017 [1] our terminology matched Hazelnut's - non-empty holes, our current term for these as of 2018 is "Fragments".

The other misleading depiction is in the following text:

Not all structure editors are for educational purposes. For example, ... Lamdu [33], like Hazelnut, is a structure editor for a statically typed functional language. It is designed for use by professional programmers.

... One apparent exception is Unison [8], a structure editor for a typed functional language similar to Haskell. Like Hazelnut, it seems to define some notion of well-typedness for expressions with holes (though there is no technical documentation on virtually any aspect of its design.)

This alludes that Lamdu, in contrast to Unison and Hazelnut, did not maintain well-typedness. In fact Lamdu maintained it and even shared Hazelnut's notion of non-empty holes.

I can understand how such misunderstadings could occur, as you accurately described in your TFP 2016 draft paper -

while Lamdu has many interesting features, there is no theoretical basis presented for their work – it is a rather large body of Haskell code

Indeed, other than implementing it, we haven't described this mechanism in as much detail as you had.

Our website only briefly touched on the topic:

Type errors are confined and localized to the sub-expression involved, made simple and comprehensible.

Type information is not lost when type errors exist, allowing the IDE to guide the programmer in resolving type errors intelligently.

We did also briefly describe it in this video from the 2014 Future Programming Workshop. From the summary at 12:41 in the video:

• Type errors are localized. Instead of inaccurate or difficult feedback from the compiler, type errors in Lamdu are incrementally detected, allowing error localization and better blame assignment. Immediate type feedback help detect errors as soon as possible while they are easiest to correct.
• Lamdu's type inference works continuously, even in intermediate states. Unlike textual editors which necessarily go through states where even parsing correctly is difficult, Lamdu maintains not only a correct structure of the program, but also fully functional type inference.

In the rest of the video the non-empty holes are demonstrated, appearing as code with a red background and type annotations for the expression in the hole and the expected type at the hole's position (when the type of the expression in a non-empty hole matches, and background is green). Note that currently Lamdu displays fragments with a rectangular frame rather than a background color.

We're looking forward to hear your talk and to meet you in person at the LIVE Workshop!

[1] Code references:

• As of https://github.com/lamdu/lamdu/commit/0b20516b50c0af554ae9c207e17d1d942778f327 (2013.06.05) Lamdu's solution to type errors was using non-empty hole like the solution described in this paper.
• At https://github.com/lamdu/lamdu/commit/dbc3deab8b1589b652836503c1577a67d310ddc6 (2012.09.09) Lamdu already partially matched the current solution - for hole results with mismatching types, it replaced them with a hole applied with them (i.e "_ 5" instead of "5").

[cyrus-]

Hi Yair, thanks for the feedback. As I recall, we could not really figure out how Lamdu dealt with type errors when we were playing with it in 2016. We should have been more careful in our characterization, as it does appear that your implementation has non-empty holes. I think the typing machinery is slightly different in that you don't assign holes the hole type, right? Instead, you treat holes like exceptions? Also, how are the non-empty holes inserted? Is there a hole-insertion pass after each edit or does the edit action itself insert holes where necessary to maintain what we call the "Sensibility" invariant?

Unison I think took an even stronger approach in that you couldn't insert ill-typed terms at all, so there were only empty holes in Unison.

We'll make sure to be more clear in future related work sections. Looking forward to meeting you at LIVE!

[yairchu]

I think the typing machinery is slightly different in that you don't assign holes the hole type, right? Instead, you treat holes like exceptions?

Yes, holes act just like Haskell's undefined, or GHC's "holes" :) So their type is forall a. a and they indeed act like exceptions at run-time.

Also, how are the non-empty holes inserted? Is there a hole-insertion pass after each edit or does the edit action itself insert holes where necessary to maintain what we call the "Sensibility" invariant?

Yes, the sensibility invariant is maintained. The edit action for filling a hole itself inserts the term wrapped in a non-empty-hole/fragment if needed (when the term's type won't unify with the hole's inferred type). In some more details: the generation of hole completions (the _holeOptions field of Hole), while offering all the completions everywhere, already generates them wrapped in a non-empty-hole when necessary (when their types don't match), so the completions are already displayed as non-empty-holes even before choosing them.

All other edit actions, like for example adding a field to a record, if implemented naively could had caused type errors, but instead they too wrap the results in fragments in situations where the action would had caused a type error, maintaining sensibility.

Note that non-empty-holes/fragments is a feature of Lamdu's surface language (which is the language that the user interacts with). In the lower-level calculus a fragment containing x is simply _ x (a hole applied with x).

Unison I think took an even stronger approach in that you couldn't insert ill-typed terms at all, so there were only empty holes in Unison.

One could say that if you look at Lamdu's lower-level calculus, then it acts like this description of Unison. The surface/sugared language adds the non-empty-holes/fragments concept on top of it.