What was wrong with SML? (blog.plover.com)

Grammar and language semantic are details regarding language adoption.

I thought Scala had an even stricter value restriction than ML, where only function/methods may get a polymorphic type?

CakeML is also a very cool project in SML land.

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

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.

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.

[0] http://reddit.com/r/sml

[1] https://www.reddit.com/r/sml/comments/qyy2gs/getting_started...

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.

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.

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/

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

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

It didn't have a big company like Sun pushing it

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

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...

    mapM :: Monad m => (a -> m b) -> [a] -> m [b]
    mapM f []     = return []
    mapM f (x:xs) = (:) <$> f x <*> mapM f xs

    fun map f []        = []
      | map f (x :: xs) = op:: (f x) (map f xs)

> 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.