Valim Readies Native Set-Theoretic Type System for Elixir Compiler

Code Sync

Set-theoretic types allow Elixir to enforce static compile-time safety and exhaustiveness across legacy dynamic code without altering the underlying runtime.

AI-assisted summary of Bringing Types to Elixir by Giuseppe Castagna and Guillaume Duboc | ElixirConf EU 2023 — original source. Check the original for full context.

Source published: 2023-10-23

Key ideas

A set-theoretic type system for Elixir has been developed through 1.5 years of PhD research under Giuseppe Castagna and José Valim, designed to provide ahead-of-time static analysis natively within the Elixir compiler. (0:25)
The framework models types literally as sets of values, utilizing unions, intersections, singletons, and negation types to capture multi-clause function contracts and pattern matching without false positives. (2:20)
Gradual typing is addressed using a novel 'strong function' classification that guarantees type soundness at dynamic boundaries by verifying that inputs outside a domain either fail at runtime or evaluate within the declared codomain. (19:17)
Developer adoption will prioritize typing patterns, guards, and struct definitions first, while legacy Erlang typespecs will continue to coexist alongside the new compiler-integrated type system. (28:47)

Detailed notes

## Background This presentation was published on YouTube by Code Sync on October 23, 2023, featuring a talk delivered at ElixirConf EU 2023. According to the page description, speaker Guillaume Duboc discusses the design of a set-theoretic type system tailored for Elixir, exploring how it catches common bugs, improves code quality feedback, and uniquely fits the language's semantics.

## TL;DR Guillaume Duboc presents the culmination of eighteen months of PhD research supervised by Giuseppe Castagna and José Valim to introduce set-theoretic static typing to Elixir. The presentation outlines core mechanisms such as function intersections, singleton types, complement/negation types, parametric polymorphism, and extended protocol composition. It demonstrates how pattern matching and map access rules provide rich typing context for ahead-of-time analysis, while introducing novel 'strong function types' and dynamic intersections to enable sound gradual typing. During the Q&A, Valim and Castagna join Duboc to unpack the mathematical necessity of negation for subtyping, early adoption paths via struct annotations, and the immense theoretical effort required to formalize Elixir map subtyping.

## Atmosphere & style The presentation carries an atmosphere of intellectual excitement and collaborative academic rigor balanced by practical software engineering realism. Guillaume Duboc delivers a clean, focused, and pedagogical walkthrough of complex type theory, while the dynamic shifts into a relaxed, good-humored camaraderie during the Q&A as José Valim and Giuseppe Castagna jump in to add color and field tough theoretical queries. Watching the session feels like witnessing a pivotal milestone in Elixir's evolution, where deep formal mathematics meets real-world developer ergonomics amidst enthusiastic audience engagement and shared relief over surviving marathon design meetings on map types.

## Bulletin - [00:25](https://www.youtube.com/watch?v=gJJH7a2J9O8&t=25s) A set-theoretic type system for Elixir has been developed through 1.5 years of PhD research under Giuseppe Castagna and José Valim, designed to provide ahead-of-time static analysis natively within the Elixir compiler. - [02:20](https://www.youtube.com/watch?v=gJJH7a2J9O8&t=140s) The framework models types literally as sets of values, utilizing unions, intersections, singletons, and negation types to capture multi-clause function contracts and pattern matching without false positives. - [19:17](https://www.youtube.com/watch?v=gJJH7a2J9O8&t=1157s) Gradual typing is addressed using a novel 'strong function' classification that guarantees type soundness at dynamic boundaries by verifying that inputs outside a domain either fail at runtime or evaluate within the declared codomain. - [28:47](https://www.youtube.com/watch?v=gJJH7a2J9O8&t=1727s) Developer adoption will prioritize typing patterns, guards, and struct definitions first, while legacy Erlang typespecs will continue to coexist alongside the new compiler-integrated type system.

## Key takeaways - [00:25](https://www.youtube.com/watch?v=gJJH7a2J9O8&t=25s) Existing Elixir typespecs and Dialyzer act primarily as external documentation tools, whereas the new system introduces native compile-time static type checking. - [02:20](https://www.youtube.com/watch?v=gJJH7a2J9O8&t=140s) Naive union types destroy return precision across multi-clause functions, requiring function intersection types (`and`) to track specific input-to-output relationships. - [05:19](https://www.youtube.com/watch?v=gJJH7a2J9O8&t=319s) Negation types allow concise description of complement sets, solving the impractical requirement of enumerating unbounded sets of atoms or terms in truthy-coalescing operations. - [25:50](https://www.youtube.com/watch?v=gJJH7a2J9O8&t=1550s) Under set-theoretic subtyping, testing if S is a subtype of T reduces algorithmically to checking whether the intersection of S and the negation of T is empty (S ∩ ¬T = ∅). - [09:09](https://www.youtube.com/watch?v=gJJH7a2J9O8&t=549s) The type system upgrades Elixir protocols by turning protocol types into exact unions of conforming types, allowing element parameterization and compositional intersections like Traversable. - [12:56](https://www.youtube.com/watch?v=gJJH7a2J9O8&t=776s) Pattern matching in function clauses and case statements supplies deep structural information, allowing the compiler to detect non-exhaustive matches and dead code clauses. - [16:09](https://www.youtube.com/watch?v=gJJH7a2J9O8&t=969s) With return type deduction (`result -> _`), the compiler statically infers output types across all pattern-matched branches without requiring explicit return annotations. - [16:09](https://www.youtube.com/watch?v=gJJH7a2J9O8&t=969s) Map access syntax is formally partitioned: dot notation requires guaranteed static field presence, whereas bracket notation returns a union with nil for potentially absent keys. - [19:17](https://www.youtube.com/watch?v=gJJH7a2J9O8&t=1157s) Unannotated dynamic code returns an intersection of the inferred bounds and `dynamic` (`(integer or boolean) and dynamic`), permitting flexible usage without generating false positives. - [28:47](https://www.youtube.com/watch?v=gJJH7a2J9O8&t=1727s) Structs are represented as maps with a fixed `__struct__` module tag atom, enabling them to fit cleanly into existing map typing semantics. - [28:47](https://www.youtube.com/watch?v=gJJH7a2J9O8&t=1727s) The initial user-facing rollout will focus on typing patterns, guards, and struct definitions before requiring manual annotations on general functions. - [38:32](https://www.youtube.com/watch?v=gJJH7a2J9O8&t=2312s) Formalizing open map typing with key exclusions was the most mathematically complex aspect of the project, requiring extensions to existing academic type theory.

## Detailed walkthrough ### [00:25](https://www.youtube.com/watch?v=gJJH7a2J9O8&t=25s) Project Genesis and the Motivation for Static Typing in Elixir

Guillaume Duboc opens the presentation by introducing the fruits of his PhD research, conducted under the joint supervision of type systems expert Giuseppe Castagna and Elixir’s creator, José Valim. The initiative began two years prior through email exchanges between Castagna and Valim, who realized that bringing formal type theory to Elixir required dedicated academic horsepower. As Duboc recounts, “This project was initiated two years ago during mail exchanges between José and Giuseppe when they decided to bring on a PhD candidate to help realize their ideas, and now after one year and a half of work I'm super excited to present you the type system that we've designed for Elixir.” The primary objective of the talk is to demonstrate the system's capabilities and show how it materially elevates the Elixir developer experience.

Addressing the obvious question of why Elixir needs types, Duboc acknowledges that Elixir already features dynamic runtime type checks. Developers can write guard clauses and runtime tests to inspect inputs, but because these checks occur exclusively while code is executing, defects are often uncovered far too late. Similarly, while Erlang-style typespecs exist, Elixir utilizes them primarily for documentation purposes. Although third-party tools such as Dialyzer can consume typespecs for external static analysis, the Elixir compiler itself has historically remained hands-off. Duboc explains the fundamental shift this project introduces: “And this is precisely what we want to do: we want to introduce a system of types that will be used before running your programs, before compilation, to analyze the behavior of your programs and detect bugs.” He illustrates this with a straightforward bug: an invalid expression where a boolean negation operator is erroneously applied to an integer, which should immediately flag a compile-time type error blaming the addition operator.

