11 ms·

What was wrong with SML?

pjmlp 4y ago
What was wrong is not having a killer application or an industry giant pushing it. Grammar and language semantic are details regarding language adoption.
- eatonphil 4y ago
  Yup, adoption has nothing to do with being a sensible language. More often it seems to be completely inversely related.
  - exikyut 4y ago
    What are some sensible (coherent, load-bearing, force-multiplying etc) tools that have terrible adoption? Unreasonably open-ended question (suppose the scope is ML, or perhaps FP in general, or maybe even wider) - but I'm very curious.
    - youerbt 4y ago
      TLA+ or Nix comes to mind. By some notion of terrible I guess.
    - eatonphil 4y ago
      Google "worse is better". :)
    - pharmakom 4y ago
      I would say F#. It has most things you could want: - Proper functional programming support - Fast enough runtime - Cross-platform and open-source - Mainstream ecosystem - Large corporate backer - Compile to JS - Commercial and open-source tooling options … and yet C# is far more popular. This is because language adoption is driven by existing user base and other network effects NOT the quality of the language itself.
    - macintux 4y ago
      Erlang is underutilized at least in part due to its odd syntax, despite being a powerful tool. Elixir is helping address that, although I much prefer Erlang’s syntax.
throwamon 4y ago
A bit off-topic, but could someone ELI5 what a lattice is in this context?
- chombier 4y ago
  I think this refers to a system of types in which for any two types there is also an union type and an intersection type in the lattice.
- mjd 4y ago
  If you have two types, there should be a single type that "joins" them, in the sense that you can understand both of the original types as somehow being special cases of the join type. A join is not necessarily a union, since the representations of the three types might be completely different, and also because the third type might contain many values that don't correspond to anything in the two original types. (It might be much bigger than the union.) Mathematical lattices must also have "meets", which are like joins except down instead of up. I'm not sure that meets are as important as joins in this context.
- layer8 4y ago
  It refers to https://en.m.wikipedia.org/wiki/Lattice_(order) https://en.m.wikipedia.org/wiki/Lattice_(order), with the elements of the lattice being the arithmetic types and the order relation being the subtyping relation here. Given any two types in the lattice, the lattice property then guarantees that there exists a unique common (least) supertype (aka upper bound, supremum) of the two types. Which means you can apply the binary operation (e.g. addition) as defined for that common supertype.
chombier 4y ago
> Scala has a very different solution to this problem, called covariant and contravariant traits. I thought Scala had an even stricter value restriction than ML, where only function/methods may get a polymorphic type?
- samth 4y ago
  Yes, that statement is very confused. Scala doesn't do generalization, or polymorphic values, and thus the problem doesn't occur at all.
porcoda 4y ago
I still actively use SML - mlton or smlnj usually, polyml too. I’m aware of the issues raised in this post but haven’t ever found them to be a source of much headache. To be honest, the biggest headache is moving between compilers and their different build processes. Other than that, the fact that the language isn’t really changing is a big attraction for me. CakeML is also a very cool project in SML land.
- Karrot_Kream 4y ago
  I am curious what you use SML for. Any examples? Just interested in seeing what you can do in SML.
  - porcoda 4y ago
    Mostly programming languages related: code analysis, compilers, code generators, and formal verification tools. Outside PL work, I’ve used it to build some modeling and simulation tools. I also use it for misc. little tools that I need every so often where I want the type system to help me out. For a brief few years (‘09-‘15) Haskell played this role for me but I went back to SML after getting frustrated with various parts of that ecosystem.
    - Karrot_Kream 4y ago
      Oh modeling and simulation is an interesting idea, that sounds like a perfect thing to play around with SML for. Thanks!
- mbarbar 4y ago
  >CakeML is also a very cool project in SML land. I've been very interested in CakeML lately, do you use it for anything?
eatonphil 4y ago
I mentioned to Mark when I saw this, and he noted it in the addendum at the end, that calling Standard ML dead is a bit too much. I've written recently [0] about how active it surprisingly is. I also disagree that its failure to "succeed" has anything to do with syntax or semantics and solely that it doesn't have a Jane Street or any company publicly behind it. [0] https://notes.eatonphil.com/standard-ml-in-2020.html https://notes.eatonphil.com/standard-ml-in-2020.html
- porcoda 4y ago
  I don’t think it succeeded or failed. Languages don’t need to be wildly popular in industry to be valuable. I personally like that industry ignores SML. Even for Ocaml I don’t use the Jane street core: I just use the stock language since it’s small and stable. I like that Jane street helps improve the core compiler though.
  - pjmlp 4y ago
    Haskell's motto is "avoid success at all costs", after all.
- mjd 4y ago
  I would like to point out that the article does not use the words “succeed” or “fail”, and makes no claim about whether SML “succeeded” or “failed”. Indeed I don't think that is a useful question to ask. My article was trying to address a much less nebulous issue: what problems did I personally see with SML in the mid 1990s that let me to abandon it at that time.
  - eatonphil 4y ago
    Sorry, I didn't mean to put words in your mouth. I may just have gotten the wrong impression of your intent. Any criticism of any language is valid and good to have!
- gkuan 4y ago
  I do wonder if differences in language governance models impact uptake. Being completely biased (having worked on the SML/NJ compiler a long while ago), I very badly want to see more adoption. There is definitely continuing activity with new (IFL award winning) LLVM backend work [1] and Manticore. [1] http://cs.uchicago.edu/news/smlnj-overhaul/ http://cs.uchicago.edu/news/smlnj-overhaul/
