A float walks into a gradual type system
4 comments
·March 3, 2025lifthrasiir
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
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)
- 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.
null
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.