- Project timeline: Conceived 2 years prior via email correspondence between José Valim and Giuseppe Castagna; developed through 1.5 years of PhD work by Guillaume Duboc. - Existing status quo: Dynamic type checks occur strictly at runtime; typespecs exist chiefly as documentation with minimal native compiler enforcement. - New paradigm: Ahead-of-time static type analysis executed prior to code compilation to catch bugs before execution.

---

[02:20](https://www.youtube.com/watch?v=gJJH7a2J9O8&t=140s) Function Contracts, Union Types, and the Need for Intersections

Duboc moves into how types serve as formal contracts governing the inputs and outputs of functions. He proposes an explicit type annotation syntax marked by a dollar sign (`$`). Starting with a simple toy function, `negate/1`, which manipulates an integer, an annotation `$ (integer()) -> integer()` guarantees that passing an integer yields an integer. When invoked inside another annotated function like `subtract/2`—typed as `$ (integer(), integer()) -> integer()`—the code typechecks smoothly because `negate(b)` is guaranteed to evaluate to an integer.

Complications emerge, however, when `negate/1` is extended with multiple clauses to support additional data types such as booleans. If a developer attempts to update the contract using a naive union type: ```elixir $ (integer() or boolean()) -> (integer() or boolean()) def negate(x)... ``` Duboc notes: “And this is a union type, and it has to be understood in the most intuitive meaning that if a value has type T1 or T2, then it has either type T1 or type T2.” While mathematically straightforward, this union signature destroys precision. When `negate(b)` is called inside `subtract/2`, the typechecker only knows that the return value is `integer() or boolean()`. Because Elixir's numeric `+` operator cannot accept a boolean, `subtract/2` fails compilation with a type error—even though an integer argument passed to `negate/1` will always return an integer in practice.

To resolve this loss of precision, the type system introduces function type intersections using `and`: ```elixir $ ((integer()) -> integer()) and ((boolean()) -> boolean()) def negate(x)... ``` Duboc highlights the exact semantics: “Here this type annotation tells you that negate has both the type of functions that when given an integer value they return an integer, and when given a Boolean they return a Boolean.” Armed with this intersection, the typechecker can verify that passing an `integer()` into `negate/1` specifically produces an `integer()`, allowing `subtract/2` to typecheck without false positives.

---

[05:19](https://www.youtube.com/watch?v=gJJH7a2J9O8&t=319s) Singleton Types, Negation Types, and Expressiveness

Beyond basic unions and intersections, the type system includes set-theoretic primitives like singleton and negation types to precisely model idiomatic Elixir branching patterns. Duboc demonstrates this with a simple logical negation function, `logical_neg/1`. The first clause matches when the input is specifically the atom `false` or `nil`, returning `true`. This behavior is represented using singleton types—types that denote a single specific value: ```elixir $ (false or nil) -> true ``` To express the fallthrough clause—which accepts any value *except* `false` or `nil` and returns `false`—the system provides complement/negation types: ```elixir $ (not (false or nil)) -> false ``` Here, `not (false or nil)` encompasses the set of all Elixir terms excluding those two truthy-violating primitives.

Duboc then transitions to parametric polymorphism, where functions operate generically over arbitrary types using type variables. Demonstrating with `Enum.map/2`, the annotation defines list elements via type variable `a` and mapped outputs via `b`, quantified using a `where` clause: ```elixir $ (list(a), (a -> b)) -> list(b) where a: term, b: term ``` Upper bounds can be placed on type variables to constrain valid types, though here they default to `term`. Duboc emphasizes that the engine handles instantiation automatically: “The type system also performs local type inference, meaning that you do not have to specify what A and B are when you apply those functions.” If `map` is invoked over a list containing integers and booleans with a transformation function mapping numbers to integers, the compiler statically infers that the resulting value is `list(integer())`.

Furthermore, polymorphism and intersections compose naturally. For an Elixir short-circuiting logical OR helper taking two arguments: 1. If the first argument is `false or nil`, it returns the second argument unmodified, yielding type `(false or nil, a) -> a`. 2. If the first argument is truthy, it discards the second argument and returns the first, typed as `(b, term) -> b where b: not (false or nil)`. Intersecting both clauses forms an exact static specification of Elixir’s truthy-coalescing runtime behavior.

---

[09:09](https://www.youtube.com/watch?v=gJJH7a2J9O8&t=549s) Enhancing Protocols with Static Types: Parameterization and Composition

Duboc demonstrates that having this sophisticated static foundation directly enhances native Elixir language constructs, notably protocols: “Having this precise system of static types means that we can improve the usability of some of Elixir's features, and one of those is to improve the use of protocols.” In Elixir, protocols define polymorphic interfaces across data structures, such as `String.Chars` with its required `to_string/1` implementation. A critical concept is the protocol type representing all values implementing that protocol. In standard Elixir, the compiler automatically generates `String.Chars.t()`, but historically approximates it as `term()`. Under the set-theoretic engine, `String.Chars.t()` becomes an exact union of every type implementing the protocol—subsuming primitive types like integers and strings as well as user-defined structs.

This breakthrough unlocks two longstanding requests for protocols: 1. **Protocol Parameterization:** Specifying the inner types handled by a protocol container. For example, `Enum.into/2` takes an `Enumerable` and a `Collectable`, pushing items from one into the other. Its existing typespec lacks the capacity to describe element types. With the new system, `Enumerable.t(a)` designates an enumerable yielding elements of type `a`. Consequently, `into/2` is cleanly typed as: ```elixir $ (Enumerable.t(a), Collectable.t(b)) -> Collectable.t(a or b) ``` 2. **Protocol Composition:** Combining requirements through intersection types. Developers can declare an alias for data structures implementing multiple protocols simultaneously, such as a `Traversable.t(a)`: ```elixir @type traversable(a):: Enumerable.t(a) and Collectable.t(a) ```

```mermaid flowchart TD accTitle: Protocol Composition via Intersection accDescr: Diagram showing how Enumerable and Collectable protocols intersect to define Traversable.

subgraph Protocols ["Protocol Types"] E["Enumerable.t(a)"] C["Collectable.t(a)"] end

subgraph Composition ["Intersection Type"] T["Traversable.t(a)<br/>(Enumerable.t(a) and Collectable.t(a))"] end

subgraph Implementation ["Concrete Conforming Implementations"] S["IO.stream / Streams<br/>(Element specialized to String.t)"] end

E --> T C --> T T --> S ```

Duboc illustrates this with a small `echo` function that requires an argument supporting both enumeration and collection. By passing an `IO.stream`—which in Elixir satisfies both `Enumerable` and `Collectable`—to `echo`, developers get a fully typechecked, bidirectional read-and-write loop that mirrors input directly back to output. Because the elements inside the traversable can be specifically constrained to strings, operations on those elements are safely guaranteed by the compiler.

[12:56](https://www.youtube.com/watch?v=gJJH7a2J9O8&t=776s) Pattern Matching as a Rich Source of Type Information

Guillaume Duboc explains how set-theoretic intersections and parametric types can type check complex patterns, such as a read/write loop that capitalizes strings passed across protocols. A central challenge in designing a type system for Elixir is accounting for its ubiquitous pattern-matching mechanism, which appears in identical semantics across both top-level function clause definitions and `case` expressions. Pattern matching inherently contains a wealth of typing information that the type checker can extract directly to provide actionable compiler feedback and infer precise signatures.

To illustrate, Duboc presents a `result` type defined as a map containing an `:output` field. When `:output` is `:ok`, the map also defines a `:socket` field holding a value of type `socket`. Conversely, if `:output` is `:error`, the map defines a `:message` field holding either the atom `:timeout` or a 2-tuple containing the atom `:delay` and an integer.

```mermaid flowchart TD accTitle: Result Type Map Structure accDescr: Branching structure of the result map type showing output ok with socket versus output error with message variants.

subgraph ResultMap["result type"] FieldOutput["output::ok |:error"] end

subgraph OkBranch["When output is:ok"] SocketField["socket: socket"] end

subgraph ErrorBranch["When output is:error"] MessageField["message::timeout | {:delay, integer}"] end

ResultMap -->|":ok"| OkBranch ResultMap -->|":error"| ErrorBranch ```

When a developer writes a handler function matching on this structure, missing cases immediately produce static warnings:

- If a function clause only pattern matches on `output::ok` and `message::timeout`, it misses the error branch containing the `{:delay, integer}` tuple. Duboc emphasizes: “the type Checker would give you here A type warning sending saying that this pattern matching is uh non-exhaustive and it would output you it would compute for you the precise type of the values that escape your pattern matching in all cases.” - If an author covers the valid branches and then appends an extra clause attempting to handle a socket when one is present, the type system detects that the prior clause already exhausted that condition. The compiler flags this as an unused branch, highlighting the exact clause that will never be reached at runtime.

[16:09](https://www.youtube.com/watch?v=gJJH7a2J9O8&t=969s) Return Type Inference and Map Access Typing

Because pattern matching yields such high-fidelity data, the type system can infer exact return types without requiring manual annotations for every clause. Duboc highlights the syntax `result -> _`, which specifies only the function's input type while directing the type checker to calculate the output type automatically:

```mermaid flowchart LR accTitle: Pattern Matching Return Type Deduction accDescr: How matching clauses map to inferred return types, culminating in a union or intersection type.

subgraph InputClauses["Clauses"] C1["Clause 1: output is:ok"] C2["Clause 2: message is:timeout"] C3["Clause 3: rest of values"] end

subgraph InferredTypes["Clause Return Types"] R1["socket"] R2[":timeout"] R3["integer"] end

C1 --> R1 C2 --> R2 C3 --> R3

R1 --> FinalReturn["socket |:timeout | integer"] R2 --> FinalReturn R3 --> FinalReturn ```

- When the first clause matches `output::ok`, the returned socket is typed as `socket`. - When the second clause matches `message` as an atom, the type checker narrows it to the literal atom `:timeout`. - When the third clause catches the remaining case, the message must hold the `{:delay, integer}` tuple, typing the extracted second element directly as `integer`. - Aggregating all branches yields a return type of `socket |:timeout | integer`, or an even more granular intersection type describing exact return types for every valid sub-domain of the specified input.

Duboc then addresses the syntax and typing rules devised for Elixir maps. Consider a map type `T` where field `foo` must hold an atom, optional field `bar` holds an atom if defined, and any remaining atom keys map to integers:

[19:17](https://www.youtube.com/watch?v=gJJH7a2J9O8&t=1157s) Gradual Typing, Strong Functions, and Dynamic Intersections

Because Elixir is an established language with an extensive ecosystem, the type system cannot demand a total rewrite. As Duboc notes, “adding types to Elixir means that we have to take into account that a large part of the code is already written in fact all of the code is already written.” To solve this, the team adopts gradual typing via a `dynamic` type that can materialize as any concrete type at runtime, offering a relaxed soundness property: if a program expression $e$ has type `integer`, any value it successfully evaluates to at runtime will be an integer.

However, standard gradual typing (as found in TypeScript) allows `dynamic` to silently bypass annotations without enforcing safety at boundaries. Duboc contrasts two approaches using identity functions:

```mermaid flowchart TD accTitle: Weak vs Strong Function Types Under Dynamic Inputs accDescr: Contrasting id_weak (which propagates dynamic) against id_strong (which enforces an integer return).

subgraph WeakID["id_weak(dynamic)"] WIn["Input: dynamic"] --> WOut["Output: dynamic"] WNote["A boolean passed as dynamic passes through as boolean"] end

subgraph StrongID["id_strong(dynamic)"] SIn["Input: dynamic"] --> SCheck{"Runtime Guard / Type Check"} SCheck -->|"Matches Domain"| SOut["Output: integer"] SCheck -->|"Outside Domain"| SFail["Fails with Type Error"] end ```

Duboc defines this mechanism: “a strong function type is a function type that outside of its domain it's going to fail on the type error or it's going to give you a value which is inside of its co-domain and here the co-domain is integer for id_strong that makes us able to give a strong guarantee on the types that strong functions output and we do that without modifying at all the Elixir compilation because we take into account what is already being performed by The Elixir runtime.”

The type checker also handles unannotated code dynamically without producing unnecessary false positives. For an unannotated `negate` function taking `dynamic` and returning an integer or a boolean: - Simply typing the return as `integer | boolean` would break calling code like `subtract(negate(x), 5)`, because passing `integer | boolean` to `+` or `-` triggers an error. - Instead, the type checker infers the intersection `(integer | boolean) & dynamic`. - This relaxed intersection type signals that the return value is bounded by `integer | boolean`, but may be treated as dynamically compatible in numeric contexts. - Expressions like `subtract` type check successfully (failing at runtime if a boolean emerges), while provably invalid operations—such as passing the result to the string concatenation operator `<>`—are rejected at compile time.

[23:22](https://www.youtube.com/watch?v=gJJH7a2J9O8&t=1402s) Research Status, Compiler Roadmap, and Q&A

Duboc concludes by reviewing the project's milestones and outlining next steps: - A complete formalization of the set-theoretic type system for Elixir has been established, accompanied by dedicated syntax specifications. - A functional research prototype was implemented to validate and type-check the foundational examples. - The academic paper formalizing the type system is available in draft form on Duboc's academic webpage. - During the second semester, the team plans to transition from research to production by integrating the type checker directly into the upstream Elixir compiler.

Duboc offers attendees access to an experimental prototype to try out the examples, but warns that it is strictly a research artifact rather than a finished end-user tool. As applause breaks out, an organizer reminds the audience: “please do not share these URLs.” The session transitions to audience questions, with Duboc joking that he might redirect tough queries to his PhD advisor, Giuseppe Castagna. The first question from the floor focuses on the decision-making behind adding negation types versus requiring explicit type definitions.

[25:50](https://www.youtube.com/watch?v=gJJH7a2J9O8&t=1550s) The Role of Negation and Set-Theoretic Foundations

```mermaid flowchart TD accTitle: Set-Theoretic Typing Operations accDescr: Visualizing union, intersection, and negation operations used to express types and compute subtyping via emptiness checks.

subgraph Types["Type Universe"] T1["Type S"] T2["Type T"] end

subgraph Operations["Set Operations"] Union["S ∪ T (Union)"] Intersect["S ∩ T (Intersection)"] Negate["¬T (Negation: Values not in T)"] end

subgraph Subtyping["Subtyping Algorithm"] EmptyCheck["S ∩ ¬T = ∅?"] Result["S is a subtype of T (S <: T)"] end

T1 --> Intersect T2 --> Negate Intersect --> EmptyCheck Negate --> Intersect EmptyCheck --> Result ```

Responding to an audience inquiry regarding allowed versus disallowed inputs and return values, Guillaume Duboc explains that negation types introduce powerful expressive capabilities into the language. A negation type allows one to select any given type and represent strictly the set of values that do not belong to it. This directly mirrors the foundational mathematical theory underpinning the project: set-theoretic types. Under this framework, types are treated literally as sets of runtime values. For instance, the integer type represents the set of all integers ($0, 1, 2, 3, \dots$). Consequently, standard set operations can be applied directly to types: computing the intersection of two types ($T_1 \cap T_2$), taking their union ($T_1 \cup T_2$), or using negation to denote every value except those belonging to a specific set.

José Valim steps in to illustrate the practical necessity of negation by showing a slide example involving boolean logic and guards. When handling an expression like `not false`, attempting to express the resulting type positively without negation would require explicitly enumerating every alternative value that could possibly inhabit the system. Because atoms in the BEAM ecosystem are unbounded, a developer or compiler would be forced to enumerate an infinite list of atoms, followed by integers, lists, maps, and every other distinct data structure. As José puts it: “the negation is just very convenient because describing infinity would be hard.”

Giuseppe Castagna adds the theoretical perspective behind why negation is indispensable to the underlying algorithms. Relying on De Morgan's laws, intersections can be encoded through unions and negations. Furthermore, subtyping—verifying whether a type $S$ is contained within a type $T$—relies on an emptiness test: $S$ is a subtype of $T$ if and only if $S \cap \neg T = \emptyset$. Because the type-checking algorithms operate by systematically testing the emptiness of these derived sets, negation is fundamentally required from a formal point of view.

[28:47](https://www.youtube.com/watch?v=gJJH7a2J9O8&t=1727s) Struct Typing and Erlang Dependencies

Turning to how the proposed type system handles Elixir structs, an attendee asks whether there are concrete plans to type check them. Guillaume confirms that structs are already handled cleanly: beneath their syntax, Elixir structs are maps containing a special `__struct__` field tied to the module name of the struct. As a result, the type checker evaluates them as map types where the struct tag field is fixed to that specific struct atom.

Another audience member asks whether the system will be able to type check Erlang dependencies and analyze how external libraries influence types across an Elixir codebase. Guillaume clarifies that for foreign codebases without native type annotations, developers would likely need to author interface signatures manually to dictate expected input and return types. While the set-theoretic approach could theoretically apply to Erlang due to its shared execution runtime, Guillaume has not focused on Erlang directly. Establishing a reliable static type system in Elixir, however, lays the groundwork for writing foreign function interfaces that external dependencies can safely pass through.

José adds a clarifying parenthesis regarding the implementation roadmap for structs: - The team's immediate focus centers entirely on typing patterns and guards, as existing guards already supply rich type information without demanding code changes from users. - In patterns, struct declarations match on names, but individual struct fields often have implicit type requirements (e.g., expecting a user name to be a binary) that are not currently tracked through the compiler. - José notes: “most likely the first contact that we are going to have as developers with the new type system is going to be through typing structs.” - Developers will probably type struct definitions and their fields long before annotating functions directly.

[32:08](https://www.youtube.com/watch?v=gJJH7a2J9O8&t=1928s) Gradual Migration, Dialyzer Type Specs, and Tooling

Addressing how developers will migrate from existing `@spec` annotations, an attendee notes that tools like ElixirLS extract type information from `@type` and `@spec` tags, and asks what the gradual adoption strategy will be. Guillaume jokingly redirects the question: “I think this is the question for José.” After a round of laughter from the room, José acknowledges the handoff with “Nice one. Nicely dodged.”

José explains that legacy type specs and the new set-theoretic annotations are designed to coexist for a prolonged period, and potentially forever, because type specs remain essential for Erlang interoperability. However, the new system intends to provide far deeper integration directly inside the Elixir compiler and developer tooling. Highlighting work introduced in his keynote regarding code fragments and IDE tooling, José emphasizes that language server maintainers will eventually consume type diagnostics, completions, and inferences directly from core Elixir rather than relying on external heuristic tools. This will establish tighter feedback loops in both code editors and the interactive IEx shell.

[33:54](https://www.youtube.com/watch?v=gJJH7a2J9O8&t=2034s) Strong vs. Weak Function Types and Struct Invariants

A participant asks for clarification regarding the distinction between "weak" and "strong" function types, specifically querying how this mechanism interacts with structs when a function matches only on a struct module name rather than asserting guards across every individual struct field.

Guillaume initially explains that matching a struct pattern does produce a strong constraint because Elixir guarantees a structural check verifying that the incoming value is a map with the correct struct name. José then expands on the formal rule governing strong function types:

```mermaid flowchart LR accTitle: Strong Function Typing Rule accDescr: Evaluation flow showing how strong function types are verified by negating the domain and testing the function behavior.

Arg["Input Negates Domain (arg ∈ ¬Domain)"] --> Check{"Function Execution"} Check -->|"Fails / Raises"| Strong["Strong Function Type Verified"] Check -->|"Returns Codomain"| Strong Check -->|"Returns other dynamic value"| Weak["Weak Function Type"] ```

When evaluating a function signature $Domain \to Codomain$, the system examines what happens when an input value belongs to the negation of the domain ($\neg Domain$). If invoking the function with a value outside its declared domain either immediately raises an error or still returns a value within the declared $Codomain$, the signature is classified as strong. For instance, if an integer-expecting function raises when handed a boolean, it satisfies the strong condition. For structs, the function's strength depends on the operations performed inside: if an unvalidated field access subsequently triggers an exception when the type is violated, the function upholds the contract. José emphasizes that while this formal classification represents a major theoretical achievement for gradual typing, users should not feel burdened by it: “the concept of being strong it's like it's very important and we are very proud because it's like new theory for gradually typed languages but hope is that as developers we won't have to worry about it it's just going to be there.”

The session transitions to a question comparing Elixir's approach to TypeScript, where developers can construct union types derived from the keys or atoms of map structures. Guillaume begins answering by emphasizing that bringing dynamic key unions and precise map types into set-theoretic systems required significant extensions to existing academic type theory.

[38:32](https://www.youtube.com/watch?v=gJJH7a2J9O8&t=2312s) Typing Maps and the Challenges of Map Subtyping

An audience member follows up with a question regarding map types—specifically whether the proposed type system supports specifying the type of any atom except for designated keys like `:board` and `:field`. The speaker confirms that this refers to a very specific extension to the typing of Elixir maps, validating that the system indeed handles it: “The feature he's talking about is being able to specify the type of any other atom except board and field; this is a very specific extension to typing of maps, and yeah, it works.” For those interested in the formal theory behind this capability, the speaker mentions that the full technical details will appear in an upcoming research paper.

The discussion highlights just how much effort went into tackling maps compared to other Elixir language constructs. José Valim steps in to confirm the difficulty, asking, “Maps were actually the hardest part of the work so far, right? Do you agree?” Guillaume Duboc agrees, and José elaborates on the behind-the-scenes struggles of the design process, emphasizing that while the resulting rules might look deceptively clean, they were the product of intense debate: “We have that, but it was lots of lots of work; it doesn't look like that, but sometimes we'd have three, four hours meeting just talking about maps and how to type them.” With that final insight into the development process, the talk concludes to enthusiastic applause from the audience.

- **Open map key exclusions**: The type system can express map types with open atom keys while explicitly excluding specific known keys (such as excluding `:board` and `:field`). - **Forthcoming theoretical paper**: The formal semantics and rules for these map extensions are slated for publication in a future academic paper. - **Design complexity**: Formalizing map types in a set-theoretic framework required marathon three- to four-hour design meetings, proving to be the most demanding aspect of the typing work to date.

## Notable quotes > [19:17](https://www.youtube.com/watch?v=gJJH7a2J9O8&t=1157s) adding types to Elixir means that we have to take into account that a large part of the code is already written in fact all of the code is already written. — Guillaume Duboc

## Mentioned Giuseppe Castagna, Guillaume Duboc, José Valim, Elixir, Erlang, Dialyzer, TypeScript, ElixirLS, IEx, BEAM, ElixirConf EU

## Video description SAVE THE DATE FOR NEXT EDITION: 18-19 April 2024 📆 🔥 Check https://elixirconf.eu for details about ElixirConf EU 2024! 🔥 Call for Talks is open and you can also join the waiting list for access to limited Very Early Bird pricing - don't miss the cheapest tickets!

About the talk: Set-theoretic types, and how they are uniquely suited to represent Elixir programs: Guillaume Duboc discusses the potential benefits of a type system designed for Elixir, such as detecting common bugs and providing direct feedback on code quality.

Follow us on social: Twitter: https://twitter.com/ElixirConfEU and https://twitter.com/CodeSyncGlobal LinkedIn: https://www.linkedin.com/company/27159258 Facebook: https://www.facebook.com/CodeSyncGlobal

Looking for a unique learning experience? Attend the next Code Sync conference near you! See what's coming up at: https://codesync.global

[Source](https://www.youtube.com/watch?v=gJJH7a2J9O8)

中文简报

Valim筹备为Elixir编译器引入原生集合论类型系统集合论类型使Elixir能够在不改变底层运行时的情况下，对既有动态代码强制执行编译期静态安全与穷尽性检查。 Guillaume Duboc展示了在Giuseppe Castagna与José Valim指导下进行的一项长达18个月的博士研究成果，该研究旨在为Elixir引入集合论静态类型。演讲概述了函数交集、单例类型、补集/否定类型、参数多态性以及扩展协议组合等核心机制。内容展示了模式匹配与映射访问规则如何为预先分析提供丰富的类型上下文，同时介绍了新型的“强函数类型”与动态交集以实现健全的渐进类型。在问答环节中，Valim和Castagna与Duboc共同探讨了否定类型在子类型化中的数学必要性、通过结构体注解的早期采用路径，以及形式化Elixir映射子类型化所需的巨大理论工作量。在Giuseppe Castagna和José Valim指导下，经过为期1.5年的博士研究，Elixir集合论类型系统已开发完成，旨在Elixir编译器内原生提供预先静态分析。 (0:25) 该框架直接将类型建模为值的集合，利用并集、交集、单例和否定类型来刻画多子句函数契约与模式匹配，且不产生误报。 (2:20) 渐进类型通过一种新型的“强函数”分类来解决，该分类通过验证定义域之外的输入要么在运行时失败，要么在声明的值域内求值，从而在动态边界保证类型健全性。 (19:17) 开发者采用方面将优先对模式、守卫和结构体定义进行类型化，而传统的Erlang typespec将继续与全新的编译器集成类型系统共存。 (28:47)

Source quotes

[19:17] Guillaume Duboc: adding types to Elixir means that we have to take into account that a large part of the code is already written in fact all of the code is already written.

Original transcript

[0:00] [Music] [0:15] thank you [0:18] [Applause] [0:25] so hello everyone [0:28] um I'm very happy to present you the [0:30] outcomes of my PhD program conducted [0:33] under this provision of type systems [0:35] expert Jose pekastania and the renowned [0:38] Joseph Lim [0:39] this project was initiated two years ago [0:42] during mail exchanges between Jose and [0:45] Giuseppe when they decided to bring on a [0:48] PhD candidate to help realize their IDs [0:50] and now after one year and a half of [0:53] work I'm super excited to present you [0:56] the type system that we've designed for [0:58] elixir [0:59] this presentation [1:01] its goal would be to Showcase its [1:04] capabilities and the ways it can enhance [1:07] the Alexi developer experience [1:10] so let's dive in and first discuss why [1:13] types [1:14] so as you know Elixir already [1:17] adds us types in fact you can write a [1:20] function that checks the type of its [1:22] entity of its input but this [1:25] manipulation only occurs during runtime [1:27] which is why we talk of a dynamically [1:29] typed function [1:31] it is also possible to write type specs [1:34] but Elixir uses those mostly for [1:36] documentation and although it is [1:38] possible to pass them to external tools [1:40] to provide a code analysis elix elixit [1:43] itself does not make large use of it and [1:48] this is precisely what we want to do we [1:50] want to introduce a system of types that [1:53] will be used before running new programs [1:56] before completion to analyze the [1:58] behavior of your programs and detect [2:01] bugs [2:02] and speaking of bugs here's a simple [2:05] example of the kind of bug that we want [2:07] to catch this is a function that applies [2:09] a Boolean negation to something that is [2:13] always an integer and you would get a a [2:15] simple typer blaming the plus operator [2:18] here [2:20] in in general though [2:22] um you would want to use uh types to [2:26] annotate the behavior of your functions [2:29] and to act as contracts between the [2:32] input and the output that you function [2:34] that you functions produce so an example [2:37] of that would be this toy function [2:39] negate it manipulates integer and we [2:43] would want to enable the Syntax for [2:46] adding a type annotation of our over [2:48] this function this syntax with the [2:51] dollar sign is a type in addition and [2:53] what it tells you it does is that the [2:55] function definition that follows if you [2:57] you give it a value that has Type [2:59] integer it returns an integer now when [3:02] you use this function in another [3:04] annotated function such as subtract [3:07] which has The annotation that if you [3:10] give two integer arguments to this [3:12] function it returns an integer [3:15] well this function is well typed because [3:17] uh the negative B does have type integer [3:21] what happens though if you modify the [3:24] implementation of negate and if you add [3:26] more Clauses to handle other kind of [3:30] data types for example adding close for [3:33] booleans now means that you have to [3:36] update your type of notation and one [3:40] example of a type annotation that you [3:42] could write is the following one [3:44] this type of notation means that when [3:47] you give a value that is either an [3:49] integer or a Boolean to function negate [3:53] it returns you something that is either [3:55] an integer or Boolean and this is a [3:58] union type and it has to be understood [4:00] in the most intuitive meaning that if a [4:03] value as type T1 or T2 then it has [4:07] either type T1 or type T2 now though the [4:12] problem is that a function subtract [4:14] doesn't type check anymore [4:17] because you are giving to the plus [4:20] negative B which is an integer or a [4:24] Boolean so you get a type error here [4:26] which is informed tonight because if you [4:30] look at the implementation of negate if [4:33] you give an integer to negate you're [4:34] always going to get an integer back so [4:37] we want to be able to write [4:40] a type for negate that is precise enough [4:43] so that function subtract type checks [4:46] and we can do exactly this [4:49] using a type intersection [4:52] a type intersection of function types [4:54] and this is the type of notation that we [4:57] want to write for negate [5:01] here this type of Nation Station tells [5:04] you that negate has both the type of [5:07] functions that when given an integer [5:09] value they return an integer and when [5:12] given a Boolean they return a Boolean [5:15] and now subtract type checks [5:19] our type system also has other features [5:23] that make it quite expressive to type to [5:26] write a type of notation for your [5:28] functions for example here for this [5:30] example of a logical neck which is very [5:33] simple function [5:34] Its Behavior is that when you give an [5:37] input which is either the atom Falls [5:39] O'Neill you get true and you can write [5:41] exactly this type using Singleton types [5:45] which are types containing exactly one [5:47] value [5:48] here the false type in The annotation is [5:52] a type that represents exactly the atom [5:55] false and if you want to write a type [5:58] that describes the second Clause of this [6:00] function [6:01] whose behavior is that if you give it X [6:03] which can be any value except the atom [6:06] falls on nil you can write this too [6:09] using a negation type [6:11] here the type not false O'Neill is the [6:14] type of any value that is neither false [6:17] nor nil [6:20] a type system also allows you to write [6:24] polymorphic type annotations [6:26] so polymorphic functions they are [6:28] functions that can [6:30] do their work on many different types [6:33] and the map example is good example of [6:36] that and here's its implementational [6:38] lists and we can write this type of [6:41] notation for it so here [6:44] the leftmost type [6:46] is the type of lists with elements of [6:50] type A [6:51] and hey here is a type variable [6:54] so this type if we read it together it [6:58] is the type of lists with a it is a [7:01] function type which when you give it [7:03] lists with a elements and a function [7:06] from a elements to B elements you get [7:08] back list of B elements and the type [7:11] variable they are Quantified after the [7:14] type using this one syntax and we can [7:18] specify upper bounds on them [7:20] here the upper bound is just term [7:23] meaning that we do not restrict a but we [7:26] could write a precisely bound if we [7:28] wanted to restrict what a can be [7:31] yeah [7:31] the type system also performs local type [7:35] inference [7:36] meaning that you do not have to [7:39] specialize to to specify what A and B [7:43] are when you apply those functions for [7:45] example if you apply map to this list [7:49] that contains integers and booleans and [7:52] you apply it with a function that takes [7:54] a double and returns an integer [7:56] then the type Checker before running [7:59] your program before compilation we'll [8:01] see that this function application [8:03] returns a list of integers [8:07] we can also combine the two time type [8:11] intersections and polymorphism [8:15] say is an example of that with this [8:17] logical or function [8:20] so if you look at the behavior of [8:21] logical or it has two arguments and when [8:25] the first argument is either false [8:27] O'Neill [8:28] it returns you its second argument [8:30] meaning that the return type will be the [8:33] same as the as the second argument so if [8:36] you capture this type by variable a you [8:38] can write this exact type [8:41] now if you want to write a type that [8:43] describes the second close [8:45] you can see that this second close when [8:47] it receives the first argument which is [8:49] anything but false O'Neill it discards [8:53] its second argument and Returns the [8:55] first so you can write the following [8:57] type where B here [9:00] as an upper bar which is not false [9:03] O'Neill meaning that B can become any [9:05] type that doesn't contain fossil nil [9:09] so having this precise system of static [9:13] types means that we can improve the [9:16] usability of [9:18] other of some of Elixir features and one [9:21] of those is improve the use of use of [9:24] the of protocols [9:27] um so just a quick reminder protocols [9:30] they allow you to define a set of [9:32] operations to be defined on a certain [9:34] data type [9:35] and the string colors example is the [9:38] simplest example of that it mandates [9:40] that you implement the tostring function [9:43] and one essential type [9:45] when you work with protocols is the type [9:48] of all values [9:49] that Implement a certain protocol [9:51] and for string cars that would be string [9:54] cars dot T and in fact this type it is [9:58] automatically filled in by the Galaxy [9:59] compiler but currently It Is [10:03] approximated by term by any type but now [10:07] we can use a precise Union type to [10:10] represent exactly all the [10:13] the union the exact Union of all the [10:15] types that implement the tostring [10:17] protocol and that would include the base [10:19] type for which this is defined strings [10:22] and integers but also some con some [10:24] custom types that for which you would [10:26] Define tostring [10:29] having this feature enables us to solve [10:32] two issues of protocols one is how to [10:37] parametrize them can we pass a type to [10:40] parametrize the protocol in particular [10:42] for a specific use and if you look at [10:46] libraries that are defined on values [10:49] that Implement certain protocols such as [10:51] the function into this is its current [10:54] type spec [10:55] the into function it takes [10:58] a an enumerable [11:01] a collectible and it inserts the [11:04] elements of the color enumerable into [11:05] the collectible and currently you cannot [11:08] you do not have a way to specify what [11:11] the elements of those structures are but [11:13] now we can because numerable T of a [11:17] is the type of values that implement the [11:20] animal protocol and which contain [11:23] elements of type A that would be a list [11:26] of a elements for example [11:28] and now we can write a precise type [11:31] notation for the into function [11:34] which is the following one which tells [11:36] you that given an M normal containing a [11:39] elements a collectible containing B [11:42] elements you will get as a return [11:46] you will get returned some collectible [11:49] and its elements are either of type A or [11:52] of type B [11:53] using this and also intersection types [11:56] we can also do a composition of [11:59] protocols and let me show you an example [12:01] of that [12:03] you can Define the custom type of [12:05] traversables they are type of values [12:08] that Implement both protocols and which [12:11] contains elements of type A [12:13] and if you want it if you had to write a [12:17] function that needs values that [12:19] Implement both protocols such as this [12:21] little Eco function now you can write a [12:25] precise type annotation for it so now if [12:27] you apply equal to istream you have a [12:30] read and write Loop that you have type [12:33] checked a nice read and write Loop that [12:35] tells you back just what you said [12:37] because I stream because streams in [12:40] Elixir they Implement both enable and [12:42] the collectible protocol in fact if you [12:44] look at this example more closely we [12:47] have specialized the elements inside [12:49] that reversible To Be Strings [12:52] so we can easily add an operation on [12:56] strings to the function so that now we [12:58] have type checked and a read and write [13:01] Loop that will capitalize everything [13:04] that you that you give it and [13:07] this this is uh this is a good [13:10] application of both intersections and [13:13] parametric types for protocols [13:16] now one key issue in devising the type [13:21] system for Elixir was to handle its [13:24] powerful pattern matching mechanism [13:26] and the pattern matching it occurs both [13:29] in function definitions and in case [13:32] Expressions which is why those two the [13:35] function definitions are equivalent [13:38] in fact but the matching an Elixir it [13:40] gives us already a wealth of typing [13:43] information [13:44] and we can leverage that [13:47] to provide more precise types and to [13:50] give some good feedback on your code and [13:53] let me show you how so this result [13:56] type definition it defines result which [13:59] is a kind of map which has two Fields [14:03] defined [14:04] its first field is the field output [14:07] and if output is set to the OK atom then [14:11] there will be a second field which is [14:13] socket [14:14] which contains a value of type socket [14:17] and if the field is set to error then [14:20] you will have a message field defined [14:22] with inside either timeout or a double [14:26] with the atom delay and an integer [14:30] now if you write the function that [14:32] handles this kind of result value you [14:36] would write for example this one and you [14:39] would pattern match on what the values [14:42] inside of the fields are and here if you [14:47] pattern match on our output is okay and [14:51] then on our message when it is Timeout [14:54] what you see is that you are going to [14:57] miss the cases where the result is [15:00] something where the field is set to [15:03] error and you have a double [15:04] and the type Checker would give you here [15:07] A type warning sending saying that this [15:09] pattern matching is uh non-exhaustive [15:12] and it would output you it would compute [15:15] for you the precise type of the values [15:17] that escape your pattern matching in all [15:19] cases [15:22] similarly [15:24] if you were to change this code and now [15:27] correctly button matching okay then on [15:30] air [15:31] and if you were to write a third Clause [15:34] here that wants to do something when [15:36] there's a socket inside of your result [15:37] well this third Clause is already [15:41] matched by the first one [15:43] meaning that this is an unused branch [15:45] and you would get also a type warning [15:48] pointing out at the exact branch that is [15:51] never going to be considered never going [15:54] to be entered [15:57] this wealth of typing information inside [16:00] inside of pattern matching means that [16:02] the type Checker usually can compute the [16:05] exact type that one of your functions [16:07] will return [16:09] and here's how we can leverage that by [16:12] using this notation result to underscore [16:15] this is a way to say that [16:17] you just specify the input the input [16:20] type of your function and then [16:23] you led to the type Checker the goal of [16:25] computing the exact result type that you [16:28] get and here that would mean that [16:31] in the first close [16:33] the type Checker looks at our output [16:36] being matched to okay so it knows that [16:39] our socket is something of type socket [16:43] in the second close when you check that [16:46] our message is in the atom it means that [16:48] it is the timeout atom [16:51] and in the third clause which matches [16:54] the rest of the values it knows that [16:56] message must contain the Tuple so this [17:00] will be typed LM the second element of [17:03] our message will be typed as an integer [17:05] meaning that you get the return type [17:07] computed for this function as this Union [17:10] of all the types possible when [17:12] considering all of your branches in fact [17:14] the type Checker could infer the even [17:17] more precise intersection type that [17:20] follows and that X and that gives you [17:22] the exact [17:24] written type for every possible input [17:27] type as long as it is a subtype of the [17:30] one that you specified for the input [17:34] one key issue was also to divide device [17:37] away a syntax to to represent map types [17:43] and here's here's how we do it so this [17:46] is an example of type T which represents [17:49] a map which has a full field set to atom [17:55] it has an optional field bar set to an [17:58] atom if it is defined and then any other [18:01] atom field would be defined would have [18:04] to be defined to an integer [18:07] and here's how then we are going to type [18:09] check the access to this map to to your [18:13] program to M if it is of type t [18:18] m.fill will be typed with the type atom [18:22] but if you try to access the field bar [18:24] you would get the type error because the [18:27] dot access in Elixir means that the key [18:29] has to be defined inside of your map [18:32] this however another way to access Maps [18:35] who is field may be undefined and that's [18:37] the bracket notation and in that case we [18:40] would type [18:42] M bar with the type atom or nil because [18:45] you will get nil in the case where bar [18:48] isn't defined if you try to access any [18:50] other atom [18:52] such as other you would type it with the [18:55] type integer or nil because that follows [18:58] the type specification and then finally [19:01] if you try to access an integer field [19:04] this would be type with the type nil and [19:07] possibly you would get a warning a type [19:08] warning here because you're trying to [19:10] access a field that would never exist [19:15] so [19:17] adding types to Elixir means that we [19:20] have to take into account that a large [19:22] part of the code is already written in [19:25] fact all of the code is already written [19:26] and and [19:30] so to address that problem with the [19:33] strategy of gradual typing which means [19:36] it is a way to blend statically typed [19:38] and dynamically type code and for that [19:40] we use we introduce the dynamic type [19:43] which is a type that can become any of [19:46] the type at runtime [19:48] so we offer a relaxed type safety [19:51] guarantee that tells you that if some of [19:53] your program e that does some [19:55] computation as type integer then if this [19:58] program evaluates the value then this [20:01] value should be an integer [20:04] one issue with using Dynamic which has [20:08] been used for in popular languages such [20:10] as typescript is that the dynamic can go [20:15] through your type annotations and not [20:17] take them into account let's take [20:20] another example here with ID week which [20:22] is the identity function [20:24] here the this this [20:27] annotation is good right because if you [20:29] give an integer to ID week you get back [20:32] an integer and if you apply ID week to [20:35] something that is dynamic the only thing [20:37] you can say is that the return of this [20:39] function as type Dynamic 2 because you [20:41] could give a Boolean under the guise of [20:43] dynamic and you would get a Boolean [20:46] however if you look at this second [20:47] function ID is strong it is the same but [20:50] it it checks the input the type of its [20:53] input [20:54] meaning that now if you apply is strong [20:57] to something of dynamic [20:59] you know that if something is written it [21:02] will be an integer so we call that a [21:05] strong function type for ID strong and a [21:08] strong function type [21:09] is a function type that outside of its [21:12] domain it's going to fail on the type [21:14] error or it's going to give you a value [21:17] which is inside of its go domain and [21:20] here the code domain is [21:22] integer for I destroy that makes us able [21:27] to give a strong guarantee on the types [21:30] that strong functions output and we do [21:34] that without modifying at all the Alexa [21:36] compilation because we take into account [21:40] what is already being performed by The [21:42] Elixir runtime [21:44] in fact [21:45] or type Checker can do something more [21:48] specific if you give it if you look at [21:51] this function negate and you type check [21:54] it in a dynamic typing mode meaning that [21:57] you don't write an annotation so the its [22:01] input is assumed to be something of type [22:03] Dynamic well you could say that this [22:06] function checks its input [22:09] and it's always going to return [22:11] something that is that is either an [22:13] integer or Boolean [22:15] but if she did that then if you try to [22:18] apply this function inside of subtract [22:20] you get a type error possibly because [22:23] you gave something that is either an [22:25] integer or Boolean to Plus [22:26] well we don't want to do that in Dynamic [22:30] typing mode [22:31] so instead we give [22:34] as a result type for negate this more [22:36] precise type [22:37] this is integral Boolean intersected [22:40] with the dynamic type [22:42] which means that the function negate can [22:44] return something that [22:47] has to be lower either an integer or [22:50] Boolean but it could be always an [22:52] integer or it could be always a Boolean [22:54] and [22:56] this relaxed way of type checking allows [22:59] us to type check Subtract with type [23:01] integer knowing that if a Boolean is [23:04] given there you will get a clear type [23:06] error [23:07] however if you give the result of [23:09] negative 2 for example the concatenation [23:11] operator you will get the type error [23:14] because it is not possible that this [23:16] apple that this application [23:18] succeeds [23:20] so [23:22] to sum up what we've been doing [23:25] we've been working on the formalization [23:28] of complete type system for Elixir we've [23:30] developed we've defined a syntax that [23:33] have show and I've shown you a few [23:36] examples of that [23:37] we've also implemented a prototype to [23:40] type check all specific examples on [23:42] which we design on which we conducted [23:45] our research and as this presentation [23:48] ends we've now presented our design [23:50] choices to the community our next step [23:53] will be to publish the our approach [23:56] and uh in the second semester we'll work [23:59] on the implementation to bring that to [24:01] The Elixir compiler [24:03] if you're very interested in more [24:06] details you can rate you can find at my [24:10] academic page a draft for paper about [24:15] the galaxy type system and it will give [24:18] you much more explanations about [24:20] everything that I showed you in this [24:22] presentation [24:23] I also spoke of a prototype and if you [24:27] want you can play with it it is only for [24:30] the conference the people who come at [24:32] the conference it is very experimental [24:35] it is only to type check the examples [24:37] that we've been developing the research [24:39] on [24:40] and it is not something that is a user [24:45] product it is just if you're curious [24:47] about what we're doing you want to [24:48] interact with us and give us feedback [24:50] you can play with it [24:53] um [24:54] and that's all for me if you have any [24:57] clay any questions I'll take them and [24:59] possibly I'll redirect them to my PhD [25:02] advisor [25:11] [Applause] [25:19] remind people to not share the URL [25:22] please do not share these URLs [25:26] okay so unfortunately we don't have time [25:30] for Q a [25:31] no joking [25:34] okay who has any questions yeah raise [25:37] your hands okay I'm going to start from [25:38] closest to forests [25:43] I had a question about the negation type [25:45] specifically uh what was the decision [25:47] making around wanting to add those [25:48] versus being explicit about what types [25:50] are allowed versus ones that aren't [25:52] allowed in terms of return and input [25:56] so the the negation time you um [26:00] the negation type is something that is [26:02] even more expressive it is a new type [26:06] that allows you to take any type and say [26:09] I want only the values that are not at [26:12] all in this type [26:13] so if I understood your question [26:15] correctly uh [26:17] it is a because it is something that is [26:21] more recursive expressive and that also [26:23] it comes with the original theory that [26:26] we are using which is the idea of seeing [26:29] uh types as a sets meaning that if a [26:32] type is [26:35] um in in ID the set of all the values [26:38] that have this type like integer is the [26:41] set of all of zero one two three then [26:44] you can take two types and say I want [26:46] the intersection of this type T1 and T2 [26:49] you can say I want the union of these [26:53] two types T1 or T2 and you can say I [26:56] want any any value except the ones that [27:00] are in the inside of this type and Jose [27:02] do you want to add something to [27:05] or true [27:15] I have too many slides [27:20] yes [27:22] so in this case you can't you need the [27:27] negation because it will be impossible [27:29] to explicitly say everything else that [27:33] does not go there [27:34] yeah so in this case we have not false [27:37] so the question is like well maybe we [27:40] don't need not but not saying well [27:43] you're going to have all the atoms which [27:45] are infinite so you would have to list [27:47] all the atoms which are infinite and you [27:50] would have to list integer [27:53] um list map so the negation is just very [27:57] convenient because [27:59] uh describing Infinity would be hard [28:05] I can give the theoretical answer is [28:07] that we don't need intersection because [28:10] they are encoded by the Morgan laws with [28:13] Union and negation and do check [28:16] subtyping so when one type is containing [28:18] to the other well s is smaller than T if [28:21] s intersection note D is empty so all [28:25] our algorithms work checking the [28:27] emptiness of all these types so you need [28:30] also from a theoretical point of view [28:36] three answers for each question [28:41] Does this answer a question by the way [28:47] first of all for sharing your findings [28:49] really interesting I have a question [28:52] do you have any plan for type checking [28:56] regarding struct elixir structs [28:58] yes in fact struck scenarios in Elixir [29:02] there are maps so we already type check [29:05] them perfectly with a map type which as [29:08] the struct field defined to the name of [29:11] the of the struct [29:14] um [29:15] yes [29:16] [Laughter] [29:22] um do you want to go there no yeah [29:27] I think [29:30] okay uh hi I'd like to know how would [29:34] would it be able to also type check how [29:38] long dependencies sorry [29:40] um how long and all independence is so [29:43] you could also see how it how your [29:46] dependencies would influence your code [29:49] like the types how it would influence [29:52] your types to all independencies [29:56] um [29:56] well uh you're talking about uh adding [30:00] type signatures to some foreign code [30:02] right yes foreign libraries well in that [30:05] case uh I think you would have to write [30:09] um interfaces uh manually that specify [30:12] what kind of uh input that and written [30:15] you expect from those foreign interfaces [30:18] um about specifically type checking uh [30:21] Allen code well our work is elixir is [30:24] similar so Ellen so it it applies to it [30:27] but this is not something I've [30:30] specifically worked on but this is once [30:33] we once you have a static type system [30:35] those kind of things become possible to [30:38] write interfaces and take them into [30:40] account [30:43] yeah just uh one parenthesis on this [30:45] truck uh when it comes to the [30:47] implementation our mindset right now is [30:51] to first start working with uh patterns [30:54] and guards because sgium said there's a [30:57] lot of information in guards already we [31:00] know we can extract a lot of information [31:02] from that but the other thing that we [31:04] have in patterns are structs and structs [31:08] usually match on the name but all the [31:11] struct fields they may have type [31:13] information so like the user name is [31:16] going to be a binary and that [31:18] information right now is not carried [31:21] through the system so it may change but [31:24] right now our [31:26] while we are thinking when it comes to [31:28] the implementation is that we are going [31:30] to focus on patterns and guards and then [31:33] the next thing we are actually going to [31:35] type and when we start typing patterns [31:37] and words you won't have to change our [31:39] code it's just going to work because the [31:40] patterns and guards are there and most [31:43] likely the first Contact that we are [31:45] going to have as developers with the new [31:48] type system is going to be fruit type [31:50] instructs so it's likely that you're [31:53] going to be typing a struct and adding [31:55] types to struct Fields before you add [31:58] types to functions that's the mindset [32:01] right now but it will see how it goes [32:04] but that's [32:05] yeah where we are [32:08] all right I think we have time for one [32:10] final question and see a gazillion hands [32:12] up yeah sorry so I'm just going to [32:16] choose the closest one I'm sorry so [32:18] I'm sorry overrun even yeah but we are [32:21] officially already okay let's see let's [32:23] see how it goes so you raised your hand [32:26] so if I'm not wrong current currently [32:30] Elixir LS can get some typing [32:32] information from type specs and so [32:37] introducing this new syntax can be [32:39] gradual uh like I had the new new things [32:43] to my Elixir code base but what is the [32:46] strategy of migrating from Thai spec [32:48] annotations to those new annotations [32:52] I think this is the question for Jose [32:55] nice one nicely dodged [32:59] yeah so they will both coexist [33:02] um for a while potentially forever [33:05] because I don't think type specs are [33:07] getting away are going anywhere because [33:09] of verling so they are going to coexist [33:12] but the idea is that [33:14] um because if this works out right it's [33:17] important to put that condition if like [33:19] it's working out so far but there's [33:21] still a lot of work but if this works [33:23] out it's going to be much more [33:24] integrated with Elixir and today during [33:27] my keynote I said we have like the code [33:29] fragment which is like we are working on [33:31] the tooling for IDs so when it comes to [33:34] the Elixir language server folks to [33:36] implement those features it's all going [33:38] to be coming directly from Elixir and [33:41] will be more integrated in this aspect [33:43] or try to be more integrated in IEX and [33:46] all this kind of stuff and try to have [33:48] more visibility uh of the types to the [33:51] developer [33:54] all right so to make it a little bit [33:56] more fair I'm going to walk this side [33:58] all the way back [34:01] so [34:04] foreign [34:06] so when it comes to uh struct and you [34:10] mentioned weak versus strong was it a [34:12] signature so what what was the word you [34:15] used [34:16] strong strong function types strong [34:18] versus weak function types when it comes [34:20] to uh from the example at least you uh [34:24] you showed that for the function type to [34:26] be strong you had to uh match with a [34:28] guard on every single sort of condition [34:30] on the on the type [34:32] um how does that intersect with or [34:34] interact with structs where a lot of the [34:36] time you only match on say the the name [34:38] of the struct and then a lot of sort of [34:41] information comes in through that [34:43] theoretically but you don't actually [34:46] um match [34:48] with a guard because [34:50] I I don't know because then it would [34:51] have to sort of check the types that get [34:53] set in destruct and when they get pulled [34:55] out or like I don't know that was a [34:57] general question but did you understand [34:59] the gist of it yes yeah yeah definitely [35:03] um so your question is if we pattern [35:05] match on the strict is that strong [35:09] well yeah it is because uh I think that [35:12] Elixir is then going to uh to [35:15] specifically check if the struct of this [35:18] map that you get as input which is [35:19] tracked is defined and possibly it could [35:22] check some more if the strict definition [35:25] allows to specify some type in inside of [35:28] it but I guess this would be an [35:32] extension uh something different [35:34] so [35:37] just come on [35:40] it's all right [35:42] yeah so so the idea and you may have to [35:47] correct me [35:48] um but the idea we are we are going to [35:50] automatically check if uh where are you [35:52] hence yes uh we are going to [35:54] automatically check if the function is [35:57] strong or not so for example if you have [35:59] a struct and you don't have any guard on [36:02] the struct fields so the the rule for uh [36:05] strong functions it's clear is that so [36:07] the if we if you look at the arrow the [36:10] domain is the left side of the arrow and [36:12] then call domain is the right side of [36:14] the of the arrow so if we magic yeah [36:18] yeah so if we pass something that is not [36:22] the domain if we negate the domain and [36:25] it either raises [36:27] or Returns the code domain so looking at [36:30] this example here at the bottom so let's [36:31] say well what happens if I uh I I uh I [36:36] do Strong's damage yeah I did strong so [36:38] if you pass something that is not [36:40] integer like a Boolean does it return an [36:44] integer fail in this case it's going to [36:45] fail so it's like oh it's a strong [36:47] function the type check is going to [36:48] check that first so in the instruct case [36:50] it may be or may not be strong because [36:53] depending on the operations that you are [36:55] doing so for example dependent [36:57] operations that you are doing we are [36:58] going to figure out oh okay yeah we can [37:00] see that this rule is applied we are we [37:04] are passing something that is not a [37:05] struck like if we say like the field is [37:08] a binary and then when we type check it [37:10] with the field not being a binary it [37:13] raises they're like oh okay yeah it's [37:14] this strong but yeah so the idea is that [37:16] this is not the the concept of being [37:19] strong it's like it's very uh important [37:22] and we are very proud because it's like [37:24] new theory for gradually typed languages [37:26] but hope is that as developers we won't [37:29] have to worry about it it's just going [37:32] to be there and it means the type system [37:34] is going to do what we expect even when [37:37] we are intersecting static and and [37:39] dynamic code [37:44] awesome uh hi Gail thanks for presenting [37:47] uh your research I think it's really [37:49] exciting and uh yeah it could be [37:50] transformative for The Elixir language [37:53] uh my question is uh so I was working [37:56] with uh typescript a bit and actually [37:58] you have uh some more advanced types [38:01] where for example if you have a map with [38:03] a specific set of atoms then you can [38:06] define a type that is basically a union [38:08] of all of those possible atoms so is [38:11] that something that you thought about [38:13] given any thought or is that this [38:15] syntactic sugar that be you know built [38:17] on top of what you presented this this [38:20] required a significant extension to the [38:24] theory be that types Maps [38:28] specifically this being able to do that [38:32] um and that that was the was that the [38:34] gist of your question I think [38:43] so what is the feature [38:46] the the feature is talking about is [38:49] being able to specify uh the type of any [38:52] other atom except board and field uh [38:55] this is a yeah this is a very specific [38:57] extension to typing of maps [39:00] and yeah yeah it works uh oh sorry yeah [39:05] um the answer is yes [39:07] it is uh if you are very very curious [39:11] this uh or no maybe it will appear in [39:15] the paper later [39:19] yeah [39:22] like Maps were actually the hardest part [39:25] of the work so far right do you agree [39:28] yeah so but yeah yeah that's what [39:31] guillaum is saying like we have that but [39:33] it was lots of lots of work it doesn't [39:36] look like that but sometimes would have [39:38] three fars meeting just talking about [39:39] maps and how to type them so [39:45] [Applause] [39:49] [Music] [39:51] [Applause] [39:54] [Music] [40:02] foreign [40:06] [Music]