Static and/or Dynamic Types

Chat
#1

If you’re using PureScript there’s every chance you’ve read the same blog posts and heard the same pros/cons a bunch. If you’re like me, you enjoy having a compiler enforce some invariants in your software systems. This is a sort of ramble about why I’m not sure it really makes sense to extol the virtues of static or dynamic types.

The thing I’d like some feedback on is whether people agree that Static types live on a spectrum for how static they are. Does it even makes sense to say such a thing? Let me try to explain:

You can have a list whose length can only be known at runtime or a list that tracks it’s length statically in the type system. I have this intuition that the second type of list is less dynamic. I can tell you exactly how much memory to allocate for the second, whereas I still need some additional runtime information before I can allocate memory for the first. I’m not sure “information I need before I can allocate memory” is the best proxy for “how static vs dynamic is a type,” but I don’t really have anything formal since the whole difference is a bit fuzzy for me. Different types with identical runtime representation can sit in different places on the static->dynamic based on the API they expose (For example: If the size of an array is just its capacity, then perhaps it’s length is still dynamically set by some terminal character).

In light of the idea that types can be more or less dynamic and that many (most?) of the types used in static types systems aren’t wholly static (I suppose wholly-static types have no runtime representation - like proof terms), it seems to me that the extreme positions in this static vs dynamics arguments take a different form.

I’ve never used a statically sized vector which means, I suppose, that I’m less of a static-type zealot than somebody who will only use dynamically sized vector’s as a last resort when absolutely necessary.

In statically typed languages, the boundaries of a system are often defined with types that carry a lot of type information dynamically. I suppose part of the role of a parser (esp. in a static language) is to take dynamic-er types and express them as static-er types (for certain scopes at least - since errors are types, why not).

I suppose the view I hold that I’ve not really seen spelt out before is that “While dynamic type systems feel lacking to me, dynamic types do not”.

#2

A type is just an assertion about a term.

You can use static analysis tools—including the tools built into a compiler—to verify assertions about your programs. You can also build logic into your program to verify assertions at run time. That’s the essence of the static/dynamic divide. It’s only a ‘spectrum’ if you believe that sets are on a ‘spectrum’ from the empty set to some universal set—imagine the set of all assertions you’d ever want to make about your program. Some of them can be checked statically, some of them can be checked dynamically, some both, some neither. There will always be more assertions you might care to make about some term, so in that sense there’s no such thing as a ‘wholly-static type’.

3 Likes
#3

:smile:

A type is just an assertion about a term.

I’ve never really thought about it that way, but that’s a very succinct way to talk about what a type is. I suppose (in theory) you can write programs about which you don’t formally check any assertions about your terms.

There will always be more assertions you might care to make about some term

Wouldn’t it be the case that, say, I could assert that a term is itself. Say the constant 5 is asserted to be a 5 at the type level, what more could I say? Or am I looking at that the wrong way around?

#4

As examples, you could say that 5 is a valid response to a particular survey question. You could say that it’s a measure of length or area or time, or specify what units it’s provided in. You could say that it’s a valid product ID in your product database table. Any of these things could be expressed in the type system or validated at run time, but none of them are intrinsic to the term 5 without some additional information.

2 Likes