[HN Gopher] The Design Principles of the Elixir Type System [pdf]
___________________________________________________________________
The Design Principles of the Elixir Type System [pdf]
Author : weatherlight
Score : 93 points
Date : 2023-06-13 15:40 UTC (1 days ago)
(HTM) web link (www.irif.fr)
(TXT) w3m dump (www.irif.fr)
| tolmasky wrote:
| 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?
|
| 1. Scroll down to "Girard's Paradox" here:
| https://en.wikipedia.org/wiki/System_U
| samth wrote:
| 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.
| weatherlight wrote:
| 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.
| weatherlight wrote:
| TLDR:
|
| 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).
| fritzo wrote:
| Great summary. Are you superhuman, or did you use an AI tool?
| What tool?
| weatherlight wrote:
| I use Chat GPT sometimes to reformat some of my rabbling
| longer posts. The bullet points are a giveaway.
| jefc1111 wrote:
| Thanks for this! Will be following a couple of the references
| wrt "gradual typing literature".
| haskellandchill wrote:
| 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
| lpgauth wrote:
| I'm not sure if I missed the announcement, but was there a
| timeline shared for a first alpha/beta release?
| agos wrote:
| no announcement yet, this was presented in April at ElixirConf
| EU, it's still in the exploratory phase, not even an alpha.
| fndex wrote:
| > 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.
| josevalim wrote:
| 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).
| fndex wrote:
| 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?
| josevalim wrote:
| 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.
| [deleted]
___________________________________________________________________
(page generated 2023-06-14 23:02 UTC)