A type system that bakes failure into its model is instantly way more productive of a language.
Fairly unrelated, but once upon a time I messed around with creating a scripting language that used ternary Kleene-Priest logic for all of its control structures, rather than the binary Boolean logic that we’re used to using. I did this on a whim because I saw that Fortran used to have three-way if statements and something in me just thought that would be really cool.
As I was developing it, I thought about how to make this system actually useful, and it occurred to me that this was a very natural place to put type checking. This was a dynamically typed language, and so normally to impliment that kind of stuff you’d use assertions or exeptions or reflection. The problem with each of those paradigms is that they’re something extra the programmer has to remember to insert, but if your type checking mechanism was baked into your logic system and control flow, then it would become ubiquitous.
It looked a little like this:
Code:
if x > 5:
then: // Explicit true block
return x - 5
else: // Explicit false block
return x
err: // Explicit unknown block
print("Looks like X isn't a number!")
return unknown
Where unknown is the name of the third logical constant. The comparison operator does a type check, and instead of throwing an exeption or returning false if X is the wrong type, it returns unknown, and the if statement upon seeing the unknown jumps to the block labelled “err”. Thinking about it now, it would be great to combine this with an errors as values scheme. Imagine the previous statement but returning
error(“value is not a number!”) in the err block.
This wouldn’t have the advantage that errors as values has in statically typed languages, that is explicitly flagging which functions can fail, but the thing about dynamically typed languages is that (theoretically) every function could fail, so it balances out.
I thought it was a neat idea.