Yeah, incremental parsing is quite anti-functional--but tree editors don't need to parse.
Type checking I am less convinced. With syntax-directed methods one should be able to hash-n-cache each sub expression and get incremental for free. In the case of syntax directed + passing hints down the tree, just keep track of the hints too. [...let's not talk about Damas-Milner. :)]
Then, which I think Unison goes for, there is the approach where one never has untyped syntax to begin with. Not sure how annoying this is with normal programming, but should be great for theorem proving, which probably where tree editors will shine the most anyways.
We agree incremental use of global type inference algorithms is non-function.
But I am also saying you don't need to do that. Certainly don't need type-inference in the case where the ASTs are typed by construction. And the syntax directed algorithms can also infer somewhat.
You can also alternatively cache the result of global inference, which sucks for refactoring but preserves purity.
You will need type inference if you want any sort of non local communication...e.g. variables that hold different values or functions. But ya, if your language is just pure trees with no names or symbol tabkes, you don't need it; not very useful, however.
Type checking I am less convinced. With syntax-directed methods one should be able to hash-n-cache each sub expression and get incremental for free. In the case of syntax directed + passing hints down the tree, just keep track of the hints too. [...let's not talk about Damas-Milner. :)]
Then, which I think Unison goes for, there is the approach where one never has untyped syntax to begin with. Not sure how annoying this is with normal programming, but should be great for theorem proving, which probably where tree editors will shine the most anyways.