Everything Should Be Typed

Media
1

This was an interesting read, and I thought the fine people of Ziggit could add some more color to the discussion. This seems like something that should be layered on top of a language, not part of the core of a language.
We do have this concept as part of Zig already. Non-exhaustive enums allow for custom int types with good ergonomics. Are there other ways to further wrap slices or things like that?

2

Obligitory nod to Matklad’s writeups on this as well:

3

Meeeh
 :slight_smile: IME too strong typing is just as bad as too weak typing. The sweet spot is somewhere in the middle, but nobody agrees what the ‘correct’ sweet spot is.

There’s too many issues to list, but from what I’ve seen over the years:

While strong typing makes code more robust, it also makes code more change resistant since the strong types need to creep into each corner of the code, otherwise “you’re doing it wrong”.

..and: let’s say two unrelated libraries define two “identical” types const Meter = u32;. Should those two types be assignable to each other? Obviously yes, because they both mean the same thing. But then should those types be assignable from any other u32-derived type (or raw u32’s)? Obviously no because that would break strong typing. So with strict strong typing, whenever I get a Meter as a result from library A and want to put this as parameter into library B I need a MeterToMeter() glue function. That doesn’t make any frigging sense.

What I would like to see in statically typed languages is more support for structural typing. If two unrelated struct types have the same interior (same struct item types and names) they should be assignable to each other!

I’d also like separate type keywords for defining a C-like type-alias versus an “actual” type.

7 Likes
4

No thank you

5

I’d tackle this from a different angle: there should be a place where the type system gives up, and something stronger takes over. We see this in C: the type system is extremely poor, bonkers really, and yet, proving the correctness of C code is something people do.

Heavily annotated C code :slight_smile:

Your meter-casting example doesn’t bother me much, that’s just glue. The same problem can arise from two enums which “should be the same”.

A Temperature distinct type has worse problems: you cannot meaningfully add them, but, you can subtract them! The difference between 10Âș and 20Âș is -10
 but that isn’t a Temperature, is it. It’s “a difference of negative ten degrees”, as in “it cooled down by ten degrees overnight”. A TemperatureDifference.

Adding two temperatures doesn’t produce a sensible value at all! But you can add their differences! It’s madness!

I’d love some compiler support for annotating the meaning of types and variables, to run validators and proof assistants against, in an open-ended way which is beyond the purview of the core language.

You can spot the distinction in the Fine Article: it’s not 100% clear what the relationship between NetAmount, Amount, TxFee, and PlatformFee is modeled as being: but I’d guess there is one. Arguably that means the example is reifying a result and should just not do that, but that doesn’t generalize. Maintaining the double-entry invariant is an easy case to reach for, if it were possible to do that with one variable it would have a different name.

I expect this to be especially powerful in a no-magic language like Zig. Rust handles a lot of invariants with magic, like the reference-count invariant, but that means you can’t see it happen: and a validator can’t either, so an attempt to go beyond what’s built into the type system has a much larger amount of ambient knowledge to pull in from more places.

It’s possible that adding Go-style newtypes to the language would leverage a facility like that, probably the case, even. Defining an enum and then only ever using it as an integer doesn’t ‘favor reading code’, not really; we shouldn’t be too proud of “newtype pattern”, although it’s better to use it than not.

But the facility is the important part, not the newtypes. If I’m defining Meter, I’m going to want to ensure that meter * meter gets assigned to SquareMeter: and I don’t think building that into Zig is going to happen, or that it should.

The amount of premises one might want to validate isn’t bounded, after all. A facility with which to state them which isn’t just ‘special comments’ would be nice though.

4 Likes
6

A more common situation is that, even if they refer to “similar” things, one uses u32 while the other uses u64, or even if their underlying types were originally the same, then after a library update, it decides it should expand from u32 to u64. Unless you never assume that a library’s version will be upgraded, relying on this kind of pass-through based on underlying types can bring endless trouble. Interaction between libraries is inevitable, and glue code is always unavoidable.

However, there is indeed a situation where, even in the interactions between different libraries, I can be certain that the essence of the same type defined by each of them is always the same: protocol-prescribed Types.

For this type, Zig defines them using extern struct, and for types with the same layout, it is easy to use @bitCast to convert to the corresponding isomorphic type without needing additional glue code.

1 Like