Modular Implicits

compiler
faq

#1

Are we going to merge this to master? If not what’s blocking it? Thanks!


What is the preferable solution for the role of standard library?
(WIP) Frequently Asked Questions
#2

This question comes up fairly often. Perhaps it should be in a FAQ of some sorts? r/ocaml has a stickied thread about multicore due to the endless questions of this sort. Maybe it makes sense to gather what is known about this topic in 1 place.


#3

I think that’s a good idea, although to me the best place for such FAQ would be the project page on OCaml Labs website.

I’ve been following the project since its initial announcement. Sadly the modular implicits fork has not been very active in the last year, at least publicly, and, as far as I know, there has been no announcement on the project roadmap and future neither from OCaml Labs nor the core devs. A relevant question on GitHub from a couple of month ago was closed with “no roadmap because it is hard to explain to mere mortals”. While I do understand @lpw25 point there, I believe it would still benefit to the community if the work on modular implicits was a bit more open.


#4

Suppose I just wanted polymorphic versions of the four common arithmetic operators that would work with both floats and ints. Is there a version of the modular implicits fork that I could use, safely, probably, now?

Some days the clutter of dots in float arithmetic really bothers me.

(I appreciate that there might be contexts where it’s safer to use different operators for float and int arithmetic, but sometimes convenience and clarity are more important.)

(I don’t assume that getting the four arithmetic operators to work with floats and ints in all situations is necessarily simple. I know that I have no idea what’s involved.)

(One of several reasons I decided to learn OCaml even though I was very happy doing what I was doing in Clojure was that, even though I’m extremely comfortable with Lisp syntax, for arithmetic, prefix notation will never be as easy to read as infix notation. Decades of math notation has its effect. But I find Clojure arithmetic easier to read that OCaml float arithmetic!

Don’t make me use Haskell or F# ! Just kidding. I have other reasons to avoid them.)


#5

I agree that for computation-heavy code doubling the size of common operators can be too much. However, even without modular implicts, I find that local opens combined with local redefinition of these operators, e.g.

 module Float = struct
   let (+) = (+.)
   let (-) = (-.)
   …
end
let normal mu sigma2 x = let open Float in
  exp ( - (x-mu) ** 2. / (2. * sigma2) ) / sqrt ( 2. * sigma2 * pi )

alleviate much of this pain. The main exception being functions which heavily mix integer and float arithmetic for which modular implicits would be useful. However, in my experience, these cases are not that common.


#6

Oh, very nice. I didn’t think of that. I’m going to start using it immediately.


#7

If it is reading rather than typing the dots that bothers you, Tuareg can help you with that thanks to prettify-symbols-mode:
Tuareg

P.S. you must be careful with the expression as written in the original post: -(x)**2.parses as (-x)**2. not as -(x**2) — which is the mathematically correct way. This is an quirk in OCaml syntax that unfortunately has not been fixed for fear that this would affect people using that “feature”.


#8

Interesting, and very nice. I’m not sure it’s right for me at the moment. I like knowing exactly what I’m typing, and although my fingers were once Emacs-linked, they’re now Vim fingers. :slight_smile:


#9

I asked the relevant people (Leo White, Jacques Garrigue and Frédéric Bour) at ICFP in early September, and I thought that people may be interested in a summary of “where we are right now”. Please remember however that (1) I am not personally working on modular implicits, so I may very well be wrong on various points and (2) Leo, who is working on modular implicits, has provided an explicit non-response indicating in particular that giving detailed explanations on a work-in-progress is taxing. For these reasons, please be considerate in how you respond and whether to ask further questions.

My understanding of the current status is that:

  1. there is wide consensus that the feature is important and desirable
  2. there is no consensus, or even clear picture, of whether the type system (module system) changes implied by the feature preserve the desirable properties of the OCaml type system (soundness and principality); Leo says they do, but no one else knows.

The plan for the future is to have (1) a theory of the feature that people agree on and (2) a type-checker that implements this theory. Right now, Leo provided a draft of (1), but it is substantially more powerful/complex than what the OCaml type-checker currently implements. We need to bridge that gap, by making the theory simpler, or the type-checker beefier, probably a bit of both.

One reason why this takes time is that this is very specialized work, with only a handful of people with both (1) the skillset to work on this and (2) time they are willing to volunteer for this. They are effectively working at the time scale of research, which is a long time scale.


#10

I stand by my non-response in that I’m not about to get involved in a detailed discussion here. But I just wanted to point out that with:

(soundness and principality); Leo says they do, but no one else knows

I think soundness is generally accepted as not really an issue – they basically elaborate into existing OCaml constructs. It is on principality, and more generally on similar properties of the inference itself where things are less clear.


#11

@lpw25 : Did you have some discussion with the Coq Team on this subject ? In Coq, there is canonical structures, since more than 15 years, which are analogous to Modular Implicit. The system is explained in the article Canonical Structures for the working Coq user by Assia Mahboubi and Enrico Tassi. There is also a mechanism of implicit arguments. Both are based on the Coq’s unification algorithm.

The article’s abstract is :

This paper provides a gentle introduction to the art of programming type inference with the mechanism of Canonical Structures. Programmable type inference has been one of the key ingredients for the successful formalization of the Odd Order Theorem using the Coq proof assistant. The paper concludes comparing the language of Canonical Structures to the one of Type Classes and Unification Hints.

Hope this will also give some guarantee to @gasche about the type soudness of such a system.


#12

There’s plenty of prior work on a variety of similar systems. I’m fairly confident I’m familiar with all the relevant literature. As I said, the interesting question is not soundness but predictability of inference.


#13

Given that there is a working prototype of modular implicits, is the problem simply proving principality in the general case, or have actual problematic examples been found?


#14

The problem isn’t really with proving things. The prototype is just that – a prototype – it is not a full implementation. There are plenty of parts not yet implemented and most of these parts are not yet precisely specified. They need a precise specification, producing that specification and making sure that it has predictable inference is the thing that still needs to be done. Obviously the most reassuring way to “make sure that it has predictable inference” is to prove it – but we’re not at that point yet.