CDuce is interesting, an XML oriented functional programming language. That's where they draw semantic subtyping from, worth checking out for language nerds: https://www.cduce.org/design_features.html
Given that it appears that this type system has a universal type (or top type) in the form of the "term()" type in this paper, how does it avoid Girard's paradox[1]? Is it because the the rest of the type system isn't sufficiently expressive to run into it (by allowing dependent types or other higher-order polymorphism?). If so, does this mean it will be difficult to add such features?
The proposed type system for Elixir doesn't run into Girard's paradox because it doesn't allow for impredicative polymorphism, which is where the paradox arises. The type system is based on set-theoretic types and includes a top type (the term() type), but it doesn't allow for types to be quantified over all types. As for adding features like dependent types or higher-order polymorphism, these would increase the type system's complexity and could potentially lead to issues like Girard's paradox. The authors don't discuss adding such features, so it's unclear how difficult it would be.
Every type is inhabited in most type systems for general-purpose programming languages. For example, to inhabit a type T in Haskell syntax (the same approach works in basically any language):
f :: () -> T
f x = f x
myT = f ()
What this shows is that Haskell types are not sound as a logic, but that doesn't mean they aren't a fine type system.
> Each “key type” in a map type is either required or optional.
I wonder how that will work with Ecto schemas, or if it will work at all. Ecto Schemas do not specify required/optional keys, the Changesets do. But Changesets only exists in runtime. Loosing the ability to reuse the schema and have required/optional keys defined on the changesets would be a huge step back in my opinion, but pretty much all the type systems I know work that way.
The schema struct itself has all keys as required (the keys are always present). The map you receive on your changeset has all keys as optional because they can be missing (which we convert into a changeset error if the field is validated as required).
But how will it deal with nulls? For example, let's imagine I have a user schema. This schema has 3 fields, username, is_admin and admin_level. I can guarantee using changesets that when is_admin is true, admin_level must be non null. When is_admin is false, it can be null. admin_level would be always treated as nullable by the type system?
The type system _may_ allow the type of a field to be based on the value of another field. I will investigate and, if possible, we would have to figure out a syntax that makes this possible to express.
The type system they propose is based on the framework of semantic subtyping and includes several new features and improvements:
Semantic subtyping: The authors extend the semantic subtyping framework to fit Elixir/Erlang, particularly defining new function domains to account for the tight connection between Elixir/Erlang functions and their arity.
Guards: They develop a precise type system for analyzing guards in pattern matching.
Records and dictionaries: The authors propose a new typing discipline unifying records and dictionaries.
Dynamic type: They integrate the dynamic type into the type system, which is used to describe untyped parts of the code and how they interact with statically typed parts. This uses techniques from the gradual typing literature.
Strong arrows: The authors introduce a new gradual typing technique for typing functions that takes into account runtime type tests performed by the virtual machine or inserted by the programmer. This allows for more precise static types without modifying the source code compilation.
The implementation of the proposed type system for Elixir faces several challenges:
Performance and Usability: The authors are concerned about how the type system will perform on large code bases and how the community will interact with and use the type system. They plan to introduce the type system gradually to assess its performance impact and the quality of the reports it can generate in case of typing violations (Page 24).
Type Annotations: The introduction of typing must not require any modification to the syntax of Elixir expressions. The system must extract a maximum of type information from patterns and guards. Programmers who prefer a fully statically typed environment should be able to reduce the reliance on gradual types within their code by emitting warnings when dynamic() is used (Page 21).
Structs: The second milestone is to introduce type annotations only in structs, which are named and statically-defined closed record types. By propagating types from structs and their fields throughout the program, they aim to increase the type system’s ability to find errors (Page 24).
Function Annotations: The third milestone is to introduce the $-prefixed type annotations for functions, with no or very limited type reconstruction. Users can annotate their code with types, but any untyped parameter will be assumed to be of the dynamic() type (Page 24).
Row Polymorphism: To type functions operating on maps, row polymorphism is needed, but extending semantic subtyping with it is an open problem the authors are working on. They also plan to study how to remove the constraint that key-types must be chosen among a predefined set of types (Pages 25-26).
Message-passing: Typing the concurrency constructs and the actor model of Elixir is an obvious next step. Elixir's concurrency and distribution system is based on message-passing between lightweight threads called processes (Page 26).
