Wait, the strong arrow stuff is basically what I was just talking about… oh boy. I think I’m out for the day 
But ya, that is crazy exciting.
sodapopcan
0
billylanchantin
Great talk! I keep meaning to read that paper…
One thing I was wondering: will strong arrows have a syntax? I (think I) get that they differentiate these two cases:
$ integer() -> integer()
def negate_weak(int), do: -int
$ integer() -> integer()
def negate_strong(int) when is_integer(int), do: -int
negate_weak fails to be “strongly arrowed” because it accepts arguments from the negation of its domain. E.g. negate(2.0) works just fine even though 2.0 isn’t of type integer, but negate_strong(2.0) would fail because of the guard.
But is this property implicit? Like if I annotate a function with a type, is its strong-arrowedness known only to the compiler? Or can I opt in/out of it with syntax, e.g.:
$ integer() -> integer() # $ for weak arrow
def negate_weak(int), do: -int
$$ integer() -> integer() # $$ for strong arrow
def negate_strong(int) when is_integer(int), do: -int
5
D4no0
I think it is implicit and is kind of a distinction between runtime constructs guarantees (like guards) and the new spec.
I think the whole reasoning behind this system is the fact that spec errors will not stop execution of program, in the same way dialyzer works, so if the guards were not to be integrated with the spec system, there would be invariant at runtime witch defeats the whole propose of type-checking.
1
LostKobrakai
No, not a syntax on the type notation. By my understanding what makes something a strong arrow function is what it does/is expected to do at runtime based on the used guards on the function. So you can opt in/out by adding/removing guards.
7
zachallaun
It’s obviously too early to know, but my guess is that, when function type annotations are supported, there will be an opt-in way get a warning when you write an explicit type annotation that doesn’t result in a strong arrow.
0
JEG2
Author of Designing Elixir Systems with OTP
adw632
I initially thought the same but there is very good reason to not specify annotions for return types.
The Elixir types paper on page 17 suggests that return type annotations should leave it the compiler function body proofs and guards so that we benefit from gradual typing.
Therefore, as a good programming practice it is better to leave the system to deduce the return types of all functions whenever gradual typing is used, by systematically using the underscore _ for return types, since an explicit return type may hinder the propagation of dynamic().
It’s the guards that make it a strong arrow that the Elixir compiler will use to guarantee the return type is within the domain
If you read page 17 it explains how the type system can do a better job by permitting dynamic to flow but using intersections of types. In Jose’s talk he mentioned his t-shirt colour to help explain the concept of “gray and any colour”.
I am optimistic that Elixir will get the balance right and look forward to it landing in the compiler, and also the arrival of types on structs.
2
zachallaun
I don’t think these things are at odds: the return type can be _ and the type can still be a strong-arrow.
2
josevalim
Creator of Elixir
Generally speaking, the more expressive a type system, the harder or more expensive it is to have full inference. If a language chooses to have performant type inference for all of its valid programs, then it often ends up with a type system that rejects more programs. A classic example in Haskell is (\x -> x x) (\y -> y) which is not valid because inference is undecidable (although iirc you can write that with some extensions and explicit type annotations).
I chose to accept more programs instead of full-blown type inference early on in our journey for three reasons:
-
We must avoid breaking changes (i.e. rejecting valid programs today)
-
If you don’t want to write the types, you can already not write the types today (and strong arrows/type inference from patterns and guards do their best to find errors)
-
Users of languages with type inference often recommend writing the types anyways (at least for public functions, private functions can make use of other techniques such as inlining to find errors)
I believe there will be a paper at POPL 2023 on type inference of set-theoretic types which will go into more details. However, it will be too expensive to make it part of the compiler. The types it infers though are incredibly precise. For example, imagine you have a list of integers and strings, and you want to get only integers:
Enum.filter(list_of_ints_and_strs, &is_integer/1) #=> [1, 23, 56, ...]
In most programming languages, filter has the type: [a], (a -> boolean()) -> [a], which means both incoming and outgoing list still has the type [integer() or string()], even if you keep only integers. However, with set theoretic types, we could get (and infer) the type:
[a or b], (a -> true) and (b -> false) -> [a]
Which in our example it would instantiate:
[integer() or binary()], (integer() -> true) and (binary() -> false) -> [integer()]
And therefore that the type system knows you removed all strings from the list. Being this precise has a high cost during inference (and we want to be precise!). At best, we could be able to use it as an explicit command like “what is the signature for this function” but not as part of compilation.
One last note: a type system with unions and intersections do not necessarily make it a set-theoretic type system. To be set-theoretic the foundation of the type system must all be based on set semantics. You can implement set operations in other ways.
16
josevalim
Creator of Elixir
That’s an excellent question and I ask myself the same. I believe we do want to provide mechanisms for the developers to know and/or enforce if arrows are strong or not, but it is yet unclear what those mechanisms should be.
12