Athas 4y ago
> Haskell's primary solution to this is to burn it all to the ground. Mutation doesn't cause any type problems because there isn't any. This is true, but I think it is also misleading. Haskell has the same problem if you use unsafePerformIO to create a polymorphic IORef at top level. You can then use this IORef to subvert the type system. I think this is something many Haskell programmers are not fully aware of: unsafePerformIO doesn't just break referential transparency; it can also fundamentally break memory safety. Now, you may say that unsafePerformIO is obviously unsafe (it's in the name!) and should never be used. But if you look at many foundational Haskell libraries, you will find that they use unsafePerformIO or similar functions internally, usually for performance reasons. What are the rules that govern safe usage of unsafePerformIO? As far as I can determine, these rules are basically just GHC implementation details, and people often get them wrong. And if you break these rules, you don't just get a function that doesn't do what you expected - you may have subverted memory safety entirely. I think this is an interesting conundrum. Haskell makes much stronger promises than SML, but if you break the rules, all bets are completely off.
jasonhansel 4y ago
IMHO Haskell's lazy evaluation has some significant disadvantages compared to SML's strict evaluation. In particular, lazy evaluation makes it difficult to find the performance bottlenecks in a particular piece of code or to determine the time complexity of an algorithm just by reading it. Furthermore, subtle changes in how a function is written (for instance, making a multiplication function not evaluate the right operand if the left operand is zero) can cause wildly unexpected performance changes in that function's callers. In effect, the performance of a function is no longer just determined by that function's structure and by the function calls it contains; performance of one function now depends heavily on the implementation details of others and the context in which that function is used. Granted, any optimizing compiler can have this effect, but it's rarely noticeable in strictly-evaluated languages, where at least to some extent the order of evaluation must correspond to the structure of the code.
- zozbot234 4y ago
  It would be nice to have a language that could treat both strict and lazy evaluation as equally first-class, as opposed to having one be the default (whether "strict" as in ML or "lazy" as in Haskell) and the other only being expressed by syntactical kludges. This may well be possible by relying on logically-inspired features like polarity and focusing, and endowing data types with strict or lazy "natural" polarities.
  - eatonphil 4y ago
    Any strict language can implement laziness. The inverse may(?) not be possible.
    - ravi-delia 4y ago
      It's the opposite, no? Basically every lazy language has some way to force evaluation, but in most strict languages laziness is never fully supported. Closest I can think of is a Scheme with continuations, but even then it takes some extra work. I know in CL even primitive laziness takes a lot of work and a code-walker, and whatever it's other flaws Common Lisp is at least adaptable.
eatonphil 4y ago
For folks interested in learning Standard ML, check out /r/sml [0] and the sticky post [1] with a getting started guide. [0] http://reddit.com/r/sml http://reddit.com/r/sml [1] https://www.reddit.com/r/sml/comments/qyy2gs/getting_started_with_standard_ml/ https://www.reddit.com/r/sml/comments/qyy2gs/getting_started...
shpongled 4y ago
SML is one of my favorite languages (I've been (very) slowly writing a compiler & language server for it). Sure, it has some warts/differences compared to newer languages - we have moved towards traits/typeclasses/etc, and I wish I could just write #[derive(Debug) - but I feel that SML fits in a very unique spot for programming languages. It's extremely simple, yet still powerful and expressive. I hope we will see continued work on SML/Successor ML descendants (like 1ML, etc), because I think there's still potential there I think some updated language tooling would dramatically help.
- jaytaylor 4y ago
  Is your development progress taking place in the open? (e.g. GitHub or somewhere similar) It sounds like a cool project and I'd love to see it! And even have the option to open a PR and help ;)
  - eatonphil 4y ago
    Yes, please share or open-source it even if it's not done!
    - shpongled 4y ago
      You have already linked to it :)
  - shpongled 4y ago
    I have the compiler on GitHub [1] - I just started working on it again after a 2-year hiatus (to finish my PhD). As for language-server, I'm currently sketching out some plans to use SMLnj's "Visible Compiler" feature, since that seems the easiest path forward. I have a half-baked language-server based on MLton's def-use output, but it's too unstable to share. I am planning to make some progress on the language-server in the next couple weeks. [1] You'll notice it's just a fragment of the language for now, and only half-implemented. https://github.com/SomewhatML/sml-compiler https://github.com/SomewhatML/sml-compiler and https://github.com/SomewhatML/sml-analyzer https://github.com/SomewhatML/sml-analyzer (again for a fragment of SML)
tialaramex 4y ago
SML was the First Language used for the Computer Science degree I took. I felt at that time, and continue to feel years later (that degree course now teaches Java as First Language) that this was a good decision despite the fact that most graduates don't end up using SML to write anything. In the course of my education I experienced some things which I'm convinced are a bad idea even though they worked out OK for me such as selective education (whole schools only for "talented" children) and single sex secondary education, but SML as First Language is not one of those things. It worked well for me and I'm convinced it's a good idea even though I would not advocate writing new real world projects in SML unless you've got some very particular reason.
- ravi-delia 4y ago
  I feel like there should be some expected order. Like BASIC->functional->scheme or something. Maybe switch them around, or throw in Python. There are a bunch of hurdles for new programmers to jump over, and it seems like maybe the best way to get them over them is with a different language for each. When my roommate took his intro CS course in Python he was mystified by type errors since they're often somewhat hidden. In Java the next semester the boilerplate made the whole program feel less understandable, but a semester or two later and it could have taught valuable lessons.
- wink 4y ago
  Interestingly we used OCaml in the first semester (by the professor's choice) in late 2003, and I hated it and failed the course. A year later I retook the course and as it was some other professor's turn it was SML, which I kinda liked. I did revisit OCaml more than 10 years later and actually enjoyed it, so maybe it was a bit of "wrong place, wrong time" but as I heard from some users it should have evolved quite a bit in those 10 years. (I am 95% sure it was not functional programming per se, but I never figured out what exactly was the culprit, I guess a dose of "I know how to code" was involved).
fanf2 4y ago
There was a history of Standard ML published as part of HOPL4 a couple of years ago - https://dl.acm.org/doi/10.1145/3386336 https://dl.acm.org/doi/10.1145/3386336 I was particularly interested by the more recent history, after SML '97, where there was plenty of interest in improving the language and its library, but Milner insisted that there would be no further changes, and the Definition was non-free so the others could not build on it. (It has since become Free though its source code was lost.) Despite that there is/was an SML Basis Library project, and a Successor ML project, but it looks like even the die hard fans have drifted away https://smlfamily.github.io/ https://smlfamily.github.io/
bzxcvbn 4y ago
I'm not really convinced by the author's first example. While an element of type bool is an instance of type a, an element of type bool -> bool is not an instance of type a -> a. The issue is precisely an issue of variance, which is mentioned in reference to Scala, but somehow it's glossed over. The type a -> a is covariant in its second argument, but contravariant in its first argument. As a result, you cannot "specialize" it to bool -> bool, because specialization is really another name for covariance. Another name for contravariance is "generalization". If you ask for something of type "bool -> b", and someone provides you with some function f of type "a -> b", then you're happy. The map f is indeed an instance of "bool -> b": it can eat anything, so it can eat booleans. But with type a -> a, you cannot do what I just did: type "a" is already the most general one, and you cannot do better. If SML accepted something of type "bool -> bool" for an instance of type "a -> a", then it was a fundamental error. But this doesn't mean that the whole thing should have been thrown out and replaced with monads. In fact, I don't really get how monads have anything to do with the problem at hand. If Haskell can prevent the following code, then I don't see why SML couldn't have prevented the authors' code: do m <- STRef id m <- not m 42
- lexi-lambda 4y ago
  > While an element of type bool is an instance of type a, an element of type bool -> bool is not an instance of type a -> a. This sentence is true if you interpret `a -> a` to mean `∀ a. a -> a`, i.e. a universally-quantified type. But it is false if you interpret it to mean `α -> α` where α is an unsolved metavariable, for the reasons I describe in this comment: https://news.ycombinator.com/item?id=31238081 https://news.ycombinator.com/item?id=31238081 > The issue is precisely an issue of variance, which is mentioned in reference to Scala, but somehow it's glossed over. Not so! The issue is the incompatibility of mutable references and value polymorphism, which variance alone does not solve. For example, in Scala, you cannot write something like val xs[A]: ArrayBuffer[A] = ArrayBuffer[A]() because if you could do that, then you could write val bools: ArrayBuffer[Bool] = xs[Bool] bools += true val ints: ArrayBuffer[Int] = xs[Int] ints.last and all hell breaks loose. Note that variance does not in any way save you here—the type variable `A` is always covariant, so this code is variance-correct. Scala prevents this by only permitting polymorphic functions, so you would have to write the above example like this, instead: def xs[A](): ArrayBuffer[A] = ArrayBuffer[A]() Now everything is okay, because if you call this function twice, you get two different buffers. This is precisely what the ML value restriction enforces. > Another name for contravariance is "generalization". Maybe this is true in some sense of the word, though I’ll admit I’ve never seen “generalization” used in this way. But in Hindley-Milner type systems, “generalization” is a term of art that means something fairly specific, namely the implicit introduction of universal quantification, so using it in this context to mean something else may be a little confusing. > If SML accepted something of type "bool -> bool" for an instance of type "a -> a", then it was a fundamental error. But this doesn't mean that the whole thing should have been thrown out and replaced with monads. In fact, I don't really get how monads have anything to do with the problem at hand. I sort of agree—introducing monadic structure has essentially nothing fundamental to do with this particular problem. However, it is incidentally true that the monadic encoding of mutable state in Haskell sidesteps the problem. To see why, suppose we translate the Scala example from above into Haskell. Suppose we have a constructor like this: newArrayBuffer :: forall a. IO (ArrayBuffer a) Note that this is itself a polymorphic value—it isn’t a function! But since it’s wrapped in `IO`, it isn’t itself a polymorphic buffer, just a recipe to create one. If we wanted to trigger the bad behavior, we’d need to be able to create a definition with a type like this: xs :: forall a. ArrayBuffer a But that isn’t possible to obtain from `newArrayBuffer`, even though Haskell allows polymorphic values. That’s because, in the type of `newArrayBuffer`, the `forall` is outside the `IO` constructor, so in order to actually use it in a computation using `>>=`, we have to instantiate `a` to some concrete type. In other words, `IO` plays precisely the same role here that a nullary function does in Scala: it ensures each instantiation is generative, i.e. it returns a distinct buffer. So Haskell doesn’t need a value restriction because, in a sense, everything impure is subject to a value restriction, with `IO` playing the role of the nullary function type, and that includes anything that contains mutable state. But since Haskell relies on this property of `IO` to preserve safety `unsafePerformIO` can subvert the type system. We can write xs :: forall a. ArrayBuffer a xs = unsafePerformIO (newArrayBuffer @a) and we get the potential for badness again, just like in the Scala example. This is considered acceptable because `unsafePerformIO` is, well, unsafe.
bobbylarrybobby 4y ago
> In Structure and Interpretation of Computer Programs, Abelson and Sussman describe an arithmetic system in which the arithmetic types form an explicit lattice. Every type comes with a “promotion” function to promote it to a type higher up in the lattice. When values of different types are added, each value is promoted, perhaps repeatedly, until the two values are the same type, which is the lattice join of the two original types. I've never used anything like this and don't know how well it works in practice, but it seems like a plausible approach, one which works the way we usually think about numbers, and understands that it can add a float to a Gaussian integer by construing both of them as complex numbers. Julia uses this in pretty much all of its math functions and probably elsewhere as well, and it works unbelievably well. The type promotion system makes math Just Work, even (and especially) in the face of different-sized numbers. The result is that 99.9% of the time you simply don't have to think about the types of your numbers. Here are some examples from the docs: julia> promote_type(Int64, Float64) Float64 julia> promote_type(Int32, Int64) Int64 julia> promote_type(Float32, BigInt) BigFloat julia> promote_type(Int16, Float16) Float16 julia> promote_type(Int64, Float16) Float16 julia> promote_type(Int8, UInt16) UInt16 And not only are types promoted, but in well-typed Julia code, the deduction of promotion types happens at compile time instead of runtime, so there is almost no performance cost to this either.
- HalcyonCowboy 4y ago
  Wouldn’t that last example be incorrect mathematically? For example, if the Int8 was -10 and the UInt16 was 10, what would that casting do? Would a better promotion be Int32 for both? Just curious, Julia is a language I’ve been very interested in using for a long time, just haven’t had the opportunity to sit down and learn yet.
  - adgjlsfhk1 4y ago
    Yeah, it's a little iffy. Finding a sensible set of promotion rules is hard. I don't know the reason (this was decided before I was involved), but if I had to guess, it would be because unsigned types are much less common, so if the user has them, they probably want to keep them for a reason.
adultSwim 4y ago
What was wrong with SML? It didn't have a big company like Sun pushing it
wrp 4y ago
How about OCaml? I studied it alongside SML and liked it a bit better. Whenever something in SML struck me as a poor design choice, I looked over and saw that Caml had done something about it. (I felt the "O" was a completely unnecessary addition.)
GnarfGnarf 4y ago
"SML" = Standard Meta Language. Talk about betriebsblind.
kragen 4y ago
I think that in some sense the correct solution to the reference type problem is the Scala solution, which depends on subtyping. This is pretty tricky to reason through, and adding subtyping makes type inference a lot more difficult, so it's hardly surprising that SML avoided this, but it provides a much more satisfying solution. (OCaml later embraced subtyping, but in the particular case of mutable references, it instead adopted the same value-restriction approach as SML.) Here's the way I understand it; be warned that I'm just starting to understand this stuff, so I might have got something wrong. I'd welcome corrections. S is a subtype of T (S <: T) iff you can use an object of type S wherever you need an object of type T. This gives us a partial order on types, in the sense that ∀T: T <: T ∀S:∀T: S <: T ∧ T <: S ⇒ S = T ∀S:∀T:∀U: S <: T ∧ T <: U ⇒ S <: U which all follow from the above informal definition. Sometimes we make it a lattice, for example by adding a ⊤ type ("top") that everything is a subtype of and a ⊥ type ("bottom") that is a subtype of everything. In general in the presence of subtyping we can only infer type bounds on most things, not exact types. For example, consider that {3} <: ℤ <: ℝ <: ℂ; if we see a function being applied to the value 3, we can infer that it must be at least applicable to {3}, but a function that is applicable to ℤ or ℝ would also work. Given this informal definition, surprisingly, α → α (the type of the identity function) is a "subtype" of bool → bool, not vice versa. That is, α → α <: bool → bool. Whenever we want a function of type bool → bool, we can use a function of type α → α, but not vice versa. α → α is a weird type because it includes an implicit universal quantifier: ∀α: α → α. As it turns out, the judgment above that α → α <: bool → bool is not because α <: bool or bool <: α. It's because bool → bool is what you get when you instantiate the quantifier with a particular value, α = bool. There's also a function-specific rule for subtyping, and it's a real mindbender: B → C <: A → D if A <: B and C <: D. We say functions' argument types are contravariant and their results are covariant. Considering the A <: B case, if we need a function from integers to booleans, we can use a function from real numbers to booleans—we just won't happen to invoke it with any non-integer real numbers, but it will still work, assuming there aren't incompatible binary representations at play (as in the case of the OCaml +. and + operators MJD mentions.). Considering the C <: D case, we can also use a function from integers to true: it will never return a value we cannot use as a boolean. We can decompose the operation of taking a reference to x, ref x, into a step of creating a reference r and then applying the reseating operation r := x to it. This operation is valid iff the assignee is of a subtype of the referent type; that is, (r : T ref) := (x : S) is valid iff S <: T. That's because later when we read r we will be using its value as a T, so any subtype of T is fine. So for ref (fn x ⇒ x), we have that S = α → α, so we can derive the type bound that T must be some supertype of α → α. As mentioned above, this includes bool → bool, but it also includes ℤ → ℤ, (ℤ × ℂ) → (ℤ × ℂ), and the polymorphic type α → α itself. So reseating a reference is contravariant: we can write a value we know is an integer or anything more specific (a subtype such as a positive integer) into a reference we know to hold an integer or anything more general (a supertype such as a real number). The dereferencing operation !r turns out to instead be covariant: !(r: S ref): T is valid iff S <: T. That is, we're going to use the result as type T, so the reference can hold any subtype of T. So if we see ((!m) 23) we have (!m) : {23} → ⊤, from which we can deduce a type bound (m : U) where U <: ({23} → ⊤) ref. That is, the type of the referent of m is a subtype of a "function that can take 23 and return something". For example, (ℤ → string) <: ({23} → ⊤), because {23} <: ℤ and functions are contravariant in their arguments, and string <: ⊤ (because every type is a subtype of ⊤), so if m has type (ℤ → string) ref, we're good. (bool → bool) ref would not work, because (bool → bool) ref is not a subtype of ({23} → ⊤) ref, because bool → bool is not a subtype of {23} → ⊤, because, even though bool <: ⊤, {23} is not a subtype of bool. How does this resolve the problem? If m is of type (α → α) ref, ((!m) 23) would work; for example, if m happens to be a reference to the identity function, it evaluates to 23. (In many languages that's the only function of type α → α, in the interests of making the Curry–Howard correspondence meaningful.) But if we've previously seen (m := not), we have an incompatible type bound: (not : bool → bool), so we know that m is of type (bool → bool) ref or a ref to some supertype of bool → bool, U ref where bool → bool <: U. And, as I said above, it is not the case that bool → bool <: α → α; it's the other way around. This seems to give us a nice, clean solution to the problem of types for references. Aside from being confusing as hell, the cost is that instead of inferring a type for every expression we can now only infer an infinite set of possibilities for its type. This sounds ridiculous but it is precisely what OCaml does for polymorphic variants and objects (though not mutable refs; details are in https://v2.ocaml.org/manual/polymorphism.html https://v2.ocaml.org/manual/polymorphism.html). With polymorphic variants: # let f a = match a with 1 -> `P (3, 4) | _ -> `Q (5) ;; val f : int -> [> `P of int * int | `Q of int ] = <fun> # let g b = match b with `P (c, d) -> c + d | `Q (c) -> c ;; val g : [< `P of int * int | `Q of int ] -> int = <fun> The "<" here means that what's being given is an "upper bound": it's perfectly acceptable to apply g to an expression whose type is a subtype of the type given, like this: # `Q 2 ;; - : [> `Q of int ] = `Q 2 # g (`Q 2) ;; - : int = 2 But the ">" on f's return type is a "lower bound": you can only use f in a context where its return type is a subtype of the expected type. Including the same type, so we can pass it to g: # g (f 1);; - : int = 7 # g (f 2);; - : int = 5 Similarly we can write a function that calls a couple of methods on its arguments: # let mf o = (o#foo ; o#bar + 1) ;; val mf : < bar : int; foo : 'a; .. > -> int = <fun> Here OCaml infers that the object needs to have a method "bar" returning int and a method "foo" of some type, but the .. makes this an upper-bound object type: it's okay for the object to be of some subtype that has more methods. And similarly if you construct an object with some methods, it can be used in a context that requires some supertype that doesn't have all of them. (There's a very close analogy between an object with a certain set of methods and a function that can be applied to terms with a certain finite set of polymorphic variant tags.) The subtyping approach would seem to provide a logical solution to the problem of mutability, but it isn't the approach OCaml took, for reasons I don't understand. It's confusing and difficult to understand, but less so than OCaml's current set of rules. I suspect the answer is that OCaml had to be backward-compatible with earlier versions of Caml before subtyping was added, but possibly it's instead to keep the type inference problem decidable or something.
lexi-lambda 4y ago
I don’t think the complaints about evaluation order in this blog post really make sense. The evaluation order of `map` in SML is no more mysterious than the evaluation order of `mapM` in Haskell. The use of explicit monadic sequencing has its advantages (as well as nontrivial disadvantages), but this is not one of them. This is particularly true if `mapM` is written using applicative functors, as the definition mapM :: Monad m => (a -> m b) -> [a] -> m [b] mapM f [] = return [] mapM f (x:xs) = (:) <$> f x <*> mapM f xs is virtually identical in structure to the SML definition fun map f [] = [] | map f (x :: xs) = op:: (f x) (map f xs) aside from the “plumbing” of `return`, `<$>`, and `<*>`. Indeed, the whole motivation of applicative functors, as well as the source of their name, was a desire to write code in a form closer to an applicative style, which is to say non-monadic, direct-style code like the SML example. The blog post says > Does it print the values in forward or reverse order? One could implement it either way. but obviously this is also true of `mapM`. That would just be a different function. Monadic sequencing does not help with this at all. Furthermore, the author mentions algebraic effect systems. It isn’t clear to me from the wording if the intent is to offer them as a solution for the shortcomings of monadic encodings or as a nicer way to pin down evaluation order, but the latter is certainly not true—the two are entirely orthogonal. Algebraic effect systems depend on the evaluation order being well-defined by other means to work in the first place. In fact, one could argue that the entire point of algebraic effect systems is to allow the composition of different effects while respecting an underlying notion of evaluation order.

What was wrong is not having a killer application or an industry giant pushing it. Grammar and language semantic are details regarding language adoption.

eatonphil 4y ago
Yup, adoption has nothing to do with being a sensible language. More often it seems to be completely inversely related.
- exikyut 4y ago
  What are some sensible (coherent, load-bearing, force-multiplying etc) tools that have terrible adoption? Unreasonably open-ended question (suppose the scope is ML, or perhaps FP in general, or maybe even wider) - but I'm very curious.
  - youerbt 4y ago
    TLA+ or Nix comes to mind. By some notion of terrible I guess.
  - eatonphil 4y ago
    Google "worse is better". :)
  - pharmakom 4y ago
    I would say F#. It has most things you could want: - Proper functional programming support - Fast enough runtime - Cross-platform and open-source - Mainstream ecosystem - Large corporate backer - Compile to JS - Commercial and open-source tooling options … and yet C# is far more popular. This is because language adoption is driven by existing user base and other network effects NOT the quality of the language itself.
  - macintux 4y ago
    Erlang is underutilized at least in part due to its odd syntax, despite being a powerful tool. Elixir is helping address that, although I much prefer Erlang’s syntax.

throwamon 4y ago

A bit off-topic, but could someone ELI5 what a lattice is in this context?

chombier 4y ago
I think this refers to a system of types in which for any two types there is also an union type and an intersection type in the lattice.
mjd 4y ago
If you have two types, there should be a single type that "joins" them, in the sense that you can understand both of the original types as somehow being special cases of the join type. A join is not necessarily a union, since the representations of the three types might be completely different, and also because the third type might contain many values that don't correspond to anything in the two original types. (It might be much bigger than the union.) Mathematical lattices must also have "meets", which are like joins except down instead of up. I'm not sure that meets are as important as joins in this context.
layer8 4y ago
It refers to https://en.m.wikipedia.org/wiki/Lattice_(order) https://en.m.wikipedia.org/wiki/Lattice_(order), with the elements of the lattice being the arithmetic types and the order relation being the subtyping relation here. Given any two types in the lattice, the lattice property then guarantees that there exists a unique common (least) supertype (aka upper bound, supremum) of the two types. Which means you can apply the binary operation (e.g. addition) as defined for that common supertype.

chombier 4y ago

> Scala has a very different solution to this problem, called covariant and contravariant traits. I thought Scala had an even stricter value restriction than ML, where only function/methods may get a polymorphic type?

samth 4y ago
Yes, that statement is very confused. Scala doesn't do generalization, or polymorphic values, and thus the problem doesn't occur at all.

porcoda 4y ago

I still actively use SML - mlton or smlnj usually, polyml too. I’m aware of the issues raised in this post but haven’t ever found them to be a source of much headache. To be honest, the biggest headache is moving between compilers and their different build processes. Other than that, the fact that the language isn’t really changing is a big attraction for me. CakeML is also a very cool project in SML land.

Karrot_Kream 4y ago
I am curious what you use SML for. Any examples? Just interested in seeing what you can do in SML.
- porcoda 4y ago
  Mostly programming languages related: code analysis, compilers, code generators, and formal verification tools. Outside PL work, I’ve used it to build some modeling and simulation tools. I also use it for misc. little tools that I need every so often where I want the type system to help me out. For a brief few years (‘09-‘15) Haskell played this role for me but I went back to SML after getting frustrated with various parts of that ecosystem.
  - Karrot_Kream 4y ago
    Oh modeling and simulation is an interesting idea, that sounds like a perfect thing to play around with SML for. Thanks!
mbarbar 4y ago
>CakeML is also a very cool project in SML land. I've been very interested in CakeML lately, do you use it for anything?

eatonphil 4y ago

I mentioned to Mark when I saw this, and he noted it in the addendum at the end, that calling Standard ML dead is a bit too much. I've written recently [0] about how active it surprisingly is. I also disagree that its failure to "succeed" has anything to do with syntax or semantics and solely that it doesn't have a Jane Street or any company publicly behind it. [0] https://notes.eatonphil.com/standard-ml-in-2020.html https://notes.eatonphil.com/standard-ml-in-2020.html

porcoda 4y ago
I don’t think it succeeded or failed. Languages don’t need to be wildly popular in industry to be valuable. I personally like that industry ignores SML. Even for Ocaml I don’t use the Jane street core: I just use the stock language since it’s small and stable. I like that Jane street helps improve the core compiler though.
- pjmlp 4y ago
  Haskell's motto is "avoid success at all costs", after all.
mjd 4y ago
I would like to point out that the article does not use the words “succeed” or “fail”, and makes no claim about whether SML “succeeded” or “failed”. Indeed I don't think that is a useful question to ask. My article was trying to address a much less nebulous issue: what problems did I personally see with SML in the mid 1990s that let me to abandon it at that time.
- eatonphil 4y ago
  Sorry, I didn't mean to put words in your mouth. I may just have gotten the wrong impression of your intent. Any criticism of any language is valid and good to have!
gkuan 4y ago
I do wonder if differences in language governance models impact uptake. Being completely biased (having worked on the SML/NJ compiler a long while ago), I very badly want to see more adoption. There is definitely continuing activity with new (IFL award winning) LLVM backend work [1] and Manticore. [1] http://cs.uchicago.edu/news/smlnj-overhaul/ http://cs.uchicago.edu/news/smlnj-overhaul/

Athas 4y ago

> Haskell's primary solution to this is to burn it all to the ground. Mutation doesn't cause any type problems because there isn't any. This is true, but I think it is also misleading. Haskell has the same problem if you use unsafePerformIO to create a polymorphic IORef at top level. You can then use this IORef to subvert the type system. I think this is something many Haskell programmers are not fully aware of: unsafePerformIO doesn't just break referential transparency; it can also fundamentally break memory safety. Now, you may say that unsafePerformIO is obviously unsafe (it's in the name!) and should never be used. But if you look at many foundational Haskell libraries, you will find that they use unsafePerformIO or similar functions internally, usually for performance reasons. What are the rules that govern safe usage of unsafePerformIO? As far as I can determine, these rules are basically just GHC implementation details, and people often get them wrong. And if you break these rules, you don't just get a function that doesn't do what you expected - you may have subverted memory safety entirely. I think this is an interesting conundrum. Haskell makes much stronger promises than SML, but if you break the rules, all bets are completely off.

jasonhansel 4y ago

IMHO Haskell's lazy evaluation has some significant disadvantages compared to SML's strict evaluation. In particular, lazy evaluation makes it difficult to find the performance bottlenecks in a particular piece of code or to determine the time complexity of an algorithm just by reading it. Furthermore, subtle changes in how a function is written (for instance, making a multiplication function not evaluate the right operand if the left operand is zero) can cause wildly unexpected performance changes in that function's callers. In effect, the performance of a function is no longer just determined by that function's structure and by the function calls it contains; performance of one function now depends heavily on the implementation details of others and the context in which that function is used. Granted, any optimizing compiler can have this effect, but it's rarely noticeable in strictly-evaluated languages, where at least to some extent the order of evaluation must correspond to the structure of the code.

zozbot234 4y ago
It would be nice to have a language that could treat both strict and lazy evaluation as equally first-class, as opposed to having one be the default (whether "strict" as in ML or "lazy" as in Haskell) and the other only being expressed by syntactical kludges. This may well be possible by relying on logically-inspired features like polarity and focusing, and endowing data types with strict or lazy "natural" polarities.
- eatonphil 4y ago
  Any strict language can implement laziness. The inverse may(?) not be possible.
  - ravi-delia 4y ago
    It's the opposite, no? Basically every lazy language has some way to force evaluation, but in most strict languages laziness is never fully supported. Closest I can think of is a Scheme with continuations, but even then it takes some extra work. I know in CL even primitive laziness takes a lot of work and a code-walker, and whatever it's other flaws Common Lisp is at least adaptable.

eatonphil 4y ago

For folks interested in learning Standard ML, check out /r/sml [0] and the sticky post [1] with a getting started guide. [0] http://reddit.com/r/sml http://reddit.com/r/sml [1] https://www.reddit.com/r/sml/comments/qyy2gs/getting_started_with_standard_ml/ https://www.reddit.com/r/sml/comments/qyy2gs/getting_started...

shpongled 4y ago

SML is one of my favorite languages (I've been (very) slowly writing a compiler & language server for it). Sure, it has some warts/differences compared to newer languages - we have moved towards traits/typeclasses/etc, and I wish I could just write #[derive(Debug) - but I feel that SML fits in a very unique spot for programming languages. It's extremely simple, yet still powerful and expressive. I hope we will see continued work on SML/Successor ML descendants (like 1ML, etc), because I think there's still potential there I think some updated language tooling would dramatically help.

jaytaylor 4y ago
Is your development progress taking place in the open? (e.g. GitHub or somewhere similar) It sounds like a cool project and I'd love to see it! And even have the option to open a PR and help ;)
- eatonphil 4y ago
  Yes, please share or open-source it even if it's not done!
  - shpongled 4y ago
    You have already linked to it :)
- shpongled 4y ago
  I have the compiler on GitHub [1] - I just started working on it again after a 2-year hiatus (to finish my PhD). As for language-server, I'm currently sketching out some plans to use SMLnj's "Visible Compiler" feature, since that seems the easiest path forward. I have a half-baked language-server based on MLton's def-use output, but it's too unstable to share. I am planning to make some progress on the language-server in the next couple weeks. [1] You'll notice it's just a fragment of the language for now, and only half-implemented. https://github.com/SomewhatML/sml-compiler https://github.com/SomewhatML/sml-compiler and https://github.com/SomewhatML/sml-analyzer https://github.com/SomewhatML/sml-analyzer (again for a fragment of SML)

tialaramex 4y ago

SML was the First Language used for the Computer Science degree I took. I felt at that time, and continue to feel years later (that degree course now teaches Java as First Language) that this was a good decision despite the fact that most graduates don't end up using SML to write anything. In the course of my education I experienced some things which I'm convinced are a bad idea even though they worked out OK for me such as selective education (whole schools only for "talented" children) and single sex secondary education, but SML as First Language is not one of those things. It worked well for me and I'm convinced it's a good idea even though I would not advocate writing new real world projects in SML unless you've got some very particular reason.

ravi-delia 4y ago
I feel like there should be some expected order. Like BASIC->functional->scheme or something. Maybe switch them around, or throw in Python. There are a bunch of hurdles for new programmers to jump over, and it seems like maybe the best way to get them over them is with a different language for each. When my roommate took his intro CS course in Python he was mystified by type errors since they're often somewhat hidden. In Java the next semester the boilerplate made the whole program feel less understandable, but a semester or two later and it could have taught valuable lessons.
wink 4y ago
Interestingly we used OCaml in the first semester (by the professor's choice) in late 2003, and I hated it and failed the course. A year later I retook the course and as it was some other professor's turn it was SML, which I kinda liked. I did revisit OCaml more than 10 years later and actually enjoyed it, so maybe it was a bit of "wrong place, wrong time" but as I heard from some users it should have evolved quite a bit in those 10 years. (I am 95% sure it was not functional programming per se, but I never figured out what exactly was the culprit, I guess a dose of "I know how to code" was involved).

fanf2 4y ago

There was a history of Standard ML published as part of HOPL4 a couple of years ago - https://dl.acm.org/doi/10.1145/3386336 https://dl.acm.org/doi/10.1145/3386336 I was particularly interested by the more recent history, after SML '97, where there was plenty of interest in improving the language and its library, but Milner insisted that there would be no further changes, and the Definition was non-free so the others could not build on it. (It has since become Free though its source code was lost.) Despite that there is/was an SML Basis Library project, and a Successor ML project, but it looks like even the die hard fans have drifted away https://smlfamily.github.io/ https://smlfamily.github.io/

bzxcvbn 4y ago

I'm not really convinced by the author's first example. While an element of type bool is an instance of type a, an element of type bool -> bool is not an instance of type a -> a. The issue is precisely an issue of variance, which is mentioned in reference to Scala, but somehow it's glossed over. The type a -> a is covariant in its second argument, but contravariant in its first argument. As a result, you cannot "specialize" it to bool -> bool, because specialization is really another name for covariance. Another name for contravariance is "generalization". If you ask for something of type "bool -> b", and someone provides you with some function f of type "a -> b", then you're happy. The map f is indeed an instance of "bool -> b": it can eat anything, so it can eat booleans. But with type a -> a, you cannot do what I just did: type "a" is already the most general one, and you cannot do better. If SML accepted something of type "bool -> bool" for an instance of type "a -> a", then it was a fundamental error. But this doesn't mean that the whole thing should have been thrown out and replaced with monads. In fact, I don't really get how monads have anything to do with the problem at hand. If Haskell can prevent the following code, then I don't see why SML couldn't have prevented the authors' code: do m <- STRef id m <- not m 42

lexi-lambda 4y ago
> While an element of type bool is an instance of type a, an element of type bool -> bool is not an instance of type a -> a. This sentence is true if you interpret `a -> a` to mean `∀ a. a -> a`, i.e. a universally-quantified type. But it is false if you interpret it to mean `α -> α` where α is an unsolved metavariable, for the reasons I describe in this comment: https://news.ycombinator.com/item?id=31238081 https://news.ycombinator.com/item?id=31238081 > The issue is precisely an issue of variance, which is mentioned in reference to Scala, but somehow it's glossed over. Not so! The issue is the incompatibility of mutable references and value polymorphism, which variance alone does not solve. For example, in Scala, you cannot write something like val xs[A]: ArrayBuffer[A] = ArrayBuffer[A]() because if you could do that, then you could write val bools: ArrayBuffer[Bool] = xs[Bool] bools += true val ints: ArrayBuffer[Int] = xs[Int] ints.last and all hell breaks loose. Note that variance does not in any way save you here—the type variable `A` is always covariant, so this code is variance-correct. Scala prevents this by only permitting polymorphic functions, so you would have to write the above example like this, instead: def xs[A](): ArrayBuffer[A] = ArrayBuffer[A]() Now everything is okay, because if you call this function twice, you get two different buffers. This is precisely what the ML value restriction enforces. > Another name for contravariance is "generalization". Maybe this is true in some sense of the word, though I’ll admit I’ve never seen “generalization” used in this way. But in Hindley-Milner type systems, “generalization” is a term of art that means something fairly specific, namely the implicit introduction of universal quantification, so using it in this context to mean something else may be a little confusing. > If SML accepted something of type "bool -> bool" for an instance of type "a -> a", then it was a fundamental error. But this doesn't mean that the whole thing should have been thrown out and replaced with monads. In fact, I don't really get how monads have anything to do with the problem at hand. I sort of agree—introducing monadic structure has essentially nothing fundamental to do with this particular problem. However, it is incidentally true that the monadic encoding of mutable state in Haskell sidesteps the problem. To see why, suppose we translate the Scala example from above into Haskell. Suppose we have a constructor like this: newArrayBuffer :: forall a. IO (ArrayBuffer a) Note that this is itself a polymorphic value—it isn’t a function! But since it’s wrapped in `IO`, it isn’t itself a polymorphic buffer, just a recipe to create one. If we wanted to trigger the bad behavior, we’d need to be able to create a definition with a type like this: xs :: forall a. ArrayBuffer a But that isn’t possible to obtain from `newArrayBuffer`, even though Haskell allows polymorphic values. That’s because, in the type of `newArrayBuffer`, the `forall` is outside the `IO` constructor, so in order to actually use it in a computation using `>>=`, we have to instantiate `a` to some concrete type. In other words, `IO` plays precisely the same role here that a nullary function does in Scala: it ensures each instantiation is generative, i.e. it returns a distinct buffer. So Haskell doesn’t need a value restriction because, in a sense, everything impure is subject to a value restriction, with `IO` playing the role of the nullary function type, and that includes anything that contains mutable state. But since Haskell relies on this property of `IO` to preserve safety `unsafePerformIO` can subvert the type system. We can write xs :: forall a. ArrayBuffer a xs = unsafePerformIO (newArrayBuffer @a) and we get the potential for badness again, just like in the Scala example. This is considered acceptable because `unsafePerformIO` is, well, unsafe.

bobbylarrybobby 4y ago

> In Structure and Interpretation of Computer Programs, Abelson and Sussman describe an arithmetic system in which the arithmetic types form an explicit lattice. Every type comes with a “promotion” function to promote it to a type higher up in the lattice. When values of different types are added, each value is promoted, perhaps repeatedly, until the two values are the same type, which is the lattice join of the two original types. I've never used anything like this and don't know how well it works in practice, but it seems like a plausible approach, one which works the way we usually think about numbers, and understands that it can add a float to a Gaussian integer by construing both of them as complex numbers. Julia uses this in pretty much all of its math functions and probably elsewhere as well, and it works unbelievably well. The type promotion system makes math Just Work, even (and especially) in the face of different-sized numbers. The result is that 99.9% of the time you simply don't have to think about the types of your numbers. Here are some examples from the docs: julia> promote_type(Int64, Float64) Float64 julia> promote_type(Int32, Int64) Int64 julia> promote_type(Float32, BigInt) BigFloat julia> promote_type(Int16, Float16) Float16 julia> promote_type(Int64, Float16) Float16 julia> promote_type(Int8, UInt16) UInt16 And not only are types promoted, but in well-typed Julia code, the deduction of promotion types happens at compile time instead of runtime, so there is almost no performance cost to this either.

HalcyonCowboy 4y ago
Wouldn’t that last example be incorrect mathematically? For example, if the Int8 was -10 and the UInt16 was 10, what would that casting do? Would a better promotion be Int32 for both? Just curious, Julia is a language I’ve been very interested in using for a long time, just haven’t had the opportunity to sit down and learn yet.
- adgjlsfhk1 4y ago
  Yeah, it's a little iffy. Finding a sensible set of promotion rules is hard. I don't know the reason (this was decided before I was involved), but if I had to guess, it would be because unsigned types are much less common, so if the user has them, they probably want to keep them for a reason.

adultSwim 4y ago

What was wrong with SML? It didn't have a big company like Sun pushing it

wrp 4y ago

How about OCaml? I studied it alongside SML and liked it a bit better. Whenever something in SML struck me as a poor design choice, I looked over and saw that Caml had done something about it. (I felt the "O" was a completely unnecessary addition.)

GnarfGnarf 4y ago

"SML" = Standard Meta Language. Talk about betriebsblind.

kragen 4y ago

I think that in some sense the correct solution to the reference type problem is the Scala solution, which depends on subtyping. This is pretty tricky to reason through, and adding subtyping makes type inference a lot more difficult, so it's hardly surprising that SML avoided this, but it provides a much more satisfying solution. (OCaml later embraced subtyping, but in the particular case of mutable references, it instead adopted the same value-restriction approach as SML.) Here's the way I understand it; be warned that I'm just starting to understand this stuff, so I might have got something wrong. I'd welcome corrections. S is a subtype of T (S <: T) iff you can use an object of type S wherever you need an object of type T. This gives us a partial order on types, in the sense that ∀T: T <: T ∀S:∀T: S <: T ∧ T <: S ⇒ S = T ∀S:∀T:∀U: S <: T ∧ T <: U ⇒ S <: U which all follow from the above informal definition. Sometimes we make it a lattice, for example by adding a ⊤ type ("top") that everything is a subtype of and a ⊥ type ("bottom") that is a subtype of everything. In general in the presence of subtyping we can only infer type bounds on most things, not exact types. For example, consider that {3} <: ℤ <: ℝ <: ℂ; if we see a function being applied to the value 3, we can infer that it must be at least applicable to {3}, but a function that is applicable to ℤ or ℝ would also work. Given this informal definition, surprisingly, α → α (the type of the identity function) is a "subtype" of bool → bool, not vice versa. That is, α → α <: bool → bool. Whenever we want a function of type bool → bool, we can use a function of type α → α, but not vice versa. α → α is a weird type because it includes an implicit universal quantifier: ∀α: α → α. As it turns out, the judgment above that α → α <: bool → bool is not because α <: bool or bool <: α. It's because bool → bool is what you get when you instantiate the quantifier with a particular value, α = bool. There's also a function-specific rule for subtyping, and it's a real mindbender: B → C <: A → D if A <: B and C <: D. We say functions' argument types are contravariant and their results are covariant. Considering the A <: B case, if we need a function from integers to booleans, we can use a function from real numbers to booleans—we just won't happen to invoke it with any non-integer real numbers, but it will still work, assuming there aren't incompatible binary representations at play (as in the case of the OCaml +. and + operators MJD mentions.). Considering the C <: D case, we can also use a function from integers to true: it will never return a value we cannot use as a boolean. We can decompose the operation of taking a reference to x, ref x, into a step of creating a reference r and then applying the reseating operation r := x to it. This operation is valid iff the assignee is of a subtype of the referent type; that is, (r : T ref) := (x : S) is valid iff S <: T. That's because later when we read r we will be using its value as a T, so any subtype of T is fine. So for ref (fn x ⇒ x), we have that S = α → α, so we can derive the type bound that T must be some supertype of α → α. As mentioned above, this includes bool → bool, but it also includes ℤ → ℤ, (ℤ × ℂ) → (ℤ × ℂ), and the polymorphic type α → α itself. So reseating a reference is contravariant: we can write a value we know is an integer or anything more specific (a subtype such as a positive integer) into a reference we know to hold an integer or anything more general (a supertype such as a real number). The dereferencing operation !r turns out to instead be covariant: !(r: S ref): T is valid iff S <: T. That is, we're going to use the result as type T, so the reference can hold any subtype of T. So if we see ((!m) 23) we have (!m) : {23} → ⊤, from which we can deduce a type bound (m : U) where U <: ({23} → ⊤) ref. That is, the type of the referent of m is a subtype of a "function that can take 23 and return something". For example, (ℤ → string) <: ({23} → ⊤), because {23} <: ℤ and functions are contravariant in their arguments, and string <: ⊤ (because every type is a subtype of ⊤), so if m has type (ℤ → string) ref, we're good. (bool → bool) ref would not work, because (bool → bool) ref is not a subtype of ({23} → ⊤) ref, because bool → bool is not a subtype of {23} → ⊤, because, even though bool <: ⊤, {23} is not a subtype of bool. How does this resolve the problem? If m is of type (α → α) ref, ((!m) 23) would work; for example, if m happens to be a reference to the identity function, it evaluates to 23. (In many languages that's the only function of type α → α, in the interests of making the Curry–Howard correspondence meaningful.) But if we've previously seen (m := not), we have an incompatible type bound: (not : bool → bool), so we know that m is of type (bool → bool) ref or a ref to some supertype of bool → bool, U ref where bool → bool <: U. And, as I said above, it is not the case that bool → bool <: α → α; it's the other way around. This seems to give us a nice, clean solution to the problem of types for references. Aside from being confusing as hell, the cost is that instead of inferring a type for every expression we can now only infer an infinite set of possibilities for its type. This sounds ridiculous but it is precisely what OCaml does for polymorphic variants and objects (though not mutable refs; details are in https://v2.ocaml.org/manual/polymorphism.html https://v2.ocaml.org/manual/polymorphism.html). With polymorphic variants: # let f a = match a with 1 -> `P (3, 4) | _ -> `Q (5) ;; val f : int -> [> `P of int * int | `Q of int ] = <fun> # let g b = match b with `P (c, d) -> c + d | `Q (c) -> c ;; val g : [< `P of int * int | `Q of int ] -> int = <fun> The "<" here means that what's being given is an "upper bound": it's perfectly acceptable to apply g to an expression whose type is a subtype of the type given, like this: # `Q 2 ;; - : [> `Q of int ] = `Q 2 # g (`Q 2) ;; - : int = 2 But the ">" on f's return type is a "lower bound": you can only use f in a context where its return type is a subtype of the expected type. Including the same type, so we can pass it to g: # g (f 1);; - : int = 7 # g (f 2);; - : int = 5 Similarly we can write a function that calls a couple of methods on its arguments: # let mf o = (o#foo ; o#bar + 1) ;; val mf : < bar : int; foo : 'a; .. > -> int = <fun> Here OCaml infers that the object needs to have a method "bar" returning int and a method "foo" of some type, but the .. makes this an upper-bound object type: it's okay for the object to be of some subtype that has more methods. And similarly if you construct an object with some methods, it can be used in a context that requires some supertype that doesn't have all of them. (There's a very close analogy between an object with a certain set of methods and a function that can be applied to terms with a certain finite set of polymorphic variant tags.) The subtyping approach would seem to provide a logical solution to the problem of mutability, but it isn't the approach OCaml took, for reasons I don't understand. It's confusing and difficult to understand, but less so than OCaml's current set of rules. I suspect the answer is that OCaml had to be backward-compatible with earlier versions of Caml before subtyping was added, but possibly it's instead to keep the type inference problem decidable or something.

lexi-lambda 4y ago

I don’t think the complaints about evaluation order in this blog post really make sense. The evaluation order of `map` in SML is no more mysterious than the evaluation order of `mapM` in Haskell. The use of explicit monadic sequencing has its advantages (as well as nontrivial disadvantages), but this is not one of them. This is particularly true if `mapM` is written using applicative functors, as the definition mapM :: Monad m => (a -> m b) -> [a] -> m [b] mapM f [] = return [] mapM f (x:xs) = (:) <$> f x <*> mapM f xs is virtually identical in structure to the SML definition fun map f [] = [] | map f (x :: xs) = op:: (f x) (map f xs) aside from the “plumbing” of `return`, `<$>`, and `<*>`. Indeed, the whole motivation of applicative functors, as well as the source of their name, was a desire to write code in a form closer to an applicative style, which is to say non-monadic, direct-style code like the SML example. The blog post says > Does it print the values in forward or reverse order? One could implement it either way. but obviously this is also true of `mapM`. That would just be a different function. Monadic sequencing does not help with this at all. Furthermore, the author mentions algebraic effect systems. It isn’t clear to me from the wording if the intent is to offer them as a solution for the shortcomings of monadic encodings or as a nicer way to pin down evaluation order, but the latter is certainly not true—the two are entirely orthogonal. Algebraic effect systems depend on the evaluation order being well-defined by other means to work in the first place. In fact, one could argue that the entire point of algebraic effect systems is to allow the composition of different effects while respecting an underlying notion of evaluation order.