Hello,
I want to inquire about the feasibility of adding typed holes a la https://hazel.org/ to OCaml.
There main argument is that a programmer spends much time with incomplete programs, at which many tools break down (tests won’t run, type checkers mostly fail, and even code formatters will fail on syntax errors); however, a rigorous semantic can be given even for incomplete programs, and structural editing can be used to avoid syntax errors altogether. I find this argument compelling, and would love to have these features available in OCaml itself, or at least a subset of OCaml.
For the OCaml compiler experts out there, what would it take to have an alternate backend that interprets an IR corresponding to a subset of OCaml (excluding, i.e FFI) that is tagged with type information and can handle typed holes?
More generally than typed holes, I’m arriving at the conclusion that while throwing away type information during compilation certainly makes for more efficient programs, during the debugging process, that information is extremely useful to have for introspecting the state of your program. It feels sad to spend such meticulous care crafting good types and then throw all that information away when you press “Play”. Dynamically typed languages at least tag the values at runtime, allowing easy introspection. However, I think in principle a statically typed language should have an advantage over dynamically typed languages, since we have strictly more information about the program.
Typed holes seem like the realization of this. Rather than giving up and throwing a runtime error of some kind when a program is incomplete or incorrect, we can leverage the information we have to present a clear semantic of possible values for an incomplete program.
Mmmm … for teaching, I can see the value of “typed holes”. But for professional programmers, building real systems, the overhead is … pure waste. One of the singular value propositions of the ML family of languages, is type erasure: that is to say, all the types are for the compiler: at runtime, it runs like C with a garbage collector.
Discarding that would be extremely bad for real code and real systems, where performance matters.
That’s a bit off, yes you throw it away, but it can be used to many things during codegen, and if the goal is introspecting it, you can instrument the code with types in many ways.
But I wonder, isn’t assert false enough for you? That’s what I do when I want a piece of code to ignore the specific error for now
When iterating on code or debugging a problem, performance almost never matters. Of course there are exceptions. But usually it’s the semantics you’re trying to get right, and processors are so fast that you can slow things down by several orders of magnitude without really noticing.
True, assert false is an instance of the thing I’m looking for. It gives a clear semantic to incomplete programs. However, that semantic is the most trivial one possible: throw an exception. The Hazelnut calculus gives a more nuanced treatment, allowing you to get incomplete results from incomplete programs, and gradually fill in the implementations, updating that result. It’s like EarlyBird’s time travel debugging + types holes + semantics for updating programs.
Again, I an see how this could be useful for small problems, and esp. for teaching. But when I’m iterating on a problem, often I sit on a massive tower of OCaml packages, and having all those be compiled in a manner that slows them down by 10x would be … intolerable.
Just off the cuff though, it seems like all a “typed hole of type 'a” is, is None : 'a option. And then we “lift” all the code that deals with it, or could deal with it, with options and Option.map and such, everywhere. Not sure why this would require keeping type-information around at runtime …
It is like what John Backus’ FL does for runtime exception. Like ML’s exception, It probably needs at least the runtime capable of expressing extensible variants type to working.
Although what Hazel does is somewhat different, all primitive FL functions are strict with exceptions, while in order to produce a “partial result” need some special treatment to functions that are not sensitive to arguments.
I don’t quite see how would this work in a non-pure setting. Apparently when performing I/O with “holes” there’re not many useful things can be done. Unless we can encapsulate side effects with, say, algebraic effects.
It’s more like visualizing a “lazy” language, where assuming the appropriate strict analysis has already been performed so the eval order is as close to strict evaluation as possible.
That really doesn’t really match my experience when using merlin. In nearly all situation, ill-typed programs or libraries feels like transient states where most tools work very well.
Spending effort improving this transient state doesn’t seem that worthwhile to me. Similarly, debugging code that is ill-typed feels ill-guided: when even the type system knows that your program is wrong, it seems better to correct those obvious mistakes rather than trying to run an interpreter with partial holes to try to debug less trivial error first.
Well spotted! While playing with it, I noticed Merlin still reports spurious warnings, e.g. (??) x triggers warning 20 (“this argument will not be used by the function”). I guess holes are translated internally to assert false.