Is this type-system guaranteed to be sound? (Does type checking ensure no runtime type bugs?). Also, can it infer all the types if none of the types are actually annotated?
Also, what is the novelty about this new type system?
Also, what is the novelty about this new type system?
We present a gradual type system for Elixir, based on the framework of semantic subtyping [10, 19]. This framework, developed for and implemented by the CDuce programming language [3, 15], provides a type system centered on the use of settheoretic types (unions, intersections, negations) that satisfy the commutativity and distributivity properties of the corresponding set-theoretic operations [19]. The system is a polymorphic type system with local type inference, that is, functions are explicitly annotated with types that may contain type variables, but their applications do not require explicit instantiations: the system deduces the right instantiations of every type variable. It also features precise typing of pattern matching combined with type narrowing: the types of the capture variables of the pattern and of some variables of the matched expression are refined in the branches to take into account the results of pattern matching
A semi-mainstream BEAM language with static typing would be a huge boon. For those of us who have problems that BEAM fits really well, it's like saying Typescript doesn't matter because other statically typed languages exist. Which is really missing the point.
Type inference for set theoretic type systems is expensive and that has not changed. It is not surprising either: inference is harder or undecidable in more expressive type systems.
We address this by providing reconstruction based only on patterns, guards, and return types. Other than that, inference is not a major limitation to us, given you don’t need to declare types today anyway.