later in a project where you know for sure something can be known at compile time, of course I love to check them at compile time.
As far as types go, I've found that types actually help more during prototyping than later on. (At least for code I've written myself; types are great for helping me navigate other people's long-term codebases!)
Types give me a way to sketch out and iterate on an overall design without needing to implement anywhere near all the logic I'd need; then, when I start in on the logic, it naturally lays down on the skeleton the types provide. Compared to my experience with Python—where I still use some types!—I've found it easier to start and quickly try different designs in Haskell.
I guess what I wanted to say is that, in the long run, compile-time checks may become runtime checks, especially something like enum values where at the beginning, enums are fine choice but soon you will find yourself where you have to store that to a DB etc.
Problem is, moving from compile-time check to runtime check isn't that straightforward in a lot of cases.
I believe most code is old. You mostly notice code that changes.
Types are the cheapest semantic documentation you can write, and your compiler/type checker can provide additional guarantees based on them.
Not only that, they're notes to future contributors/yourself about how a program works, so they/you don't have to reverse engineer code that was written a while ago in order to modify it with confidence.
They are not.
Unfortunately, especially Haskell world seems to think they replace documentation, that's why so much of "documentation" for a lot of Haskell libs are just a dump of types with no explanation of what they mean, how they interact, what the functions using them do, or how they can be used.
> they're notes to future contributors/yourself about how a program works
They are not. Types do not describe how a program works.
> so they/you don't have to reverse engineer code that was written a while ago in order to modify it with confidence.
Yes, you will have to reverse engineer code that was written a while ago. Because types only describe, well, types. You code contains logic. And logic is the hardest part to understand.
Personal anecdote: worked on a system that was transitioning from original ad-hoc implementation to a better designed one. Some functions would accept a Person. Others would accept a Contact. Why? How to convert between the two? What are the differences? What was behind the decision? Why did `is_empty(new_contact())` returned `false`? And so on.
Thank god it had types, right? No need to reverse engineer.
I see types as mere tests. More robust, yet more limited in scope. FWIW it's much easier to see them that way once you introduce dependent types into the discussion, but it applies to the simplest type systems just as well.
I don't see types as serious tests and I don't think they are robust. let's say that some integer must be between 10 and 100, do you use type checks for this?
A lot more awkward than dependent types, but no popular language has those.
I definitely do. In my experience, it's much easier to adopt a discipline of testing (and static typing) early on than it is to try to retroactively add that to an existing system, which may or may not be written in a way that is even testable.
But I do appreciate that viewpoints can differ on this topic. Regarding types, I studied type theory academically, so types are natural to me and don't really add any extra cognitive work (and perhaps they eliminate some). So I might as well use and benefit from them if they basically cost me nothing. But for someone who thinks of static typing as just trying to make the compiler happy (perhaps because they don't really understand the type system or because the type system is not ergonomic), I can see why they might have a more pessimistic view of it.
Yes. I explicitly mentioned dependent types for this reason.
This is also expressable in a more limited fashion in a language like TypeScript, although some may argue it also employs a form of dependent typing.
Yep. In particular, I would use:
- A "wrapper" type around an unsigned byte (we don't need negatives, or a whole machine word)
- A "newtype" feature, to replace the wrapper with a Byte after type-checking (Haskell calls this "newtype"; Scala calls this "opaque type aliases").
- A private/unexported/scoped constructor, to prevent arbitrary Byte values getting wrapped
- A "smart constructor" which checks the bounds of a given Byte, returning a 'Maybe MyBoundedIntType' or some other type-checked error mechanism (Scala's 'Try[MyBoundedIntType]' works well).
- Polymorphism/overloading to call that smart constructor of various numeric types (char, int, long, signed, unsigned, etc.)
In Scala that would look something like:
opaque type MyBoundedIntType = Char
object MyBoundedIntType {
def apply(c: Char): Try[MyBoundedIntType] =
if (c >= 10 && c <= 100)
Success(c)
else
Failure(new IllegalArgumentException(s"Value ${c.toInt} outside range [10, 100]"))
def apply(i: Int ): Try[MyBoundedIntType] = Try(i.toChar).flatMap(MyBoundedIntType(_))
def apply(l: Long): Try[MyBoundedIntType] = Try(l.toChar).flatMap(MyBoundedIntType(_))
}
module MyModule (MyBoundedIntType(), toByte, MakeBounded(..)) where
newtype MyBoundedIntType = MBIT { toByte :: Word8 }
class MakeBounded t where
mkBounded :: t -> Either String MyBoundedIntType
instance MakeBounded Word8 where
mkBounded b | b >= 10 && b <= 100 = Right (MBIT b)
mkBounded b | otherwise = Left ("Value " ++ show b ++ " not in range [10, 100]")
instance MakeBounded Int where
mkBounded i = toWord8 i >>= mkBounded
instance MakeBounded Integer where
mkBounded i = toInt i >>= mkBounded