> 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.
What was wrong with SML?
51–60 of 82 posts
Re: What was wrong with SML?
#52I'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…
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?
#53Earlier 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%
Re: What was wrong with SML?
#54Earlier 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%
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.
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?
#56I 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.
I've been very interested in CakeML lately, do you use it for anything?
Re: What was wrong with SML?
#57IMHO 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…
The only PL example I can think of is unification, which logic programming has as well as evaluation.
Re: What was wrong with SML?
#58Earlier 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).
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?
#59IMHO 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…
Re: What was wrong with SML?
#60Earlier 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…
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.