6 ms·

Okay I (having done a little Haskell and enough F# to know a higher abstraction was needed) thought that modules were already OCaml's counter to Haskell typecla

by daxfohl 11y ago

Okay I (having done a little Haskell and enough F# to know a higher abstraction was needed) thought that modules were already OCaml's counter to Haskell typeclasses, and they were already better. Some weird set-theory-looking T-shirt (obviously) proved it. So what are modular implicits, and how are they better than modules and typeclasses, why are modules not actually enough anymore as an answer for typeclasses, and are they (please no) related to Scala implicits?

mercurial 11y ago
You don't get "magic" to_string and equals with just modules, for instance.
- daxfohl 11y ago
  explain? And how do modular implicits fix?
  - thedufer 11y ago
    Under the current module system, there is no single polymorphic `to_string` function. You end up with a separate function per type, typically residing in different modules. 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.
pauldirac137 11y ago
Modules are strictly more powerful than Haskell type classes (at least, more powerful than naive type classes; there are so many extensions that I'm not sure that is still the case). Modular implicits are described here: http://arxiv.org/pdf/1512.01895.pdf http://arxiv.org/pdf/1512.01895.pdf. The main problem with modules as typeclasses is that it's pretty painful to use in practice, and modular implicits fix that, giving a solution quite reminiscent of Haskell type classes. I don't know Scala implicits well enough to comment, but the authors feel their version avoids most of the problems in Scala's implicits (they jokingly refer to it as "a more explicit kind of implicit").
- lomnakkus 11y ago
  AFAIUI modular implicits don't give you global uniqueness. While this can be "worked around" in some cases[0], it's not really possible in the general case, and global uniqueness is pretty essential for sanity when writing higher-level code[1]. [0] The paper gives set-union as an example. [1] https://www.youtube.com/watch?v=hIZxTQP1ifo 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.)
  - airless_bar 11y ago
    > [1] https://www.youtube.com/watch?v=hIZxTQP1ifo https://www.youtube.com/watch?v=hIZxTQP1ifo 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.
    - lomnakkus 11y ago
      Not sure what you mean. Could you elaborate?
      - airless_bar 11y ago
        GHC gives you none of the guarantees Kmett keeps boasting about.

by daxfohl 11y ago

mercurial 11y ago

You don't get "magic" to_string and equals with just modules, for instance.

daxfohl 11y ago
explain? And how do modular implicits fix?
- thedufer 11y ago
  Under the current module system, there is no single polymorphic `to_string` function. You end up with a separate function per type, typically residing in different modules. 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.

pauldirac137 11y ago

Modules are strictly more powerful than Haskell type classes (at least, more powerful than naive type classes; there are so many extensions that I'm not sure that is still the case). Modular implicits are described here: http://arxiv.org/pdf/1512.01895.pdf http://arxiv.org/pdf/1512.01895.pdf. The main problem with modules as typeclasses is that it's pretty painful to use in practice, and modular implicits fix that, giving a solution quite reminiscent of Haskell type classes. I don't know Scala implicits well enough to comment, but the authors feel their version avoids most of the problems in Scala's implicits (they jokingly refer to it as "a more explicit kind of implicit").

lomnakkus 11y ago
AFAIUI modular implicits don't give you global uniqueness. While this can be "worked around" in some cases[0], it's not really possible in the general case, and global uniqueness is pretty essential for sanity when writing higher-level code[1]. [0] The paper gives set-union as an example. [1] https://www.youtube.com/watch?v=hIZxTQP1ifo 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.)
- airless_bar 11y ago
  > [1] https://www.youtube.com/watch?v=hIZxTQP1ifo https://www.youtube.com/watch?v=hIZxTQP1ifo 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.
  - lomnakkus 11y ago
    Not sure what you mean. Could you elaborate?
    - airless_bar 11y ago
      GHC gives you none of the guarantees Kmett keeps boasting about.