My relationship with types is... complicated. Languages without types (asm) or too [stringly-typed](https://hacklewayne.com/stringly-typed-it-s-not-that-simple) (TCL) feel sloppy and fatiguing to use at scale, but I also find myself strongly disliking the work products of the "if some types good, more types better" mentality - and as I'll talk about later, I have my own atypical view of what a type _ought_ to be, above and beyond the type systems we usually see marketed. What I find worth exploring lately, though, is that "strong" type systems have similar patterns of diminishing returns as Property-Based Testing.

So what _is_ PBT? It's not really related to "properties" as the word was used in a lot of programming languages (fields within a record), it's more about _characteristics._ The classic example is addition. How would you test this function?

```python
def add(a: float, b: float) -> float:
	return a + b
```

You might already have some conventional answers, but let's look at a PBT approach first and then loop around. One of the properties of addition is that it's _associative_: if you're adding a few things, the order doesn't matter.

```python
def test_add_associative(a, b, c):
	assert add(add(a, b), c) == add(a, add(b, c))
```

Now, if you had a test harness that generated random numbers for `a`, `b` and `c`, which had a priority towards "edge case" numbers like +/- infinity, NaNs, etc., you could test points all over the number line, and catch a lot of failures without spending a lot of electricity on a high case count.

Of course, plenty of things are associative that aren't addition. Multiplication, for example. Right now, this totally bogus implementation would pass our tests:

```python
def add(a: float, b: float) -> float:
	return a * b
```

To combat this, you can test for more and more properties to see that they hold generally, in situations you never consciously thought to check. Properties like reversibility:

```python
def test_add_reversible(a, b):
	assert add(a, b) - b == a
```

This is kinda cool! You get to enforce multiple patterns of behavior across wide swathes of the input space. On the other hand, let's say that for our second test, we did something more conventional: a couple hand-chosen test cases where we know exactly what we expect.

```python
def test_add_handpicked():
	assert add(0, 1) == 1
	assert add(1, 2) == 3
	assert add(-3, -4) == -7
	assert add(0.5, 0.75) == 1.25
```

This doesn't cover very much of the input space, but it covers a ton of the property space - quite a lot of behaviors on display here. With just one property based test and a handful of cases, we've made it very hard to contrive a bad implementation on purpose, let alone by accident.

This is why it's not really PBT _versus_ conventional - the two can be combined to cover each others' weaknesses at an insane effort-to-reward ratio. Let's not, as they say, pit two bad bitches against each other.

Obviously, the examples I'm using here are intentionally trivial, but PBT really shines for complex functions under test. Consider a modern video codec - extremely complex, targeted by adversaries, and with performance pressure to be written in raw assembly. So, you write a clean, simple, assert-stuffed reference implementation with mostly or entirely conventional tests. Then you make a property test: "feed the same random input into the reference impl and the optimized impl, and check that you got the same answer." This isn't theoretical! The `dav1d` project, which is the fastest implementation of the AV1 video codec, relies on [checkasm](https://checkasm.videolan.me/getting_started.html) to verify parity between the outputs of reference code and platform-specific assembly. They also use fuzzing, which is just PBT checking for the property "does not crash," and some clever input generation to autodetect which possible inputs are most likely to be worth checking.[^1]

On the other hand, trying to test things with PBT _only_, and still have the tests in an adequate state, ends up being a long game of diminishing returns. Think about how many properties you'd need to define abstractly before you could really be sure that `add(1, 3) == 4`. And also, I've handwaved quite a bit about the cognitive and runtime cost of the harnesses for these things. Sure would be silly if we _weren't_ using concrete values hand-in-hand, here!
## Typemaxxing

Okay. So let's say there was an extremely popular tool within programming, which:

 * was really good at enforcing some constraints across the entire input space,
 * didn't always tell you everything you need to know,
 * didn't enforce every property you care about,
 * but could asymptotically approximate those missing pieces as you throw ever more effort at describing your constraints.

I know it sounds like I'm describing PBT. But am I? Or did I leave enough wiggle room in the constraints that they could be satisfied by something else? I'm "actually" (equally) talking about type systems!

Enough addition. Let's talk division.

```python
def div(a: float, b: float) -> float:
	if b == 0:
		raise ZeroDivisionError()
	return a / b
```

Really, we have two possible outcomes, which we can fudge our way to thinking of as possible return types. Most of the time, we'll get a `float`, but sometimes we'll get an `Exception`. It depends on the zero-ness of `b`, but that's not in the type system. Let's make the type system a little smarter.

```python
class NonZeroNumber(object):
	def __init__(self, val: float):
		assert isinstance(val, float)
		assert val != 0
		self.value = val
	
	# Various miserable glue to otherwise act numeric
	...
```

Now we can communicate a constraint to the `div` function, and it can force us to check for zero-ness earlier, as a precondition!

```python
def div(a: float, b: NonZeroNumber) -> float:
	return a / b.value
```

Well cool. Our new `div` function now has a more honest return type - it can't fail, so it's not actually implicitly `float | Exception` anymore. We can skip a check within the `div` function too, which is great for performance, as a single divisor value might be used for a lot of division operations, and now we can just check once up front.

Unfortunately, `a` can still be zero, so if you're chaining divisions, you're going to need to constantly re-wrap values in `NonZeroNumber`s. And, as commented in the example, these wrappers aren't ergonomically free, although some languages make them less painful with things like guard clauses or the `?` operator. And zero-ness isn't the only property you may end up caring about, so you end up having to worry about how to communicate _multiple_ traits of numbers: `2` is even, prime, an integer, greater than zero (and thus also non-zero), one of very few numbers where `x*x == x+x`, a power of two (which allows turning expensive divisions into cheap shifts), and probably ten other properties I'm failing to think of offhand. Which traits are worth checking ahead of time?

It's not that this technique is never useful, but it's never a free lunch either. Which means, as you solve more and more "properties of values" problems with the type system, the obvious wins will dry up, your typedefs will become too numerous to easily hold in your head, and you'll be paying the same costs or more to get the same benefits or less. The returns will diminish, and the line where the work stops being worth it is blurry and subjective.

Now, consider the following code:

```python
average = div(a + b + c + d, 4)
```

If we _inline_ the original `div` function, specializing it for the divisor of 4, we have such a bounty of information that an optimizer _could_ turn this into a shift in just a couple steps.

```python
average = (a + b + c + d) >> 2
```

That's the power of knowing a _concrete value_, which is specific enough to carry an absolutely massive bag of implicit properties. Neither `div` nor its caller really needs to find a way to talk about zero-ness or powers-of-two in a way that the type system understands, they don't have to coordinate with each other via a precondition enforcement system, it's just kinda... obvious.

The need for concrete data in order to understand and debug applications only scales with the subtlety of the constraints. Maybe you have a record type `Person` where `.fullname` needs to start with `.firstname` and end with `.lastname`[^2]. Is your type system expressive enough to enforce that? And if it is, what costs are you paying for that expressiveness? Some languages can handle this specific example very well, but then fall down for something differently subtle. And the more capable your type system becomes, the more it becomes a beast to learn in its own right, expensive at compile time, a fountain of contextually spurious errors, etc.

This is, of course, not some argument against ever using types at any level of granularity. If anything, the problem is that programming languages have a narrow idea of what types can be. The more expansive idea of _what is a type?_ in my own head is "anything you could possibly think to assert about a value," whereas what most languages can actually enforce for you is limited to schema and layout. Type-y things I care about often vary wildly _within_ the input space of language types, and can only be resolved against concrete values.[^3]

While I have complaints about TypeScript, I find it fascinating that in order to retrofit schemas onto untyped data, they actually had to start treating concrete values like `"some_string"` as types themselves, such that the tag for a discriminated union might be `"a" | "b" | "c"`. Prone's type system takes some cues from this!

This is also why C++'s `constexpr` is so powerful: it operates in the realm of concrete values. It can't prove that a function works correctly across all inputs, but it can prove the function works correctly across the inputs that actually get used:

```cpp
constexpr int div(int a, int b) {
  return a / b;
}

int main() {
  return div(5, 0); // This will cause the build to fail!
}
```

Of course, programs operate on a lot of non-constant values too, in hostile environments full of data that won't be known until deep into runtime, which is exactly where types and assertions can help communicate and enforce: "this function can handle anything you throw at it, as long as it's in a shape we've declared support for." This is why Prone is a hybrid approach: moving computation into compile time reduces the burden on the type system, but you still have a type system, and it can be expressed/enforced with arbitrary assertions.

[^1]: This is why Prone is going to have PBT tools in the standard library as part of the built-in test framework. Prone is, from a certain angle, a scripting language that encourages optimizing your code to ludicrous speeds. Using slow, safe reference code as the test criteria for lower-level hand-optimized alternatives is expected to be a common pattern, including within the stdlib itself.

[^2]: [There are reasons not to do this.](https://www.kalzumeus.com/2010/06/17/falsehoods-programmers-believe-about-names/) But it's simple to explain, and most of my audience has had to deal with similar logic at some point in their careers.

[^3]: This helps to explain why languages with strict types tend to have similar defect rates to less excessively-typed languages. I joked about the "Cult of Typists" in the title, but it really is a thing that people will treat types as their One Hammer for correctness problems - which is not adequate _and_ becomes a tumor-like burden to maintain - and then look down their noses at people who aren't persuaded by type orthodoxy.