I recently started using Jupyter with Python for some numerics work, and it got me to thinking about the difference between OCaml and Python, and suitability for integrating into such “rich toplevels”. I certainly haven’t thought about it deeply, and it’s been so long since I was a type theory cognoscenti that I can’t claim anything other than passing familiarity. But here goes anyway …
It seems like, one of the things you could get with modular implicits, is a systematic type-directed way of converting a value of some type (say, the type of a expression in a toplevel that’s about to be compiled) into a value of a standardized type that the “rich toplevel” understands. And so, that might allow for display of all sorts of values in that toplevel in a rich manner, and not just particular types like images and such.
And as I read about IPython widgets, it seems like maybe one could go further and resurrect the “active objects” of CLOS: an object in OCaml with a UI representation that communicates with the object, and a systematic way of doing that for objects in the toplevel.
All of this is already possible, at the cost of modifying the toplevel so after typechecking, it hands the type to some code that generates the extra code I describe above (and that would have been automatically generated by modular implicits) (OK, not quite, not quite, but still … could go a long way).
Anyway, just random musings. I wonder if anybody’s done anything in this vein.