7 ms·

This actually doesn't have to do with that. They "propose a redesign of ML in which modules are truly first-class values, and core and module layer are unified

• tachyonbeam 11y ago
  Can you elaborate on why these are problems for ML?
  • oggy 11y ago
    Erasing that distinction enables some goodies such as first-class type constructors, which makes it possible to manipulate types of higher kind. This in turn, presumably enables things like Generalized Algebraic Data Types.
    • platz 11y ago
      the monad example in 1ML is: type MONAD (m : type ⇒ type) = { return a : a → m a; bind a b : m a → (a → m b) → m b }; map a b (m : type ⇒ type) (M : MONAD m) (f : a → b) (mx : m a) = M.bind a b mx (fun (x : a) ⇒ M.return b (f x)) (* : m b *) not too bad.. though I wonder if things are defined structurally instead of nominally, which monad instance are you going to get for a given expression. Haskell's "one instance per class" rule means the compiler figure out which monad instance to apply. This looks more flexible, but also looks like it will require more annotations and explicit parameters.
      • tel 11y ago
        You have to explicitly pass the monad "vtable". If 1ML also grabs up modular implicits then you'll have a sensible way of passing implicit arguments not exactly unlike that of Haskell, but modularity and global canonicity are at odds so you have a more complex reasoning task.
      • iskander 11y ago
        If you combine this with [modular implicits](http://www.meetup.com/NYC-OCaml/events/222026251/ http://www.meetup.com/NYC-OCaml/events/222026251/), which are hopefully going to be added to OCaml soon, then you'll get something which is nearly as syntactically neat as type classes but more powerful.
        • platz 11y ago
          More power in terms of flexibility, but the mechanism of implicits makes it less clear which instance is in scope for a given expression. With true typeclasses, there is no ambiguity which instance will be selected (there can only be one) This distinction is often lost when comparing true type classes with their emulation via implicts. Sometimes "more power" is not what you want i.e. this is more of a tradeoff.
          • andolanra 11y ago
            The proposed OCaml implementation of modular implicits[1] considers ambiguity a compile-time error, so in that case you'd have to manually indicate which module you're passing in. (This is in contrast to Scala, in which there's an elaborate mechanism for resolving ambiguity in implicits which makes it hard to know which is being selected.) So the OCaml implementation shouldn't make it any more difficult to discover which implicit is in use in a given context, because if an implicit is used, then it must necessarily be unique and there will be no ambiguity. [1]: http://www.lpw25.net/ml2014.pdf http://www.lpw25.net/ml2014.pdf
            • platz 11y ago
              the section "6.5 Modular type classes" was very interesting. Although they did mention some restrictions as well.
    • zem 11y ago
      ocaml already has generalised algebraic datatypes as of 4.0: http://caml.inria.fr/pub/docs/manual-ocaml-400/manual021.html#toc85 http://caml.inria.fr/pub/docs/manual-ocaml-400/manual021.htm...
  • andolanra 11y ago
    One of the classic motivating examples (which is addressed in the 1ML paper) goes like this: Both trees and hash tables can be used to implement map-like data structures. You could, in ML, have an abstract signature for Map types that gets implemented sometimes by a concrete TreeMap implementation and sometimes by a concrete HashMap implementation. HashMap would be a better choice if the expected number of entries is larger, and the TreeMap would be better if the expected number of entries is smaller, so what we'd like to do is write something like module Map = if size > threshold then HashMap else TreeMap so that we choose what concrete implementation we want at runtime—but we can't really do that, because the language we use to talk about modules in ML is distinct from the language we use to talk about values. That is to say, the size > threshold part can't coexist in the same expression with the HashMap and TreeMap part. Some MLs have added the ability to wrap modules in values, so you can write it this in OCaml: module Map = (val (if size > threshold then (module HashMap : MAP) else (module TreeMap : MAP))) : MAP but it's a bit awkward because of the explicit moving-back-and-forth between value-level and module-level, and the interaction between the two languages has some rough edges (which the paper explains more thoroughly, if you're interested.) The motivation for 1ML is that we'd like to use the same language to talk about both modules and values. That way, we could write the first, simpler definition without having to worry about the fact that we're manipulating distinct 'things'. Of course, there are other tradeoffs involved in the 1ML solution, but it's an interesting, compelling experiment.
    • hoprocker 11y ago
      Thanks for pulling this out and explaining it; although I'm not familiar with ML, I get what the problem is here. Interesting!
    • rtpg 11y ago
      how does that end up working for typechecking? does the Map module end up having all the properties of the intersection of these elements? The Map example seems pretty easily solvable via Haskell through typeclasses or the more standard OOP-y languages through interfaces, but am I missing something? Does SML not have the tools for this right now?