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.