[0] The paper gives set-union as an example.
[1] https://www.youtube.com/watch?v=hIZxTQP1ifo . (Sorry for throwing video at you -- there's probably a write-up somewhere, but I'm in a bit of a rush, and this was the thing that came to mind.)
Now we just need a Haskell compiler which actually bothers to provide the "pretty essential for sanity" for global uniqueness. Currently, I count zero compilers in common use which do.
(EDIT: Just to forestall the inevitable: Yes, there are some weird and dangerous extensions you can enable, but mostly it's pretty clear that they're dangerous. It doesn't seem to be a problem in practice.)
Because they never bothered to actually implement the checks to guarantee global uniqueness in GHC?
> (EDIT: Just to forestall the inevitable: Yes, there are some weird and dangerous extensions you can enable, but mostly it's pretty clear that they're dangerous. It doesn't seem to be a problem in practice.)
No weird and dangerous extensions in use. Vanilla Haskell.
Sure they did. Orphan instances are detected by the compiler.
Orphan warnings tell you that you defined an instance in the wrong place.
Things you don't receive warnings for:
- Defining the same instance twice.
- Having code which uses both instances.
Sorry, orphan warnings are multiple magnitudes of escalation levels away from what should happen and are focused on something different (code hygiene vs. THIS-CODE-IS-WRONG-AND-BROKEN-AND-WILL-CORRUPT-SHIT-AT-RUNTIME-I-WILL-FAIL-TO-COMPILE-THIS).
I believe I've understood the issue, but if I've misunderstood then I feel extra need to comment, that my misunderstanding might be clarified.
From my first reading of what you'd written, tome seemed spot on.
On careful re-examination (after reading this comment), I think when you said "Things you don't receive warnings for:" you did not mean to say that you can write that code and receive no warnings (a reasonable interpretation), but that the warnings would not read as directed at the points you raise (also a reasonable interpretation) - which (you note) are substantially more important than "this is generally a good idea."
I claim that if you never have orphan instance warnings then your code has "the guarantees Kmett keeps boasting about". In particular you can never "define the same instance twice", and this of course implies that you cannot "have code which uses both instances".
What exactly is your complaint and why does my claim not address it?
In haskell you can just say `show a` as long as `a` is of a type that implements the `Show` typeclass, but OCaml currently has no good answer to this. You end up with `Int.to_string a` or what-have-you. It isn't less powerful, technically, just more verbose.
Modular implicits allow you to define a function `show : (S : sig type t show : t -> string end) -> S.t -> string` and then mark the first argument implicit, so you can call `show a` and the compiler fills in the first argument with the appropriate module for the type of `a`.
There are proofs that this particular feature of typeclasses is impossible to put into OCaml's module system (something to do with functors and type aliasing and not being able to ensure that there is a unique `Show` instance per type), but modular implicits come close.