A float walks into a gradual type system

https://ruudvanasseldonk.com/2025/a-float-walks-into-a-gradual-type-system

by ruuda • 1 year ago

29 8 1 year ago

It seems that the author's notion of referential transparency is too strong because it is typically about evaluation semantics, not about a type system. You can easily imagine the case where such notion would immediately break down with usual subtyping.

eyelidlessness• 1 year ago

I found their usage of referential transparency odd at first, too. But as I thought about their reasoning more, it clicked for me. If two numeric bindings are semantically distinguished not by their numeric value in absolute terms, but by their assigned type, you can think of it as if assigning the type is conceptually equivalent to a function call, which returns a value composing the numeric value and the type’s semantics. Eg

    let a: Int = 1 // let a = Int(1)
    let b: Float = 1.0 // let b = Float(1.0)

Even so, I think this is solvable by:

- De-composing the numeric value for comparison only

- De-composing and re-composing the numeric value for assignment

If you can’t do either, i.e. because one underlying value is inherently incompatible with the other in some way, then you have a static type error regardless of how your semantically distinct types interact.

AlotOfReading2• 1 year ago

I thought this was going to be about NaNs, signed zeros or other things that are fundamentally different between floats and integer types. I don't really understand why accepting implied or overspecified zeros is deeply problematic here. You're already allowing the user to omit the 14+ zeros of precision actually represented in the underlying value and there's no confusion about what the correct answer is in either case. The minor ambiguity with type inference (let b = 1) can be resolved in favor of integers without surprising anyone.

Someone• 1 year ago

You're already allowing the user to omit the 14+ zeros of precision actually represented in the underlying value and there's no confusion about what the correct answer is in either case

In json, there’s considerable confusion possible, as you don’t know how much precision is “actually represented”. For example, is “1.3” meant as a float, as a double, as a big decimal? In most languages, (double)1.3f prints as 1.299…, and is different from 1.3

AlotOfReading2• 1 year ago

That would be a good reason to be careful about floats, but it's not the issue described. There's just one implementation for the author's language with just two types: some kind of integer and some kind of real called "number". Any choice they make for the latter would have the issue in the article, but wouldn't have the issue you're describing, because there'd be a single nearest value in the chosen representation.

sfink• 1 year ago

Huh. If I had to pick a constraint to jettison from that list, I think I'd pick 1 == 1.0. In fact, I'd prefer an error when testing 1.0 == 1.0. It only makes sense to compare floats in very limited situations. While admittedly this is one of those situations where it could make sense, as long as floats aren't the result of calculations in this language, it's still better than discarding any of the other constraints given that it's not fundamentally a very meaningful operation. (One could argue that comparing float constants is ok, just not calculated floats, but it still doesn't seem that useful.)

Then again... I have a little more trouble discarding floats as keys, including floats as set members.

And anyway, you can't stop floats from being weird. 0 vs -0. NaN. +/-Infinity.

childintime• 1 year ago

There were three places — fewer than I expected! — that previously were infallible by construction, but now need a runtime check to ensure that a number is an integer. For example, when indexing into a list

A float actually sounds like the perfect way to index a list: anything in the range from from 0 to 1 (excluding either) would map to the first element. It works just like the wheel of fortune. Well almost, with the wheel exactly 0 or 1 would be invalid. So you might want to index using 0.5, 1.5, etc instead, and the implementation can round up or down the way it wants. We've solved a language incompatibility issue, lol </rant>

lblume• 1 year ago

Floats are, by their very nature, imprecise, so "excluding either" would not work up to a point. I would not want my choice of element to depend on the result of 0.1 + 0.1 (e.g. when multiplying by 10).

A float walks into a gradual type system

Related Stories