Saw this while doom scrolling on X.
Raises some great points about various forms of function overloading and the problems it creates—a great case for module functors, if you ask me!
Let’s think long and hard before anyone gets too eager for modular implicits in OCaml.
Two responses:
(1) A type error is an unintended condition[a] which might manifest in multiple stages of a program's development.
But this is saying that type errors are any error whatsoever. Any error. That’s not what type-safe programming ever promised, unless you’re an adherent of constructive type theory and proofs-as-programs.
(2)
Parametric polymorphism doesn’t help you either. You really need to be completely and explicitly monomorphic in all your types, right? I can retell that story with parametric polymophism:
(a) you start off with a type settings containing an allow_list:
type settings = {
allow_list : client_id list ;
…
}
(b) somewhere else, somebody wants its length:
let allow_list_count settings =
List.length settings.allow_list
;;
(c) and then, in order to implement our desire to let everybody in, we change the allow_list slot from client_id list to client_id list list. So [[a;b;c]] is three clients, and [[]] is no clients. And voila, that code in #b always returns 1.
====
Yes, ad-hoc polymorphism can allow you to write code that does unintended things when its environment changes. This isn’t surprising.
I thought I should make a couple more responses, b/c I felt like I was pushing-back too hard.
(1) This guy isn’t wrong.
There is a well-established learning among the hardest-core systems folks, that “template-based metaprogramming” (the C++ equivalent of traits/typeclasses/modular implicits) is something to be used only with the greatest of trepidation. For instance, the Google C++ Style Guide (circa 2015) explicitly forbade it. Now I’m sure there’s template code in system libraries used in Google’s C++ corpus. But the guide was for programmers outside the trusted core of library maintainers. And for them, that guidance is pretty much golden.
And this isn’t so surprising: you look at any language that allows even a modicum of metaprogramming (Ruby, Python), and you’ll find that using the metaprogramming tools (as opposed to using the -products- of metaprogramming) is going to be a dangerous thing. That doesn’t change the simple fact that trait-based programming is fundamentally more labor-efficient than doing it the way we do in OCaml – with module-names everywhere.
(2) there’s a reason traits/modular-implicits are so valuable
When I was working in quantum computing, I had occasion to add some support for input/output to standard sparse-matrix formats, to a (the?) Rust sparse-matrix package ( sprs - Rust ). I didn’t do anything oh-so-big, but it wasn’t trivial. I also used this sparse-matrix code in parallelizing some quite intensive numerical code.
In all of this, it was apparent just how much more effective the Rust way (with traits) was than any OCaml way. And it became obvious why Python’s numpy was winning, even though it was dynamically-typed and some of the code was interpreted: for numerical code, to put in all the types, all the module-names, is to render the code unreadable. Just unreadable.
Maybe the answer is that OCaml doesn’t care about such areas of programming. I think that’s a mistake, but hey, it’s a choice.
From the cited article: “By semantic type-safety, I mean “preventing code that still type-checks but silently does the wrong thing because of a type error”.”
That should tell you all you need to know. The author does not know what he is talking about. Type checking has nothing to do with semantics.
I agree with everything that’s been said in this thread so far (the merits and demerits of ad-hoc polymorphism and the distinction between the semantic and type planes).
In the end, this is a classic trade-off between explicitness and implicitness (readability vs writability). The arguments for and against modular implicits have been well stated and I respect OCaml’s track record of moving at a moderate pace and adopting the “right” abstractions and features over time.
While I do agree with the author’s take that traits/type class/implicits hamper readability and therefore make the code less likely to be semantically correct (paraphrasing/reading between the lines here), I do think their examples are weird. For starters, if you’re trying to encode correctness in the types to make refactoring safer, you should be at a minimum wrapping type classes, etc., in newtypes that only you control and which are fundamentally tied to the resource you’re trying to protect. Using Maybe/Option here opens you up to that “semantic risk”. The general problem seems to be exacerbated in Haskell due to the point-free style. At least in Rust, it’s pretty clear that you’re directly converting the allow-list field (which has been turned into an Option) into an iterator.
I don’t know. I think it’s valid to call using a type with function it was never intended to work with a type error, because it is still related having the wrong type in the wrong place. His usage is also borderline for me, but if we think about JavaScript, there are many things which would be a type error in a sane language which are not type errors in JavaScript, but instead semantic nonsense. Likewise, there are semantic errors in OCaml that could be type errors in Idris or Agda. In TDD, one strives to encode more invariants into types, so various kinds of errors become type errors.
Perhaps it would have been more accurate to say that type classes errode correctness in a program, but to the author’s credit, he is talking about cases which would have been type errors without type classes, but become semantic errors in their presence.
So, you’re right that there is a slight problem with the language, but I don’t think it really diminishes the point that behavioral subtyping ad-hoc polymorphism can make something that would have been a type error into something that isn’t.
I think you make valid point that there are cases where it’s more beneficial.
I guess the question for OCaml becomes, is there a way to have modular implicts in a more controlled way? Maybe that battle is already won to some extent because the standard library and the whole ecosystem is already defined without them, and people are likely to continue using lists and options in the way we always have, and they really become a special thing where they are just used in a few areas—like maybe the implicts you want have to be explicitly “turned on” with something analogous to an import.
Have you programmed much in Rust? I did so for about a half-year, and even though I’ve been an ML programmer since the late 80s, I quickly became an aficionado of the “long chain of iterators” style of programming. With very few explicit types, and everything else filled-in by trait inference.
I’m not going to argue that anybody can write traits, and that one can import traits willy-nilly. Those habits will produce crazy code that nobody understands and nobody can maintain in the face of changing libraries. It’ll be hell. Instead, what’s needed is -strong- curation of libraries of traits, so that they’re well-behaved and users can rely on them without investigating too much their implementations.
The same thing will have to happen if OCaml gets modular implicits.
So now I’ll say a very strong thing:
The OCaml community has tried a few times to build up math libraries. They’ve failed. Failed miserably. I think looking at Rust’s success, and how that success is critically due to traits, should teach us that sure, OCaml can decide that “all numerical computing is irrelevant, and hey, if you wanna do machine learning, go learn Python or C++, b/c OCaml ain’t for you dude.”
And “just wrapper Tensor flow in OCaml bindings and that’ll be good enough” is just saying that OCaml is a scripting language, and we’re never going to actually be a first-class choice for those implementation areas.
OCaml needs modular implicits, b/c without them numerical computing is intolerably verbose and people simply will not put up with it; they’ll go to other languages.
I have to admit that as a Rust programmer, I think you’re both overstating the dangers of traits and the upsides relative to (applicative) functors. The orphan rule in Rust means that trait resolution typically happens locally–if you’re using a non-local trait, chances are very high that it came from the standard library or else from some well designed third party case. In most other cases, you’re using a locally defined trait that you fully control anyway. On the OCaml side: is it really so bad to have to use a functor application at different sites for different tensor types? Maybe I don’t have the right picture of what you’re imagining. I have yet to see a reasonable tensor/matrix library in the wild that encodes things like shapes into the type system in a useful way–I suspect that such a solution would require dependent types. On the other hand, it’s quite simple and useful to simply specialize tensor types per element type, and this is how basically every library under the sun does it anyway. (NB: IIRC, the Burn library at least used to try to encode the number of dimensions in the type of a tensor, though not the lengths themselves; I’m not whether this is still the case, but it did add some friction when trying to do certain operations.)
In a nutshell: I don’t think things are quite as bad as others seem to think on either side and that things work “just fine” in practice. My main complaint about OCaml (not just in numeric programming, but in general) is the lack of control of memory layout when it really matters. Even just being able to drop down in some places (opt-in) would go a long way. But this is a very different conversation than ad-hoc polymorphism. 
Just an FYI, Julia encodes dimensionality into types. You can just flat-out have integers as type parameters. This doesn’t do much for type safety either way, as Julia does type checking at runtime, but it has some useful properties for multiple dispatch. You can, in theory, do other things with these integers in type signatures, but most novel uses are pretty terrible for the optimization strategies the compiler uses.
Can only say amen to that. I watched a talk a few years ago about what engineers at Jane Street have proposed to get over this (like adding boxed vs. unboxed as a property of every type), but I haven’t heard that anything has come of it. Would be great if it were possible to have an array of inline structs records in OCaml.
I have done a whole PhD in statistical physics, with most numerical simulation done in OCaml, and that worked very well and I more often than not regretted the few time I went with Matlab or Python. Numerical code in OCaml is certainly not doomed to be verbose, even right now.
Certainly, modular explicits will probably be an improvement when having to choose the field (aka the numerical precision).
Also, I am not sure what are you griefs with owl to say it failed miserably? (even if itt is certainly less maintained and developed than I would have hoped.)
But I don’t agree that there are any errors in the example code. The error is due to the programmer’s misinterpretation of the code. Count means count, it does not mean “on” or “off”. If you count a maybe, you get 1; if you count a nothing, you get 0. As should be expected. Nothing erroneous about it. The error is thinking that refactoring the code to use count to indicate allowability should work. From the article:
“In rust, the allow_list_count function using an ad-hoc polymorphic count still compiles but now only ever returns 0 (turned off) or 1 (turned on)”. A simple and obvious case of programmer type-error: treating an int as a boolean.
(One could debate whether or not Option should be countable at all, but that is a separate issue.)
Owl has an issue with verbosity that results from them trying to support every kind of tensor/matrix combination. The more types you have, the more you need to duplicate the operations for all of them, the more type-based dispatch becomes powerful. At the very least, you want int8, int32, float32 and float64 tensor support. That’s already quite a few types to duplicate all functionality for. Multiply by 2 for matrices if you want to distinguish them type-wise.
The next issue Owl has, has to do with reusing the Bigarray type for compatibility. This is convenient, but it means you don’t have good support for tensor views (read/write sub-indexing of existing arrays as if they are new arrays) at the level numpy has (Bigarrays have some view support, but Owl implements none of it), which is very important for efficiency.
Finally and perhaps most importantly, numpy’s DSL for slicing (based on the python slicing syntax) is concise and intuitive, and dovetails nicely with its view system: slice the precise view you want to the tensor, then use it to write to those locations in the original tensor or to copy just that slice to a new tensor. Or allocate a binary mask based on tests of the individual elements in the tensor, and then use that mask to modify specific elements of the tensor. You can accomplish a significant amount of stuff with this DSL, without touching any API methods. Trying to duplicate these operations with API calls in Owl is painful (requiring that you browse a tree of functions for every minor operation) if not impossible.
in 2022 when I started working in QC, I didn’t know Rust, and frankly, I sneered at it. I know C++, written significant codes in it, why do I need -another- language for performance computation? The QC corpus I was working with (IBM’s Qiskit) was written in Python (with numpy/scipy/etc) and there was talk about using Rust instead of C++ to accelerate some performance-critical bits (of which there are a lot in QC compilation and (esp.) simulation).
I’m an old-skool ML guy, and I know OCaml is much faster than Python: if I had a colorable excuse for using OCaml, I would have done it. But I started looking at Rust’s combination of polymorphism and traits, and it was … overridingly compelling. It’s true that some part is due to the fact that unboxing requires that we write code on floats, and separately on complex, on int, etc. But that’s not where most of the succinctness came from: it came from not having to write module-names/type-names for things like matrices/vectors/etc.
And it really is compelling: people who pooh-pooh it, saying “oh, you can do the same in OCaml” should try to implement (for instance) the Rust sprs (sparse matrix computation) package in OCaml. That was implemented by a third-party, not anywhere near the Rust core team, so a good test-case.
The points you raise are very good ones. However, the cheap view issue sounds more like an API design choice. First-class slicing syntax (or else some OCaml-friendly equivalent) is harder; I’m actually curious how that might be approached. In any case, without some explicit compiler support for the notation you’d want, it’s not clear how you would actually solve this with ad-hoc polymorphism, so that’s an orthogonal concern.
Type based dispatch would help to solve many of these issues.
Another issue I forgot is that if you want to multiply a tensor by a number, you need a special syntax (or specific function call) for that in OCaml, rather than just using the multiply symbol. This is death by a thousand cuts.
The basic principle is that heavy mathematical code needs uniformity across types and ease of access. If I convert float32 to int32 tensors, I shouldn’t need to hunt for the module that holds the new type’s functions to operate over the new values. If I multiply, the same multiplication symbol should work across types wherever it can. If I take a view of a tensor, I should be able to easily operate over any combination of tensor and view seamlessly.
So long as I’m only working in floats and integers, this isn’t so bad, but once you get an algebra that crosses over tensors, matrices, reals, integers, and converts between them and accesses them in different patterns, not having type-based dispatch becomes extremely painful, to the point that it’s just not worth doing. This is a universal observation: the more related types you have to work with in uniform patterns, the more current OCaml will become painful and the more you will wish for type-based dispatch such as modular implicits, typeclasses, objects etc.
I mainly agree with this but operator overloading can make code hard to read (e.g. to see what kind of multiplication is being performed).
I think the main problem with Owl is that it doesn’t have enough libraries.
I would like to support this view about owl:
(even if itt is certainly less maintained and developed than I would have hoped.)
I have been failing to install owl from opam on an ARM mac due to incompatible openblas compiler flags in the opam packages – this seems to indicate that currently essentially nobody is using owl on that OS? If that’s true, owl simply can’t be well-tested enough to be production ready.
Slicing syntax is available, not as succinct as python but workable IMHO. From the online docs at ocaml.xyz:
open Arr;;
let x = sequential [|10; 10; 10|] in
let a = x.${[0;4]; [6;-1]; [-1;0]} in (* i.e. Arr.get_slice *)
let b = zeros (shape a) in
x.${[0;4]; [6;-1]; [-1;0]} <- b;; (* i.e. Arr.set_slice *)
where .${} is a custom indexing operator for slicing over ranges. However, the slice always copies, so that a is not a view. This probably prevents a good deal of the uses of slicing in numpy. (Side note: a more general .!{} operator for slicing over indices, list or ranges is documented but not implemented, exemplifying my first point)
A more painful experience for me was trying to use AD in owl for optimization. As soon as any tensor or scalar needs to be differentiated through, it has to be wrapped in an opaque type, e.g. Algodiff.D.t, and from now on it’s unknown until runtime what functions will actually be able to digest it because it might be a scalar or tensor of any dimension. So, like python, but without the introspection or convenience.
I’m heartbroken about owl. I’m the target audience. I would like to use it. I even think adding module names and using monomorphic functions is not all that bad. But there is just so much work to be done in the details for it to become productive.
Out of curiosity: are the more attainable modular explicits going to streamline numerical code to some extent?
On a related note, I’ve never understood Haskellers’ general aversion to ML module systems. The arguments always fall in the way of comparing them to typeclasses. Yet, it seems to me that the second you have a situation where the canonical typeclass instance is not the one you want (in Haskell), you have a few options - one being to just devolve to dictionary passing style (which is effectively subsumed by functors and first-class modules). If you view the module language as being a bit like a type system for the specialisation of records (with OCaml providing neat extra things like first-class modules), it seems wildly superior - to me - for structuring programs at scale.
Personally, when I think of “ad-hoc polymorphism”, my mind first summons a memory of C++ spewing a bunch of template garbage to the screen because some ad-hoc overload couldn’t be resolved for some type (after several substitutions). So, by that standard, anything looks better to me. A compelling case for typeclasses, in particular, can be found in mathlib for Lean 4 (with a neat paper about using tabling for their resolution).