source language bidirectional

[ivoysey]

+ Must the source language type system be bidirectional

[ivoysey]

we said

We agree that this question is worthy of more thorough discussion in the
paper!

Replacing the bidirectional type system with one that performs HM-style
type inference would be tricky, because type reconstruction typically
assumes a complete expression. In intermediate edit states, then, one would
not always have enough information to definitively determine the types of
variables nor the expected type of an expression. At best, then, we could
attempt to constrain the action semantics to allow only those actions
consistent with presently known constraints. However, later edits would
then have non-local implications with respect to well-typedness. This could
possibly be addressed by a “whole-program” pass on each edit that put newly
ill-typed sub-terms into holes. However, from a user perspective, this
would require error messages at each such hole. The problem of coming up
with usable error messages when type inference fails is notoriously
difficult.

In contrast, in a bidirectional system the locality of inference precludes
“spooky errors at a distance”. Instead, the interaction is a sort of local
dialog between the programmer and the system involving simple, familiar
concepts -- types with holes -- rather than sets of constraints.

[ivoysey]

this one bugs me, rel to the editorializer and not assuming that there's exactly one type system for a given language.