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