Typing lists and tuples in Elixir

We have been working on a type system for the Elixir programming language . The type system provides sound gradual typing: it can safely interface static and dynamic code, and if the program type checks, it will not produce type errors at runtime. It is important to emphasize type errors . The type systems used at scale today do not guarantee the absense of any runtime errors, but only typing ones. Many programming languages error when accessing the “head” of an empty list, most languages raise on division