What was wrong with SML?
blog.plover.com
blog.plover.com
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.
See also: https://en.wikipedia.org/wiki/Lazy_evaluation#Simulating_laz...
let y = f(x) in g(y, y)
If you want conventional lazy evaluation, that is “call by need”, you need to memoize: wrap everything in stateful functions (“thunks” in Haskell-implementer-speak, “promises” in Scheme-speak, but not the same as E/JavaScript-style async promises) that compute the result and save it on the first invocation, but then return it immediately. Apart from efficiency considerations (it’s better to use a tagged union of function pointer and result value instead of calling the function all the time) and a single conceptual wrinkle[1], that’s it.
Call-by-name and call-by-need obviously yield very different complexity, but are in fact equivalent regarding termination, and optimal: if any evaluation strategy terminates on a given term, so do they. The lovely recent paper “Call-by-need is clairvoyant call-by-value”[2] shows that lazy evaluation in fact never does more steps than call-by-need and in fact does a subset of them: those and only those that influence the final result. (The problem, of course, is that none of this addresses memory usage.)
Emulating eager evaluation with lazy can be done if you have seq: (a `seq` b) means “when this is forced, force (the outermost layer of) a, then replace yourself with b (which will then be forced as much as necessary)”: replacing f(e) with (let x = e in x `seq` f(x)) everywhere is not quite enough IIRC, but gets you most of the way there. In a dynamically-typed language, you can implement seq using some of the built-in strictness, like
a `seq` b = if null(a) then b else b,
[1] https://srfi.schemers.org/srfi-45/srfi-45.html
[2] https://www.cs.nott.ac.uk/~pszgmh/clairvoyant.pdf, https://youtu.be/S69UOGqda8w
[1] Incidentally, this is why Haskell's garbage collector needs to be able to deal with mutation. A thunk might graduate to an older generation, and once it is finally evaluated it can end up having pointers to the nursery or other younger generations.
Yes, there’s weird perf things that can bite you, but there’s also a bunch of regular bread-and-butter coding things that pervasive makes very much easier.
class Thunk:
def __init__(self, f):
self.evaluated = False
self.val = f
def __call__(self):
if not self.evaluated:
self.val = self.val()
self.evaluated = True
return self.val
class Cons:
def __init__(self, x, xs):
assert isinstance(xs, Thunk)
self.head = x
self._tail = xs
@property
def tail(self):
return self._tail()
def nth(self, n):
for _ in range(n):
self = self.tail
return self.head
ones = Cons(1, Thunk(lambda: ones))
print([ones.nth(i) for i in range(10)])
# [1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
def lazy_map(xs, f):
return Cons(f(xs.head), Thunk(lambda: lazy_map(xs.tail, f)))
nats = Cons(0, Thunk(lambda: lazy_map(nats, lambda x: x + 1)))
print([nats.nth(i) for i in range(10)])
# [0, 1, 2, 3, 4, 5, 6, 7, 8, 9]
def lazy_zip(xs, ys, f):
return Cons(f(xs.head, ys.head), Thunk(lambda: lazy_zip(xs.tail, ys.tail, f)))
fibs = Cons(0, Thunk(lambda: Cons(1, Thunk(lambda: lazy_zip(fibs, fibs.tail, lambda x, y: x + y)))))
print([fibs.nth(i) for i in range(10)])
# [0, 1, 1, 2, 3, 5, 8, 13, 21, 34]
I once took advantage of this in a light way when designing a compiler targeting C in Haskell, with a goal of making beautiful-ish C code. The language, unlike C, was expression-based, so everything could evaluate to a value. The step that lowered expressions into C syntax returned a struct with multiple fields, each giving a piece of C syntax depending on how the expression was going to be used in context -- was the value of the expression going to be used? or just its side-effect? Then, due to laziness, only one of the fields of the struct would actually be evaluated. (It also handled other cases: lvalues and whether the expression's value was going to be immediately stored somewhere, since then the expression could use that location directly rather than creating a temporary variable if it might have needed one.)
But, the effort to implement call-by-need evaluation (graph rewriting or remembrance of computed value) is higher in strict languages than (sparse) addition of annotations in lazy ones.
The only PL example I can think of is unification, which logic programming has as well as evaluation.
A programming language where you can write programs to rewrite programs.
It appears that author of Pure is prone to come up with PL names that are quite unsearchable.
There is also another GHC extension called bang patterns to request strictness on pattern matches.
The original bang (`!`) which is Standard Haskell can make fields of data structures strict, see: https://wiki.haskell.org/Performance/Data_types#Strict_field...
In general both lazy and strict languages can be strict or lazy. But the way it shows in the data types is different. A strict language can defer evaluation by adding a level of abstraction (instead of type `X` you have `() -> X`). A lazy language can force evaluation (it will have to evaluate at some point anyway) but you might not see it in the type. I’m not sure which one is better to be honest. Being able to infer laziness/strictness from the type is nice, but it also hinders interoperability.
Also, your suggestion will result in identical code being copied for different contexts. Consider lazy structures in OCaml and C#.
[1] https://www.reddit.com/r/sml/comments/qyy2gs/getting_started...
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
Silently casting signed integers to unsigned is a terrible idea, and a recipe for bugs. And completely unnecessary to boot, because you could promote Int8 to Int16, and (Int16, UInt16) to (Int32, Int32).
unsigned x = (unsigned short)65535 * (unsigned short)65535;
Well....
Signed integer arithmetic and unsigned integer arithmetic do not differ. At all.
The difference between an Int16 and a UInt16 is not in the 16 defined bits. It's in the infinite number of implicit bits representing place values above 2^15. Those bits are always 0 for the UInt16, but they're identical with the high bit of the Int16.
So it's not clear what it would mean for the result type to be "incorrect mathematically". Mathematically, an Int16 and a UInt16 are the same thing.
However, the path by which you promote the values does matter. I don't know what Julia does. But:
-10 (Int8) + 10 (UInt16)
-10 (Int16) + 10 (UInt16)
65526 (UInt16) + 10 (UInt16)
0 (UInt16)
-10 (Int8) + 10 (UInt16)
246 (UInt8) + 10 (UInt16)
246 (UInt16) + 10 (UInt16)
256 (UInt16)
> Would a better promotion be Int32 for both?
Probably not; that would imply that when you add two UInt16s together, you expect to get a UInt32 (or UInt17...) back.
Great point on the path dependence.
That depends on what you're hoping to do with the number you're looking for. If you wanted -5 as an Int16, the bit pattern would be 1111 1111 1111 1011 or 0xFFFB.
If you wanted 65531 as a UInt16, the bit pattern for that is 1111 1111 1111 1011 or 0xFFFB. You're getting the same result either way. And any values you compute from that result [that is, by arithmetic] are going to be unaffected by whether you labeled the result "Int16" or "UInt16", because that's just a label. If you labeled 0xFFFB a "Snerf", the arithmetic would still be the same.
There are only a very restricted set of places where you need to be explicit about whether you think of your variable as an Int or a UInt:
1. When you're widening it.
2. When you're doing a right shift.
3. When you're formatting it for display to a human.
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.
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.
Any criticism of any language is valid and good to have!
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.
CakeML is also a very cool project in SML land.
I've been very interested in CakeML lately, do you use it for anything?
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 42This is all sound if the language is pure, which ML originally was.
There's also a relevant discussion at Stackoverflow. [2]
[1] This is a fairly concise summary of the quantification rules: https://jgbm.github.io/eecs662f17/Notes-on-HM.html
[2] "Does Scala have a value restriction like ML, if not then why?" https://stackoverflow.com/questions/48594769/does-scala-have...
let m : ∀α. ref (α → α) = Λα. ref [α → α] (λx. x)
in
(m [bool]) := not;
print ((!(m [int])) 23)
end
(The naive model of) SML runs into problems because it erases the big lambdas and so evaluates `Λα. ref [α → α] (λx. x)` to a single ref cell of type `∀α. ref (α → α)`
Sidenote: Variance does have some relation here, I couldn't think of a way to trigger bad behavior without a type that uses the type variable invariantly.
But then it will forget that inference when type checking "print ((!m) 23)"; there it will infer that a == int, and that the original definition of m was really "m = ref (fn (x:int) ⇒ x)".
Essentially the issue is that type inference forgets that it already solved for "a" and can't assign it to both "int" and "bool".
In fact, though, α → α is a subtype of bool → bool, for reasons that have nothing to do with covariance and contravariance. We can define a function whose argument is of type bool → bool; here in OCaml:
# let abool f = not (f true) ;;
val abool : (bool -> bool) -> bool = <fun>
# let f = fun x -> x ;;
val f : 'a -> 'a = <fun>
# abool f ;;
- : bool = false
# abool ;;
- : (bool -> bool) -> bool = <fun>
# f ;;
- : 'a -> 'a = <fun>
# abool (fun x -> not (not x)) ;;
- : bool = false
# not ;;
- : bool -> bool = <fun>
# abool not ;;
- : bool = true
Bound variables are variables that either the programmer wrote explicitly in their program or variables introduced by generalization. They appear underneath a quantifier, as in the type
∀ a. a -> a
In HM, a bound variable only unifies with itself, so if we use `~` to mean “unifies with”, then `a ~ a` holds but neither `a ~ Bool` nor `a ~ b` do, assuming `a` and `b` are bound variables. However, bound variables do not actually get involved in typechecking unless the programmer wrote them in their program explicitly, because when a polymorphic binding is used, the typechecker instantiates it, replacing bound variables with metavariables.
There is no way for the programmer to write metavariables in their types, because metavariables are, as their name suggests, a metalanguage concept introduced by the typechecking machinery, not a part of the underlying language of types. This makes writing them down in a way that clearly distinguishes them from bound type variables somewhat difficult, so I will adopt the convention of using Greek letters to represent metavariables. This means we can instantiate the above type to get
α -> α
All of this stuff might seem a bit fiddly, since we’re explaining metavariables in terms of internal details of a typechecking algorithm. But indeed, that’s the point: metavariables are an invention of the typechecking algorithm, a mechanism used to implement type inference. They aren’t really types, they’re “holes” in types that have yet to be filled in by the type inference process. So when you ask a question like “is `Bool -> Bool` a subtype of `α -> α`”, your question is somewhat meaningless, as it depends on what α means for whatever typechecking algorithm you’re discussing, and pure HM does not really have any notion of subtyping (just instantiation and unification).
If we introduce more sophisticated type systems that do have subtyping, then we have the machinery to talk about things like covariance and contravariance. But in HM, no such relation exists, so any notions of subtyping, covariance, and contravariance exist only in our heads, not in the type system itself. Still, we can informally establish a notion of subtyping by saying that if S is a subtype of T, written `S <: T`, then an expression of type S can be used wherever an expression of type T is expected. Given that, we can ask whether
(∀ a. a -> a) <: (Bool -> Bool)
(a -> a) <: (Bool -> Bool)
To clarify, when I wrote α, I always and only meant a bound variable under a quantifier, because I didn't know about this metavariable thing at all. I was writing α → α because that's how tuareg-font-lock-symbols renders 'a -> 'a, which does include the implicit quantifier.
It's no wonder I was never able to understand HM since I didn't know about this dual nature of variables. This will probably help me a lot next time I try to understand it! I do think I understand unification, though I've only implemented it once.
I really appreciate you being willing to engage on HN, despite the unpleasant aggressiveness and character assassination that runs rampant here.
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
> 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]()
val bools: ArrayBuffer[Bool] = xs[Bool]
bools += true
val ints: ArrayBuffer[Int] = xs[Int]
ints.last
def xs[A](): ArrayBuffer[A] = ArrayBuffer[A]()
> 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)
xs :: forall a. ArrayBuffer a
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)
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.
It sounds like a cool project and I'd love to see it! And even have the option to open a PR and help ;)
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 and https://github.com/SomewhatML/sml-analyzer (again for a fragment of SML)
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.
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/
Grammar and language semantic are details regarding language adoption.
Unreasonably open-ended question (suppose the scope is ML, or perhaps FP in general, or maybe even wider) - but I'm very curious.
- 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.
I thought Scala had an even stricter value restriction than ML, where only function/methods may get a polymorphic type?
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.
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.
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 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). 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>
# `Q 2 ;;
- : [> `Q of int ] = `Q 2
# g (`Q 2) ;;
- : int = 2
# g (f 1);;
- : int = 7
# g (f 2);;
- : int = 5
# let mf o = (o#foo ; o#bar + 1) ;;
val mf : < bar : int; foo : 'a; .. > -> int = <fun>
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.
It didn't have a big company like Sun pushing it