Strong Arrows

Notes

Elixir might add types through gradual typing. But it’s challenging to do that.

In particular, gradual typing can either propagate a dynamic() (or any in other languages) type everywhere (making types less useful). Or we can have a discrepancy between what is valid at compile-time (based on the types) and what is valid at runtime.

Elixir has a new way of dealing with parts of gradual typing called strong arrows!

The idea is that if negating the input will always result in an error, then we know the output is the expected type. That’s a strong arrow.

Here’s how the José’s excellent blog post puts it:

a strong arrow is a function that can be statically proven that, when evaluated on values outside of its input types (i.e. its domain), it will error.

For more information, check out the blog post. It’s a great read!

Clarification on debug/1’s return type

A few people have asked, shouldn’t debug/1 return binary()?

I think I made that part a bit confusing. Maybe this helps 👇

In reality debug + identity (with the is_number guard clause) should fail at compile time. So, debug shouldn’t ever return number() and be correct (since it returns a binary).

The question we’re trying to answer is:

What should the type system infer when we don’t have a type signature?

Without the is_number guard clause, the debug function works well with binaries. But at compile time, a regular type system (without strong arrows) doesn’t know what to assign as debug’s return type.

Should it be dynamic() or number()? There are trade-offs to both options.

But once we add the is_number guard clause to identity, then the compiler can correctly say that number() (not dynamic()) would be the return type. But, of course, because of the binary operation <> in debug, it should actually return binary().

So, the compiler should give us an error at that point.