Live data from Hacker News

What was wrong with SML?

blog.plover.com

51–60 of 82 posts

Re: What was wrong with SML?

#51

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

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.

Ah shit, well I guess you found the 0.1%

Re: What was wrong with SML?

#52
post #28

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 "spec…

As I explained in https://news.ycombinator.com/item?id=31222098, I don't think this explanation is correct. You're right that bool → bool is not a subtype of α → α, and that function types are contravariant on their argument type. But because function types are not also covariant on their return type, the same logic would tell us that α → α is neither a subtype of bool → bool nor a supertype.

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 = 
And we can define a function of type α → α:

    # let f = fun x -> x ;;
    val f : 'a -> 'a = 
And that function is perfectly acceptable as the argument to abool, or indeed in any other context where we need a function of type bool → bool:

    # abool f ;;
    - : bool = false
Thus α → α is a subtype of bool → bool, and also int → int, string → string, etc. And this is not because the value restriction has been sneakily applied behind our backs; f and abool still have their original types:

    # abool ;;
    - : (bool -> bool) -> bool = 
    # f ;;
    - : 'a -> 'a = 
And we can still apply abool to a function that's unashamedly bool → bool:

    # abool (fun x -> not (not x)) ;;
    - : bool = false
    # not ;;
    - : bool -> bool = 
    # abool not ;;
    - : bool = true
So specialization is not another name for covariance, and you absolutely can specialize α → α to bool → bool.

Re: What was wrong with SML?

#53

Earlier quoted context omitted.

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.

Ah shit, well I guess you found the 0.1%

This is completely off topic here, but the first promotion of Int64 -> Float64 is also iffy as not every Int64 is exactly representable. The Int64 -> Float16 promotion also looks weird to me because Float16 range is so small

Re: What was wrong with SML?

#54

Earlier quoted context omitted.

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.

Ah shit, well I guess you found the 0.1%

You think negative numbers in a signed type are a 1-in-a-1000 case, really?

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

Re: What was wrong with SML?

#55

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

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.

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

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)
is a different result from

      -10   (Int8) +   10 (UInt16)
      246  (UInt8) +   10 (UInt16)
      246 (UInt16) +   10 (UInt16)
      256 (UInt16)
One of those should be the result Julia gives. I tend to hope it's the first one. That would correspond to a promotion strategy of "always expand the type to its full width before converting between signed and unsigned". Expansion (and shift, I guess) is the only operation for which the difference between signed and unsigned is relevant.

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

Re: What was wrong with SML?

#56
post #6

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.

>CakeML is also a very cool project in SML land.

I've been very interested in CakeML lately, do you use it for anything?

Re: What was wrong with SML?

#57

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 o…

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…

I'd like to see more use of things that are more powerful than evaluation. For instance, in mathematical functions you can differentiate them, or invert them, and both of those are obviously useful in mathematical "metaprogramming".

The only PL example I can think of is unification, which logic programming has as well as evaluation.

Re: What was wrong with SML?

#58
post #54

Earlier quoted context omitted.

Ah shit, well I guess you found the 0.1%

You think negative numbers in a signed type are a 1-in-a-1000 case, really? 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).

Related, an integer bug that can't be fixed in C is that "unsigned short" promotes to "int" instead of "unsigned int", so this doesn't produce the result you want.

  unsigned x = (unsigned short)65535 * (unsigned short)65535;
(It overflows even though it's less than UINT_MAX, and worse it's UB.)

Re: What was wrong with SML?

#59

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 o…

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…

Haskell is such a language. You can enable strict evaluation on a per module basis, or for an entire package.

Re: What was wrong with SML?

#60
post #45

Earlier quoted context omitted.

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.

In strict languages, you can delay computation by wrapping it in a zero-argument lambda -- i.e., a "thunk." For efficiency, you want to memoize thunks (that's what Haskell does[1]) so that they only ever evaluate once. Scheme has the "delay" operator to create memoized thunks, which you can later "force". It is true that these are not first class in the sense that you need to manually force the computation, but if it…

So I had a bit of fun implementing something like Haskell’s “Validation” in an eager language recently that has coloured my take somewhat. Basically “perform all these computations and tell me all the things that were wrong with my inputs” is way easier to express in a default lazy language than a default eager language. In default eager you’re constantly trying to figure out the largest number of operations you can do before can no longer continue.

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.

Post reply on HN