Oh, I didn’t mean inline annotations vs not.
In that example of “typespecs can’t negate, only union”… can TypeScript do that? If not, what’s the big benefit to it?
cjbottaro
benwilson512
Author of Craft GraphQL APIs in Elixir with Absinthe
An example from one of the linked papers: https://www.irif.fr/~gc/papers/set-theoretic-types-2022.pdf
Another practical example involves using types to model states. You can have functions that work on “all states except state X and Y”.
Beyond that, it ends up being super important for functions that have multiple clauses. For this I simply recommend reading the papers, they highlight all of this, I’d just be repeating them verbatim here.
My Future with Elixir: set-theoretic types - The Elixir programming language see the " Why set-theoretic types?" section.
2
wanton7
That kind of depends on your tsconfig, I mean is it opt-in or opt-out. If you have strict or noImplicitAny etc. set then you are opt-out.
0
adw632
Just thinking out loud here playing devils advocate with myself..
If you have a function input who’s type cannot be proven to match a more restrictive type specification then the compiler could warn about this, perhaps even emit an error.
Those cases can be handled using case expressions to santise the inputs or alternatively could be silenced by defining a more generic function variant that has less restrictive types and perhaps raising an error.
Only when you do not have sufficient function variants that collectively cover all of the implied types based on caller inputs should that be an actual compiler error.
Seems reasonable…
The described “fix” above of using less restrictive function variants could potentially avoid a lot of case expressions and leverage the language function pattern matching, but this is really only applicable for modules you directly control.
.. and now I can see this driving idioms, such as developers creating defensive “catch all” functions just to avoid type errors or being forced to write lots of case expressions.
… and potentially dealing with function input santisation using module delegates to keep the compiler quiet for modules I don’t control.
… but still having almost identical runtime behaviour of raising an exception and crashing on unsupported inputs.
The only difference I can see in the approaches above is where you sanitise, at the caller or at the callee, and elixir pattern matching works really well for the latter.
There seems to be an unresolved tension between “let it crash” when function pattern matching fails (which is something I love about the language because I can code for the happy path) and the potentially new need to silence the compiler through manual sanitising of inputs, essentuallycoding for the sad path at either caller or callee (or even more madeningly potentially both once the coding standards committee have their way).
All this pushes the “sanitization” back into some form of hand rolled code to silence the compiler, with basically the same runtime effect and overall less developer and runtime efficiency before a type system existed.
How much do we really gain other than a lot more typing and overhead when the new idioms for keeping the compiler happy become “best practice”?
The coding standards committee of do gooders will not accept code with warnings, and if there is an option for warnings to be treated as errors, the nannys will demand it, entrenching manual santisation practices further.
All said, rather than me being happy coding mostly the happy path I will be unhappy coding the sad paths just to keep the compiler happy, only to end up raising exceptions to still “please crash” on bad parameters that don’t match expectations.
I will also express some caution, and suggest the type system to be “advice only” because taking the path of treating them as compiler warnings and errors means the nanny coding committees will undoubtedly drive the kind of behaviour and idioms like I have described above.
What I would really value in a type system is identifying opportunities where function argument types and return values can be expressed more restrictively but are not, to drive tighter specifications from the bottom up. This would suggest that “catch all” functions variants are bad for detecting programmer mistakes (and are a bad idiom for addressing compiler errors) and the strategy for fixing a type error should be to drive more restrictive types up the call chain with case expressions used at the boundary/external interface layer.
1
josevalim
Creator of Elixir
Elixir is a functional programming language, JavaScript is object-oriented. While they are both dynamic, Elixir is more assertive with patterns and guards, JS is more polymorphic. The deeper you dig, the larger the differences. We should look at TypeScript for ideas, but copying probably won’t make sense.
In any case, you are talking about two distinct things here. One is syntax (which I am not much concerned about at the moment). The other is semantics. TypeScript does include unions and intersections (Racket as well) but TS does not include negations. Unions use the known | operator, intersections use &, which I dislike. Even then, they are not fully set-theoretic, and there is a technical paper that explains things you can model with full-set theoretic types and you cannot in Racket/TypeScript.
9
derpycoder
How will generics be handled in Set Theoretic type system?
$ any except nil -> string or exception
def to_str(num), do: ...
def to_str(atom), do: ...
...
Or we simply omit the type defs?
Is it possible to even have something like the above imaginary syntax?
wanton7
Original post contains link to a page that explains things and has links to videos and podcast. Maybe in couple of those videos it’s explained that plan is to support multiple type declaration lines per function like
$ types
$ types
So you can create one line per function pattern match etc.
Sorc96
The design principles document mentions generics, and I think Jose talked about them in his talk.
An example from the document:
$ ((a -> boolean()) , [a]) -> [a] when a: term()
def filter(fun, []), do: []
def filter(fun, [h | t]) do
if fun.(h), do: [h | filter(fun, t)], else: filter(fun, t)
end
stevensonmt
I’m not certain but I think this might be a place where the dynamic() type is used. Though if you really need the negation maybe term() and not null() or something would be more likely.
EDIT:
Oh nevermind, I see the reply above mine is more likely correct with respect to generics.
ityonemo
so I’ve thought about this a lot and it turns out even using dynamic() or when: doesn’t really work for certain cases. Wrapped Enum.reduce is the big one. The “right thing to do” is to allow the module author to embed a custom type-transforming lambda into the module attributes, this is a planned feature in selectrix.
https://github.com/ityonemo/selectrix/issues/28#issuecomment-716645458