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”.