That is correct, the paper describes _ return type being the best approach for gradulized types. It is better to let the compiler type system infer the types and strong arrows using guards as there a number of cases where you can miss out on the benefit of type materialization if you specified the type as a() or b() and eliminated the flow of dynamic, e.g. ```integer() and dynamic()``. This relates to part in Jose’s talk about his t-shirt being allowed to be grey and something else.
adw632
0
Sebb
Just watched the talk, the strong arrow idea is great.
I fear I have code with very few strong arrows or maybe I don’t.
Would it be feasible to bring some tooling that tells us something about our code, how it will behave?
Is the first point on the roadmap “infer types from patterns and guards” maybe that?
0
adw632
That is my understanding, no annotations in the first release, then after that, type annotations on structs.
0
bottlenecked
Not sure if you’ve listened to this, but since Roc was mentioned, there’s this podcast episode where the author of Roc hosts Jose for a discussion on the implementation side of things around the type system Static Types in Elixir with Jo…–Software Unscripted – Apple Podcasts
Not sure if the details have stayed the same since then (~1yr ago) but I thought there’s some nice insights in there
2
josevalim
Creator of Elixir
There is no code with strong arrows today, because a strong arrow must be statically typed (and nothing has a static type today). The idea, however, is that as we make Elixir itself statically typed (and the underlying Erlang functions), then we may find type checking violations in your untyped/dynamic code.
On your side, what you could do is to write patterns and guards, which is idiomatic Elixir code anyway, and this will help the VM optimize code and the future type system to find bugs.
4
Sebb
Sure I understand that.
But when I have functions like these today
def foo(x) when is_integer(x)
def bar(x)
And I’d add
$ int() -> int()
when types are there, I’d have a strong arrow for foo and a “weak” for bar, right?
So thats what I mean. I have no good intuition how many of my functions would qualify for strong arrows.
Would be helpful to have sth early on to get a better view of to codebase in this context.
0
josevalim
Creator of Elixir
It depends. If bar uses other strong arrows functions, then you may get the property by transitivity.
But yes, how to discover and declare if something is a strong arrow or not is something we will tackle/expose at some point. Too early to say precisely how though.
2
konstantine
Excuse my ignorance José, but I am really curious after watching your talk: the expanse of type checking will likely be proportional to its impact on compile times. Clearly, this is an important concern. At the same time, there is little point in introducing a type system without exhausting its type-checking potential.
My question therefore is: Is it theoretically feasible to decouple compile-time type checking from compilation proper? Could we conceivably have v1.15-like-fast compilations, with the option to compile with type checking enabled, when and as often as desired?
4
josevalim
Creator of Elixir
Maybe that’s an option we can consider if the performance cost is too high but I would prefer to avoid that as much as possible, because then it would only be partially enforced.
8
D4no0
Just listened to the podcast, it is great and it tackles on the topic of this thread absolutely great.
I am wondering, will you still be able to run applications that would yield type errors or it will throw a compilation error? I know it doesn’t make much sense from the logical point of view, but I like how Roc allows to run programs that have some kind of errors in them.
0