Lambda the Ultimate

If you build your type checker to be incremental in the first place, it isn't going to give up and be fragile. Incremental type checking really isn't that different from incremental parsing using memoization and a worklist algorithm, you just have to handle remote lookup dependencies via a listener list. I don't think you can bolt this on though, type checkers written for traditional batch experiences are just outdated relics of a bygone age.

My point was not that incrementality support would make the type-checker fragile, rather than type-checker for sophisticated languages (OCaml, Scala, GHC...) are complex beasts in general, and a source of fragility, because of the problem domain itself.

Building an incremental type checker is not fundamentally more difficult. Even Scala's type system is fairly easy to make incremental (I did it) sans a couple of issues with impurity that couldn't be memoized very easily (in my case, explicit and implicit case class constructors had a weird first-to-post semantics). It didn't even require many code changes.

Compiling a source code could be separated into several phases. The first phase would compile only top-level symbols, embracing deeper symbols as simple string wholes. The second phase would compile deeper symbol string wholes. And so on recursively. This approach provides a granularity of code that could be partially compiled, with each fragment having its own isolated success/failure result, but implementing a parser that way might cause a few headaches more than implementing a single step parser.

My first reaction is that i don't really want an IDE specific to my language/compiler. I was hoping to make integration with existing IDEs easier.

I usually program in 'vi', and find i want my personal programmer experience to be 'thinking'. Most auto-completion just gets in the way, like providing the closing bracket for a function call, when inserting or editing code the IDE nearly always gets this wrong. The assumption that you type code top-to-bottom, left-to-right seems wrong to me.

One thing that does occur to me, is i would like entering value level code, and it's inferred types to be automated somehow. Program modules should have concrete type signatures to define a stable API, yet these types can be inferred from code. Sometimes we want to auto-generate the module signature from the code, sometimes we want the code to be constrained by the module signature. As such it would be great to see the types for expressions dynamically, and be able to extract them into concrete annotations.

See, you don't really want an IDE at all. At least, you don't get why those features are useful, they have never been useful to you, or you've never seen a good design of them. So you don't really have the context to do this yourself.

I usually program in 'vi', and find i want my personal programmer experience to be 'thinking'.

Got it: you want Hawkeye (the guy who can shoot arrows with amazing accuracy), rather than Ironman (the guy with the augmented power armor). Programmers should just think harder/better and not rely so much on tools to offload that thinking. I totally disagree, but I think much of the PL community thinks like you.

Most auto-completion just gets in the way, like providing the closing bracket for a function call, when inserting or editing code the IDE nearly always gets this wrong.

Auto-completion is just about API discovery. If you are programming in small libraries you understand very well, then it will be more distracting than useful.

The assumption that you type code top-to-bottom, left-to-right seems wrong to me.

Most code is written top-down, then inside-out, then inside-out again. Anyways, a backward or bi-directional type system helps out here as the type information doesn't need to fly in just one direction, but most people get this wrong.

As such it would be great to see the types for expressions dynamically, and be able to extract them into concrete annotations.

A common use case.

See, you don't really want an IDE at all.

I may not want an IDE, at least not any i have seen, for myself, but i understand other people like them, so i want to make integration as easy and useful as possible.

Programmers should just think harder/better and not rely so much on tools to offload

I don't mind offloading some thinking, for example there is little point in memorising the details of an API when documentation is readily available online. But I do think people need to think architecturally first. I think problems are solved by the application of algorithms, and the abstract form of these should be familiar to the programmer. To build a compiler I need to understand trees as a data structure, I can look up the available functions and syntax easily, but I can't easily do so with understanding the properties of a tree (isomorphisms, algebra of rational trees etc).

Auto-completion is just about API discovery

I prefer to use a web-browser open to API documentation for this, which can explain the algorithm used, invariants, etc.

Most code is written top-down, then inside-out, then inside-out again.

I am not sure i agree with this. Often specific functions can be written and tested in isolation. Fixing bugs mutates the data at "random" points. Bottom-up is an equally valid approach.

It might be that i haven't seen an IDE i like, or maybe nobody has written an IDE for me.

You can always try to write an IDE for yourself. Think about the experience you want and go for it. Technical know how isn't going to be your limiting problem.

This is a really interesting idea. I think can already answer some of this for my language, which makes this helpful. My intention was to have a Prolog like meta-language for manipulating the AST. Type inference/checking would also be a function of this language.

In light of this comment, it would make sense if all editor operations were defined in terms of this Prolog like meta-language. Complex editor functions and macros would easily fit into this model. The hardest thing to understand is what simple editing (entering characters) would be in this model.

I suppose we can start by typing the empty program, I'll use '[' and ']' to delimit the edited code:

[] : Void
[a] : X
[a(] : Error
[a(x] : Error
[a(x)] : X -> Y
[a(x)=] : Error
[a(x)=>] : {a : X -> Void}
[a(x)=>1] : {a : X -> Int}

It seems what i would need to do is turn any parse error into an 'error' type. Perhaps this should be a new kind, the kind of 'parsing errors'. Actually that makes a lot of sense now i think about it.

I think a web-based editor and sand-box for the compiler is the right way to go. Unfortunately the ES6 code does not run natively in browsers due to modules etc. I've been using TypeScript and Rollup for another project, and that might be the way to go (or Babel) it should be relatively straightforward as the compiler does not use the DOM or any browser specific functionality.

Generally I am against syntax extensions, it's kind of where Felix diverges from what i am trying to do. I want generics and expressive power, but i also want function application to always look like function application. Although i don't like Lisp as a language s-expressions do this perfectly. In a language of values and functions you don't need any additional syntax beyond '(', ')' and identifiers.

The concept is that polymorphism and type-classes can provide sufficient expressive power, that the syntax for function application and operators can always remain the same. You can create any domain-specific-language you like, but they will all use the same notation for function application and operators.