It’s the programmer that
@rand Your opinion is noted, but perhaps it would be best if we just agreed to disagree about the topic, as most other people don’t seem to share the same opinion in spite of also being reasonably well informed.
The ease of which it’s possible to express dynamic scoping with implicits
This is not dynamic scoping. This scoping is resolved entirely statically. This is implicit parameters.
I like that implicits will make OCaml better in a range of ways - but wouldn’t it be nice if we could come up with a design for implicits where it wasn’t just replacing the complexity by another kind of complexity.
You’re right, I wish I’d thought to design that system instead of working for years in my spare time on this stupid current design. (Sorry to be flippant, but it is a pet peeve of mine that people don’t realise how insulting casual suggestions like this are. As should be obvious, I’ve spent a lot of time going over the ins and outs of these issues, suggesting that there is a simple solution is basically just insulting my intelligence. Also the subtly thrown in “we” that implies that our efforts in this area are comparable annoys me as well. Obviously this shouldn’t dissuade people from questioning, querying and criticising the work I’ve done – if the work is any good it should be able to withstand such criticism and even be improved based on it – but I would appreciate it if people didn’t imply that there are obvious and easy solutions to the problem).
And where instances are placed in global/program scope (including libraries). Could one maybe support a compiler-flag where all implicit instances were global?
No. As my paper make very clear type classes are incompatible with OCaml. They are completely anti-modular, they assume that you cannot abstract types, which is the cornerstone of OCaml as a language. They are also easy to write code with that is just as confusing and hard to reason about as your examples.
They are also inferior in many ways and are fundamentally the wrong thing in a number of situations, which leads to dubious design decisions. When you create a “partial order” instance for the Int type with type classes it is equivalent to saying “Int is a partial order” which is of course nonsense – it is the instance which is a partial order. Proper mathematical practice does not say “integers are a partial order” it says “the dependent sum of integers and these operations are a partial order, when it is obvious from context we will omit the operations” – this is what implicits gives you. The type class approach leads to things like parametrising the set type by a type, rather than parametrising it by an instance/module which is both more correct and more expressive.
As I’ve demonstrated your examples of hard to reason about code already essentially exist within the language, as do a myriad of other features that can be used to create hard to reason about code. Whether you like it or not, your ability to reason about the code you maintain is dependent on your collaborators following a wide variety of explicit and implicit conventions that are not enforced at the language level. Obviously as language designers we try to design features that encourage people to write good code, but we do not throw away features that enable people to write bad code, especially when they open the door to making much existing code easier to reason about and maintain.
I’m sorry if I sounded rude, that was unintended. The ‘we’ I meant was more as a ‘we the OCaml community’, but I can see how it can be seen the other way.
I don’t know how I would be able to suggest anything, if not simply - I’m not a language designer, so I’m just throwing a ball at the subject, to get to know the shape of it. The thing I feel that I know of, is the experience of programming in different languages, and I really care about code-style - so this is the primary thing that I intended to supply with this discussion. My drive to question this feature is my love for the language as I know it.
My observation from Scala is that the possibilities in the language influences the design of libraries - and as libraries can enforce a lot of code-style by their design, and programmers tend to want to reuse existing code others have made, it’s not only the collaborators conventions that define the style of the code. It’s not everyone that makes all their own libraries.
Though, I can believe that there is a high chance that the ideals of the OCaml community will be enough to enforce good library-designs in the future, lets see.
The problem in this discussion is that, from the very beginning, I have the strong impression that you have a bad experience with implicit in Scala and so you think It will be the same with modular implicit. But the design of the proposal is far more closer to what are type classes in Haskell, i.e. implicit dictionary parameter.
Have a look the article Implementing, and Understanding Type Classes by Oleg Kiselyov. Then read again the proposal from @lpw25, @yallop and @let-def, and try to understand what they did, why they choose modules as dictionaries and why they choose to elaborate the things with first-class functors.
Basically the two systems are the same things but, to be honest, modular implicit will be more powerfull just because ML modules system is more powerful. Just take this signature:
module type Ord = sig
type t
val cmp : t -> t -> int
end
we can already define a first-class functor with it:
let cmp (type a) (module O : Ord with type t = a) x y = O.cmp x y;;
val cmp : (module Ord with type t = 'a) -> 'a -> 'a -> int
and use it explicitly:
module Int_ord = struct
type t = int
let cmp x y = x - y
end
cmp (module Int_ord) 1 2;;
- : int = -1
what the type classes system in Haskell says is that this module type
module type Ord_on_int = Ord with type t = int
is a singleton type (the unique instance of the classe on the type int), which is trivially wrong. So, what modular implicit says is that if among all the inhabitants of that type there is one you will always use then you can use it implicitly and avoid writing boilerplate code.
I’m sorry if I sounded rude, that was unintended. The ‘we’ I meant was more as a ‘we the OCaml community’, but I can see how it can be seen the other way.
No worries. I read it more as a careless use of language that happens to frustrate me rather than rude. People do roughly the same thing fairly regularly and after a while it starts get to me, so I thought expressing my frustration might encourage people to be a bit more careful with how they phrase their criticism.
I don’t know how I would be able to suggest anything, if not simply - I’m not a language designer, so I’m just throwing a ball at the subject, to get to know the shape of it.
And that’s fine. It’s more a question of how it is phrased. It’s the difference between suggesting that we do A and asking why doing A won’t work. The first implies that I haven’t even thought of A whilst the second acknowledges that I probably have and have some reason for not doing A.
My observation from Scala is that the possibilities in the language influences the design of libraries
Certainly true, and where possible its good to have a language encourage the good patterns and rule out the bad, but where that is not possible all is not lost – there are other ways to encourage people to use the good patterns beyond having the language enforce them.
Good OCaml code almost never uses open but (short) module aliases instead.
This strange programmer is probably someone who goes fast…
and breaks things.
I didn’t say no one shares his opinion. Clearly a few people agree with him. On the other hand, lots of people are really, really hoping to see modular implicits integrated. The point is that arguing about it isn’t likely to change people’s minds very much. I think the bulk of the community wants the feature, and some want it very badly.
Regardless, and this was my point, restating the same arguments about why you don’t want the feature won’t change people’s minds very effectively, and after a while it becomes rather repetitive.
I think @rand has been constructive and respectful in his or her posts so (s)he’s fully entitled to ask questions or try to understand the topic better (and perhaps help others, unacquainted with this topic, think about it in more detail). If some people are bored with this discussion, no one forces them to read this very discussion or even to answer.
I didn’t say no one shares his opinion. Clearly a few people agree with him. On the other hand, lots of people are really, really hoping to see modular implicits integrated. The point is that arguing about it isn’t likely to change people’s minds very much. I think the bulk of the community wants the feature, and some want it very badly.
I wouldn’t be surprised if your assessment was based on a smallish number of extra enthusiastic people.
It would be good to have some data on the opinions of current OCaml users, that’s what I was saying. I realize this is probably impractical. Even a questionnaire will reach only those motivated to go looking for it.
It’s fairly common to damage a good system by adding a series of “awesome” features. For example, I consider C++ to be impossibly complicated, full of redundant features, and quite difficult to understand. Whereas C was really pretty fantastic for what it is.
OCaml is already quite complicated. I personally would be looking for ways to make it less complicated.
Take care,
Jeffrey
Thanks to @rand and others.
Is there someone aware enough of Ocaml and Modular Implicits (and much more because a broad PL culture seems required here) to make a summary of this very long discussion? (pros, cons regarding safety, easiness, etc.)?
IMHO, a feature that could reduce safety should not be integrated in a PL. And if it is, libraries which are implemented with such a feature should be clearly marked as “X feature inside (possibly harmful)”.
Technical decisions are rarely best made by democratic vote. Not all users of OCaml have equally useful opinions. I think, for example, that my opinion isn’t worth as much as that of the compiler maintenance cabal; they know far more than I ever will.
Sure, but I’m reacting to your claim that many people are in favor of the change.
Please let’s not hijack the discussion with “meta” questions. The topic here is technical and software engineering aspects of modular implicits. @rand’s, @kantian’s and @lpw25’s interesting posts were about that.
(I thought my message was a private email message, sorry.)
Sorry for answering so late, it takes me some time to find how I could answer you.
It may be difficult to give you a summary of the overall discussion, and It will certainly be partial and biased. Consequently I’ll stick to a more objective point: trying to give an overview of the modular implicits proposal. This has not been done until now, and the discussion would have been easier if we had started with this.
To do so, I will take as a guideline the List.sort function of the standard library.
According to standard library documenation, this function has for signature:
val sort : ('a -> 'a -> int) -> 'a list -> 'a list
The first argument (of type 'a -> 'a -> int) is intended to define an ordering on the elements of the list given as the second argument. In mathematics this kind of functions is called a linear order or a total order. When we paired the underlying type (on which the order operates) with this ordrering, we obtained what is called an ordered set. In OCaml this translates to a module signature:
module type Ord = sig
type t
val cmp : t -> t -> int
end
At this point, we can look at the sorting of a list from another point of view: to sort a list we need an ordered structure on the type of its elements. To encode this in OCaml we need a function that can take a module as an argument: this is what is called a first-class functor. Thanks to first-class modules, introduced in OCaml 3.12, we can define such a function:
let sort (type a) (module O : Ord with type t = a) = List.sort O.comp;;
val sort : (module Ord with type t = 'a) -> 'a list -> 'a list = <fun>
And we can use it with:
module Int_ord = struct
type t = int
let cmp x y = x - y
end
sort (module Int_ord) [2; 1; 4; 3];;
- : int list = [1; 2; 3; 4]
Now, we could say: sure we can sort lists, but we can also sort arrays; what if we could abstract the type of the containers? In OCaml we can express that a cointainer is sortable if it can satisfy this module signature:
module type Sortable = sig
type 'a t
val sort : ('a -> 'a -> int) -> 'a t -> 'a t
end
This signature is not satisfied by the imperative arrays of the standard library, but in addition to lists we can think of functionnal arrays or functionnal vectors for instance.
In the spirit of the previous use of first-class functors, we could want to write something like this:
let sort (module C : Sortable) (module O : Ord) c = C.sort O.cmp c
Unfortunatly, this is not possible with the current implementation of first-class modules: the problem here is that a container is not only a base type (as in the case of Ord) but a type constructor. The possibility to abstract over type constructors, aka higher-kinded polymorphism, is not currently supported in the core language and one has to rely on the verbose module language to do so.
Higher-kinded polymorphism in the core language is one of the features provided by modular implicits. With them it will be enough to write:
let sort {C : Sortable} {O : Ord} c = C.sort O.cmp c
And then we could write:
sort {List} {Int_ord} [2; 1; 4; 3];;
- : int list = [1; 2; 3; 4]
That’s fine, but it seems that we do not gain anything compare to:
List.sort Int_ord.cmp [2; 1; 4; 3];;
- : int list = [1; 2; 3; 4]
Hence the next question. What if we can ask the compiler to fill the gap for us and simply write:
(* I ommit the module parameter instances *)
sort _ _ [2; 1; 4; 3]
(* or more briefly *)
sort [2; 1; 4; 3]
That’s where the implicit feature comes into play.
We already have in the language an implicit feature with the type inference mechanism. Consider the trivial identity function:
let id x = x;;
val id : 'a -> 'a = <fun>
Here the programmer doesn’t need to annotate the code with type, the compiler automatically infer the most genereal type for this function, namely 'a -> 'a.
In programming languages without parametric polymorphism (as C) there is one identity by type, they all do exactly the same thing: returning their parameter. With parametric polymorphism one can abstract over these types and defines only one function. If we were fully explicit, we should write:
let id (type a) (x : a) : a = x
In spirit this valid OCaml syntax is identical to this non valid one:
let id (a : type) (x : a) : a = x
id est the function id takes two parameters: a type a, a value x of type a and returns a value of type a, that is x itself. Since types are not first-class values, we never pass ourselves the type to the function and the compiler does this for us.
We can also be less explicit with this notation:
let id (x : 'a) : 'a = x
or even less explicit with this one:
let id (x : _) : _ = x
This last notation should remind you the one I use previously with the sort function:
sort _ _ [2; 1; 4; 3]
And in the same way we can fully omit type annotations and define id with:
let id x = x
with modular implicits, it’ll be possible to call the sort function with:
sort [2; 1; 4; 3]
To do so with the above example, you’ll have to define some modules as possible modules to fill the gap:
implicit module Int_ord = structure
type t = int
let cmp x y = x - y
end
implicit module List_sort = structure
type 'a t = 'a list
let sort cmp l = List.sort cmp l
end
But in the same way that nobody can force you to use implicit type annotations, nobody can force you to use the implicit feature with modules. No matter how will be designed the library you use, if you want to always explicitly pass the module arguments you could still write:
sort {List_sort} {Int_ord} [2; 1; 4; 3]
Just to conclude this presentation of the features, and answer to the question if it will make the code harder to read and to reason about, I’ll quote what @lpw25 said:
I hope I managed to show that the implicit feature “is not a whole new kind of thing that you need to deal with – it is an extension to an existing aspect of reasoning about your code”.
I will note that in Coq, a would indeed be a required parameter. Coq permits you to omit it, though, using an implicit argument mechanism. I have yet to see a Coq user complain that their code would be clearer if they had to explicitly pass all the types parameters all the time — one can if one wants to, but no one ever wants to.
Incidentally, @kantian, this is a sufficiently clear and concise explanation that I think it would be nice if we transplanted it to OCamlverse, provided you are willing to permit that.
I know and this syntax is the one of Coq. The implicit argument mechanism is described in the Amokrane Saïbi’s thesis (in french) and has, since the beginning, heuristics for implicit or canonical records that is analogous to the modular implicits proposal (described here in english).
Sure you can put it on OCamlverse. You already asked me last time for my presentation of functors, and it’s very nice to ask, but the next time feel free to do what you want with my comments (consider them as under CC-BY-SA ). 