From e585461d3d3a26ea4a68f9845cb9116a45c14721 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jos=C3=A9=20Valim?= Date: Mon, 19 Jun 2023 20:13:12 +0200 Subject: [PATCH 1/7] Type system updates --- ...-type-system-updates-research-dev.markdown | 83 +++++++++++++++++++ 1 file changed, 83 insertions(+) create mode 100644 _posts/2023-06-22-type-system-updates-research-dev.markdown diff --git a/_posts/2023-06-22-type-system-updates-research-dev.markdown b/_posts/2023-06-22-type-system-updates-research-dev.markdown new file mode 100644 index 000000000..88a111920 --- /dev/null +++ b/_posts/2023-06-22-type-system-updates-research-dev.markdown @@ -0,0 +1,83 @@ +--- +layout: post +title: "Type system updates: moving from research into development" +author: José Valim +category: Announcements +excerpt: A short status update on the effort to bring a type system into Elixir. +--- + +A year ago, at ElixirConf EU 2022, we announced an effort to research +and develop a type system for Elixir ([video presentation](https://www.youtube.com/watch?v=Jf5Hsa1KOc8)) +([written report](/blog/2022/10/05/my-future-with-elixir-set-theoretic-types/)). + +This work is happening under the lead of [Giuseppe Castagna](https://www.irif.fr/~gc/), +Senior Research Scientist at [IRIF](https://www.irif.fr), and taken by +[Guillaume Duboc](https://www.irif.fr/users/gduboc/index) as part of his +PhD studies, with further guidance from myself (José Valim). + +This article is a summary of where we are in our efforts and where we +are going. + +### Out of research + +Our main goal during research is to find a type system that can model +most of Elixir's functional semantics and develop brand new theory on +the areas we found to be incompatible or lacking. We believe we were +able to achieve this goal with a gradual set-theoretic type system +and we are now ready to head towards development. Over the last 2 months, +we have published plenty of resources on our results: + + * [A technical report on the design principles of the Elixir type system](https://www.irif.fr/_media/users/gduboc/elixir-types.pdf) + * [A technical presentation by Guillaume Duboc at ElixirConf 2023 on the work above](https://youtube.com/watch?v=gJJH7a2J9O8) + * [An informal discussion with Giuseppe Castagna, Guillaume Duboc, and José Valim on the SmartLogic podcast](https://smartlogic.io/podcast/elixir-wizards/s10-e12-jose-guillaume-giuseppe-types-elixir/) + * [An informal Q&A with Guillaume Duboc, José Valim, and the community on Twitch](https://www.twitch.tv/videos/1841707383) + +Our focus so far has been on the semantics. While we have introduced a +new syntax capable of expressing the semantics of the new set-theoretic +type system, the syntax is not final as there are still no concrete +plans for user-facing changes to the language. Once we are confident +those changes will happen, we will have plenty of discussion with the +community about the type system interface and its syntax. + +The work so far has been made possible thanks to a partnership between +the [CNRS](https://www.cnrs.fr/fr) and [Remote](https://remote.com), +with sponsorships from [Fresha](https://www.fresha.com), +[Supabase](https://supabase.com), and [Dashbit](https://dashbit.co). + +### Into development + +While there is still on-going research, our focus for the second semester +of 2023 onwards is on development. + +Incorporating a type system into a language used at scale can be a daunting +task. Our concerns range from how the community will interact and use the +type system to how it will perform on large code bases. Therefore, our plan +is to gradually introduce our gradual (pun intended) type system into the +Elixir compiler. + +In the first release, types will be used just internally by the compiler. +The type system will extract type information from patterns and guards to +find the most obvious of mistakes, such as typos in field names or type +mismatches from attempting to add an integer to a string, without introducing +any user-facing changes to the language. At this stage, our main goal is +to assess the performance impact of the type system and the quality of +the reports we can generate in case of typing violations. If we are +unhappy with the results, we still have time to reassess our work or drop +the initiative altogether. + +The second milestone is to introduce type annotations only in structs, +which are named and statically-defined in Elixir codebases. Elixir programs +frequently pattern match on structs, which reveals information about +the struct fields, but it knows nothing about their respective types. +By propagating types from structs and their fields throughout the program, +we will increase the type system’s ability to find errors while further +straining our type system implementation. + +The third milestone is to introduce the (most likely) `$`-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. If successful, then we +will effectively have introduced a type system into the language. + +This new exciting development stage is sponsored by [Fresha](https://www.fresha.com), [Starfish*](https://starfish.team), +and [Dashbit](https://dashbit.co). From 9000471abf108d21b624a6cb823b391cb4927e82 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jos=C3=A9=20Valim?= Date: Wed, 21 Jun 2023 14:30:19 +0200 Subject: [PATCH 2/7] Update _posts/2023-06-22-type-system-updates-research-dev.markdown --- _posts/2023-06-22-type-system-updates-research-dev.markdown | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/_posts/2023-06-22-type-system-updates-research-dev.markdown b/_posts/2023-06-22-type-system-updates-research-dev.markdown index 88a111920..ba614b5de 100644 --- a/_posts/2023-06-22-type-system-updates-research-dev.markdown +++ b/_posts/2023-06-22-type-system-updates-research-dev.markdown @@ -27,7 +27,7 @@ able to achieve this goal with a gradual set-theoretic type system and we are now ready to head towards development. Over the last 2 months, we have published plenty of resources on our results: - * [A technical report on the design principles of the Elixir type system](https://www.irif.fr/_media/users/gduboc/elixir-types.pdf) + * [A technical report on the design principles of the Elixir type system](https://arxiv.org/abs/2306.06391) * [A technical presentation by Guillaume Duboc at ElixirConf 2023 on the work above](https://youtube.com/watch?v=gJJH7a2J9O8) * [An informal discussion with Giuseppe Castagna, Guillaume Duboc, and José Valim on the SmartLogic podcast](https://smartlogic.io/podcast/elixir-wizards/s10-e12-jose-guillaume-giuseppe-types-elixir/) * [An informal Q&A with Guillaume Duboc, José Valim, and the community on Twitch](https://www.twitch.tv/videos/1841707383) From e6f0e1b0a2d9c45ca7cf0dbcfce3001a007523ea Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jos=C3=A9=20Valim?= Date: Sat, 24 Jun 2023 19:45:52 +0200 Subject: [PATCH 3/7] Update _posts/2023-06-22-type-system-updates-research-dev.markdown --- _posts/2023-06-22-type-system-updates-research-dev.markdown | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/_posts/2023-06-22-type-system-updates-research-dev.markdown b/_posts/2023-06-22-type-system-updates-research-dev.markdown index ba614b5de..b1da03b9e 100644 --- a/_posts/2023-06-22-type-system-updates-research-dev.markdown +++ b/_posts/2023-06-22-type-system-updates-research-dev.markdown @@ -11,7 +11,7 @@ and develop a type system for Elixir ([video presentation](https://www.youtube.c ([written report](/blog/2022/10/05/my-future-with-elixir-set-theoretic-types/)). This work is happening under the lead of [Giuseppe Castagna](https://www.irif.fr/~gc/), -Senior Research Scientist at [IRIF](https://www.irif.fr), and taken by +CNRS Senior Researcher, and taken by [Guillaume Duboc](https://www.irif.fr/users/gduboc/index) as part of his PhD studies, with further guidance from myself (José Valim). From 6fe20a2bdb61f8f99155ab4291c736eb3f90702a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jos=C3=A9=20Valim?= Date: Sat, 24 Jun 2023 19:46:09 +0200 Subject: [PATCH 4/7] Update _posts/2023-06-22-type-system-updates-research-dev.markdown Co-authored-by: Fernando Tapia Rico --- _posts/2023-06-22-type-system-updates-research-dev.markdown | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/_posts/2023-06-22-type-system-updates-research-dev.markdown b/_posts/2023-06-22-type-system-updates-research-dev.markdown index b1da03b9e..aea8d4c67 100644 --- a/_posts/2023-06-22-type-system-updates-research-dev.markdown +++ b/_posts/2023-06-22-type-system-updates-research-dev.markdown @@ -51,7 +51,7 @@ of 2023 onwards is on development. Incorporating a type system into a language used at scale can be a daunting task. Our concerns range from how the community will interact and use the -type system to how it will perform on large code bases. Therefore, our plan +type system to how it will perform on large codebases. Therefore, our plan is to gradually introduce our gradual (pun intended) type system into the Elixir compiler. From c4b4980b83c5eef26280cc426f2a130c72213233 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jos=C3=A9=20Valim?= Date: Sat, 24 Jun 2023 19:47:04 +0200 Subject: [PATCH 5/7] Update _posts/2023-06-22-type-system-updates-research-dev.markdown Co-authored-by: Fernando Tapia Rico --- _posts/2023-06-22-type-system-updates-research-dev.markdown | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/_posts/2023-06-22-type-system-updates-research-dev.markdown b/_posts/2023-06-22-type-system-updates-research-dev.markdown index aea8d4c67..9047dec04 100644 --- a/_posts/2023-06-22-type-system-updates-research-dev.markdown +++ b/_posts/2023-06-22-type-system-updates-research-dev.markdown @@ -57,7 +57,7 @@ Elixir compiler. In the first release, types will be used just internally by the compiler. The type system will extract type information from patterns and guards to -find the most obvious of mistakes, such as typos in field names or type +find the most obvious mistakes, such as typos in field names or type mismatches from attempting to add an integer to a string, without introducing any user-facing changes to the language. At this stage, our main goal is to assess the performance impact of the type system and the quality of From df34595f32da2cfe70b123b3d88255b22359aa4f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jos=C3=A9=20Valim?= Date: Mon, 3 Jul 2023 18:05:33 +0200 Subject: [PATCH 6/7] Update _posts/2023-06-22-type-system-updates-research-dev.markdown --- _posts/2023-06-22-type-system-updates-research-dev.markdown | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/_posts/2023-06-22-type-system-updates-research-dev.markdown b/_posts/2023-06-22-type-system-updates-research-dev.markdown index 9047dec04..432256593 100644 --- a/_posts/2023-06-22-type-system-updates-research-dev.markdown +++ b/_posts/2023-06-22-type-system-updates-research-dev.markdown @@ -79,5 +79,6 @@ users can annotate their code with types, but any untyped parameter will be assumed to be of the `dynamic()` type. If successful, then we will effectively have introduced a type system into the language. -This new exciting development stage is sponsored by [Fresha](https://www.fresha.com), [Starfish*](https://starfish.team), +This new exciting development stage is sponsored by [Fresha](https://www.fresha.com) ([they are hiring!](https://www.fresha.com/careers/openings?department=engineering)), +[Starfish*](https://starfish.team) ([they are hiring!](https://starfish.team/jobs/experienced-elixir-developer)), and [Dashbit](https://dashbit.co). From 81e625f1d64eeac283c2fea50eea7ddff51fca76 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jos=C3=A9=20Valim?= Date: Mon, 3 Jul 2023 18:06:09 +0200 Subject: [PATCH 7/7] Apply suggestions from code review --- _posts/2023-06-22-type-system-updates-research-dev.markdown | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/_posts/2023-06-22-type-system-updates-research-dev.markdown b/_posts/2023-06-22-type-system-updates-research-dev.markdown index 432256593..98a6ec5e9 100644 --- a/_posts/2023-06-22-type-system-updates-research-dev.markdown +++ b/_posts/2023-06-22-type-system-updates-research-dev.markdown @@ -18,7 +18,7 @@ PhD studies, with further guidance from myself (José Valim). This article is a summary of where we are in our efforts and where we are going. -### Out of research +## Out of research Our main goal during research is to find a type system that can model most of Elixir's functional semantics and develop brand new theory on @@ -44,7 +44,7 @@ the [CNRS](https://www.cnrs.fr/fr) and [Remote](https://remote.com), with sponsorships from [Fresha](https://www.fresha.com), [Supabase](https://supabase.com), and [Dashbit](https://dashbit.co). -### Into development +## Into development While there is still on-going research, our focus for the second semester of 2023 onwards is on development.