[ANN] harmatia, "prettified" compiler error message plugin

Recently, I have been playing with the plugin interface for the OCaml compiler. The result harmatia is a mostly for fun plugin which updates the standard ocaml printer to use unicode characters in place of digraphs when possible and some other minor “fixes”. For instance, the following code snippet

let f: <x:int; y:int->int > -> 'a -> unit = 0;;

raises the following error when compiled with ocamlc -plugin harmatia:

Error: This expression has type int but an expression was expected of type
         ⟨x : int; y : int ⟶ int⟩ ⟶ α ⟶ unit
8 Likes

That’s really cool! Thanks! Two questions: (1) are you planning on adding this to the standard OPAM repository and (2) any idea how to use this with a tool like jbuilder?

I like this, esp. the greek, brackets, and arrows, though I’m not sure about ⟦, ⟧ as I’d normally think of them as semantic brackets rather than arrays.

I’ve sometimes wondered how ready programmers would be to use Unicode in source code. I even considered sending a PR for accepting single lowercase Greek characters as a new class of variable names accepted as alternatives to the pre-primed ones. It seems to fit well with the current Capitalization-sensitive lexer, and it maske headers more readable, but then, how many people have bothered setting up a usable input method?

Like this one? :stuck_out_tongue:

More seriously, I do have Greek as one of my input languages.

1 Like

I wrote my own IBUS IM in Python (never published) while working on a programming language (never passed the very-experimental stage). It’s based on reserving a single prefix-key to rule them all. E.g. <prefix> g r a gives α and <prefix> r a gives .

Aha, the APL keybord :slight_smile:

@basus, The code needs some fixing and support for OCaml 4.05 before I publish it to opam. But it is planned, once the plugin I am currently working on is finished. For jbuilder, I am not too sure if it possible to invoke ocamlfind from within the “jbuild” file. If it is not possible, I fear that one would need to manually provide the path to the plugin file to jbuilder. I still need to investigate some potential issues with the integration of compiler plugins with ocamlfind.

@paurkedal, I am also not too sure about ⟦, ⟧, but since compiler plugins currently does not work with the toplevel, I could not field test them. Fotunately, what I really wanted was the ellipsis (and proper angle brackets, because ⟨φ|ψ⟩ is so much nicer than <φ|ψ>).

I think it would be insane but you can have a look at whitequark’s ocaml-m17n.

Under emacs, M-x set-input-method tex is reasonable to input greek and math Unicode symbols; you type completable TeX commands (\alpha, \aleph, \rightarrow, etc.) and they get translated to corresponding Unicode characters.

It’s possible to invoke ocamlfind from actions in jbuilder. See the camlp4 rule in https://github.com/paurkedal/episql/blob/master/tests/jbuild. It uses bash which you may want to avoid. I also found (preprocess (action (system "ocamlfind ppx_tools/rewriter -ppx ppx_lwt ${<}"))) somewhere unpublished, though commented out in favour of (flags (-ppx ppx_lwt)).

1 Like

Just to forestall the potential spread of this w.r.t. Lwt specifically, I want to note that with Lwt master and in the future 3.1.0 (about a month away), you just use the Lwt PPX as normal with Jbuilder:

(preprocess (pps (lwt.ppx)))

Yes, I’m familiar with it. There should also be something similar for Vim based on abbrev. Though, if one really depends on Unicode input, it must work everywhere including the terminal and browser, thus my choice of IBUS (after going though UIM and SCIM).

Added: Presumably one would use a normal keymap for tex-based input in Vim, but I didn’t find anything public. On the other hand there is ibus-table-latex for those using Linux or FreeBSD.

In Vim, you can use :digraphs! For example, type <C-K>l* for λ.

1 Like

I’m a recent convert to unicode in source after writing a bunch of mathematical code in racket and julia. it was a little more tedious to type in (vim’s digraphs help a lot there), but using the same symbols in code that I would use in hand-writing the equations made the code a lot more pleasant to read and maintain.

Julia seems to be the language I was missing when I worked with theoretical physics. I many of us familiar with mathematical are quite ready to adopt Unicode since early on, it may be harder to convince the rest of the PL community. As much as I would love to write (and esp. read) my OCaml programs with a selected subset of Unicode, I suspect it could raise the bar for adopting OCaml in general.

This is the problem with adding unicode to the language: it is so hard to know where to stop. One starts with or for arrows, then is nice for function compositions and for set unions. Going on, ± makes so much sense for bivariant type parameters type ±'a t= A, but then just one step further there is — at last — a nice notation for injective type parameter type ↪'a t = A … After few more steps, mathematicians (and some physicists) will feel right at home whereas other peoples wll wonder how in hell there are supposed to write (or even read) these glyphs.

For a possibly realistic PR I would stop at the Greek type variables, because they are always local. Using Unicode in the core language or the standard library (apart form local (type-)variables) would be bad indeed. The current scheme for operator precedence levels is also not well suited for introduction of a large number of new user-definable operators.

For a language targeted to people from mathematical sciences, I think a moderate well-known subset would be fair, undrer the additional constraints that (a) they should be visually distinct, (b) they should look good with a fixed-width font, © their use should match established practise syntactically and semantically.

Coq is another example where Unicode is quite common.