I've seen various posts about Elixir's gradual type system pop up on HN, but haven't been following too closely. Does anyone know whether this particular gradual type system can change the asymptotics of programs vs untyped code? As far as I'm aware, most gradual type systems (e.g. Racket) can make programs run asymptotically slower, although there are some exceptions [1].

[1] https://doi.org/10.1145/3314221.3314627

▲

eben-vranken 3 hours ago | parent [-]

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 3 hours ago | parent [-]

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

that said, I'm a fan

	▲	josevalim an hour ago \| parent [-]
		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.