[eben-vranken]

Elixir's gradual type system cannot change the asymptotic complexity of your programs. The design explicitly rules out mechanism that causes slowdowns in other gradual type systems (runtime casts at static/dynamic boundaries)

Most gradual type systems insert coercions when values cross the types/untyped boundary (checking every element of a list, wrapping values in typed proxies, etc) but Elixir's team published a "strong arrows" result specifically to achieve soundness without those runtime checks. The bytecode the compiler emits is semantically identical to untyped code.

[dnautics]

i think the design can push people into writing unnecessary matches/guards just to trigger the typechecker.

that said, I'm a fan

[josevalim]

That can be a concern indeed but it is worth noting that strong arrows compose/propagate. So if you have a function without guards that calls a function that guards on said types, the caller is also strong! We will likely have mechanisms to measure "strength" when we introduce type annotations.

[asa400]

Is it fair to think of this as the ability for type information to be propagated in both directions, e.g. both up and down the callstack? So callees down the callstack may receive any type information the caller might have, while callers up the stack may also receive any information callees further down the stack might have? Please correct me if my understanding of what you wrote is way off base!

[josevalim]

That happens with a single module but not across modules because being able to hot code load modules is an essential ability in Erlang/Elixir.

[dnautics]

very cool. would be even cooler if you could disguise type annotations as dialyzer annotations :P

[arcanemachiner]

I had to do this just the other day. I found it to be a minor papercut, but it was an easy fix.