So I think "easy to mentally model" gets harder and harder to achieve as the type system becomes more powerful. If your conclusion is that we keep the type system limited in power, that's valid! but not what I'm exploring.
Another point that I failed to make in the post (thanks for the pushback!) is that type inference algorithms leave you high & dry in the presence of a type error. Then you're left with lots of hidden state (the internal steps the algorithm took before arriving at the error) and the final conclusion, which, if you're lucky, points you to two places in the code where the inferred types are in disagreement.
With my proposed system, all types are annotated all the time (to be shown or hidden via editor flag, or on hover), and the annotations are updated in response to actions taken within the editor. The "algorithm" becomes extremely simple, with almost no intermediate steps.
Of course, proof will be in the pudding, if I can actually achieve a pleasant editing experience :)
> all types are annotated all the time (to be shown or hidden via editor flag, or on hover), and the annotations are updated in response to actions taken within the editor
So there are two possible reasons I can see for automatically "annotating" all the types:
- Caching that info to easily show in the editor (which is a good feature, but many editors already do this without having to modify the source; it happens entirely editor-side)
- Using the "current" inferred type as a jumping-off point for determining the "next" inferred type
The second was my original interpretation, and what sounded so distressing as a user
Consider this situation:
1. Your program and the inferred types are in one state
2. You modify some code which changes an inferred type
3. You change the (visible) code back to what it was previously, but now the inferred type is different because it was partially based on the previous inferred type
This is what sounds like a nightmare, assuming I understand correctly that it's possible on the described system. The inferred types are now a state machine, where it matters not just what code is on screen, but how it got there.
Hm so it is a state machine, but (my hope is that) all state transitions are simple and direct (and observable!) outcomes of user action. If the transitions get at all complex or unobservable, I'll probably call it a failed experiment.
It might also end up being the case that users keep types "visible" at all times, only turning them off in certain situations. I can also imagine a flag to "only hide inferred types that are primitives" or something similar.
Fair enough, and it's certainly an interesting experiment, don't want to discourage experimentation
But I will say I think the desire to show the inferred types is orthogonal to the desire to persist them on disk, in the source-of-truth code files. If the state machine really is what you want to experiment with then have fun, but if your desire is just to give the user more visibility into inference, I think there are simpler ways to go about that
> Another point that I failed to make in the post (thanks for the pushback!) is that type inference algorithms leave you high & dry in the presence of a type error. Then you're left with lots of hidden state (the internal steps the algorithm took before arriving at the error) and the final conclusion, which, if you're lucky, points you to two places in the code where the inferred types are in disagreement.
How much state gets hidden is 100% on the quality of the implementation, isn’t it? There’s nothing that forbids an implementation from dumping that hidden state in whatever form it wants to (as an example, compare C++ diagnostics of different compilers or different versions of a compiler)
> The "algorithm" becomes extremely simple, with almost no intermediate steps.
I don’t see how it can become simple merely be the way things are presented. If you write f(foo,qbar,baz,quux) in a language where overload resolution is complex and the compiler has 20 overloads to pick from, but can’t find a ‘best’ one, it still has to show you what overloads it considered, how it ranked them and why, and which ones were left.
So, if you want type errors to be extremely simple, I think you need a simple language (type-wise)
Although I personally think type inference is the killer feature that makes static typing accessible (almost always auto), I've seen hostility to it, in particular among C++ and C# programmers. The point of this project, as you say, is to be as explicit as possible in the code, while at the same time presenting a view of the code that is less cluttered.
My initial impression is that if I were to use a system like this, I would want any type annotation that differs from the default inference to be visible. The only choice left, then, is when to display redundant annotations, which is where a lot of the disagreement around type inference is, even without this scheme.
Yeah, it is definitely nice to have inferred types surfaced to you, but in these systems they are still re-computed on every textual edit, as opposed to being "sticky" (persisted in the source tree).
Source control does look very different in a projectional language, as git diffs no longer make much sense (viewing a pull-request with the source tree's JSON blob is essentially useless).
Unison is the language that's gone farthest with this, as far as I know; their solution to diffs & merges is to handle everything from within their CLI, bypassing git entirely. I imagine I'll do something similar.
I don't know anything about how you're storing the source, but if the data elided from view could be stored in files next to the source that were more readable than JSON, you could potentially take advantage of the whole git ecosystem still. People could put code up for review and the reviewers could even confirm if the additional (normally out of sight) information made sense to them.
FWIW, I'm totally on board with the idea of focusing on the interactive experience, but history has shown it to be very difficult for language environments not based on files to cross the chasm into more common use. (If you don't care about lots of users, then ignore this entire comment! Plus, it's always _possible_ that something will cross over, but we've got decades of people trying...)
Anyhow, I'm really excited to see where you go with this!
Oh hi kevin! So if there's a possibility that the "extra data" would get out of sync with the "source code" (e.g. via a git merge, or someone just editing the source code as plain text), then it unfortunately breaks the guarantees that this system needs :(
I guess I could store a sha of each and fail loudly if I detect that one was edited "outside of the IDE" but again I think that would break the assumptions that git makes about diffs &c.
I've tried to go down the "text but nicer" route before, and it always comes up short; so now I'm trying "text is not a supported representation" we'll see how far I get.
Yeah, good point that text is a potentially fragile approach when combined with git. I think the Squeak Smalltalk folks figured out a way to retrofit git support, so maybe it's possible to go all-in on the representation you want and work out git support later if it seems useful enough.
If I may, I’d suggest instead of shunning git, which is widely preferred as people’s revision control, perhaps consider writing a diff plugin for git to render out the diffs nicely, and include that tool with the compiler/interpreter install.
This hits on the biggest problem with projectional languages, and why text has dominated: they don't interoperate well with any existing developer tooling.
So the language implementors have to write everything the developer needs: code editor, source control, code review, code browser, etc
You're completely isolated from the wider ecosystem of development, and the benefits so far don't seem worth it. As described here, you save on the reference resolution phase of linking, which is nice, it should be faster and eliminate some classes of error.
The nice part about text as a common format is that it's common. If every language has to implement every tool then it's an N * M problem. When tools can be reused across languages they become N + M.
A user of a projectional language is giving up git, Github, their favorite code editor, and depending on language-specific tooling to replace all of that. And even when the lang-specific tooling is sufficient, it needs to be relearned and recustomized (think all the configuration just in a code editor: prefs, theme, extensions like VIM keybinds and Copilot, etc).
> bypassing git entirely. I imagine I'll do something similar.
So I'm assuming your language will have some sort of custom source code management system? If so, what do you do when a user wants to store a non-code file together with the source code, e.g. how web applications might have CSS files, fonts and image assets in the repo?
So the "repo" in this case is a database, where currently the only things stored are denormalized source tree nodes. I could imagine extending the database to support arbitrary assets, probably also addressed by the hash of their contents (same as top-level language definitions are).
Great, thanks! This all came at a perfect time -- I was just about to start working on converting a bunch of our music education games to iOS. My plan was to do that, then convert our existing games from Flash to HTML5. If I can get this up and running, it would save a great deal of time.
In the game, the only place I check the platform is to see how big I should make the screen (like 3 lines). Everything else is shared!
The big news here is that you can use a single codebase (and a nice advanced language like ocaml), and deploy to 4 platforms.
The framework I'm using is called "reprocessing", which is a ~port of the "processing" language to OCaml, targetting OpenGL. It abstracts out the different platforms.
We are actively working on it. Linux's well on its way and is much easier than windows. We're open to PRs ;)
We consolidated web and native desktop in one repo https://github.com/bsansouci/reasongl. iOS and android are still out because we're still figuring how everything should fit together to be useful.
much more readable transpiled output, really nice (and getting nicer) FFI to javascript.
but it doesn't interface with existing ocaml stuff as well (doesn't use `.cmo/.cma` so it needs to compile everything from source afaict)