7 ms·

Type system updates: moving from research into development

282 points by weatherlight 3y ago

ccday 3y ago
Very excited to hear about this. Elixir is a fantastic language but tooling lags behind some other options, a type system should help with that.
- weatherlight 3y ago
  > tooling lags behind some other options. Just out of curiosity. What other options?
  - totallywrong 3y ago
    Elixir leverages Erlang/OTP and the BEAM which is basically a whole platform for applications. Probably only the Java / JVM ecosystem is on par.
    - weatherlight 3y ago
      The tooling in the elixir ecosystem is excelent. The only lang/ecosystem that I think does a better job is maybe Rust.
      - dns_snek 3y ago
        I love Elixir, I use it daily, but I have to disagree. Elixir tooling is in my opinion one of the only sore spots of the ecosystem and its quality is seriously lagging behind the vast majority of other languages. When I say "tooling", I'm talking about language servers and overall editor support. As much as I appreciate the work the team has done, I think we have to be honest about the good and bad parts. ElixirLS has never worked quite right for me, or most other Elixir developers I know. It's often painfully slow to respond even in small project, it often gets stuck in obscure failures that require an editor reload to get it fully working again. If you run into any kind of issue with it, the boilerplate response it always: Try running `rm -rf .elixir_ls _build` which sometimes works, but usually not. Javascript, Typescript have immaculate tooling in this regard, same goes for Java, C#, Go, even Python (on IDE side, the package management situation is of course a dumpster fire). I'd go as far as to say that any language supported by Jetbrains has better tooling than Elixir does.
        weatherlight 3y ago
        https://github.com/elixir-tools https://github.com/elixir-tools Check out next-ls aims to replace ElixirLS. https://www.elixir-tools.dev/next-ls/ https://www.elixir-tools.dev/next-ls/ There's a podcast/interview from its creator below. https://podcast.thinkingelixir.com/153 https://podcast.thinkingelixir.com/153
        losvedir 3y ago
        I use VSCode at work on our Elixir codebases so I feel your pain trying to get ElixirLS working, though when it does work it's pretty good. However, on my personal laptop I've been trying out the Zed editor which has Elixir language server capabilities out of the box (not a user installed plugin) and haven't had any issues at all.
        sk0g 3y ago
        Haven't heard of Zed before, feels pretty snappy! Will try it out some more on other projects, though I can't tell how to set it up with PyEnv packages off the bat.
        dns_snek 3y ago
        > Zed editor macOS only, closed source, and VC funded :( I don't work on a Mac, so it's a non-starter for me, but I'd be very reluctant to switch my workflow to an early stage VC funded product because I don't like having my rug pulled.
        pdimitar 3y ago
        > It's often painfully slow to respond even in small project I had that problem with NeoVim's Mason plugin that manages language servers, then I just cloned `elixir-ls` and made a super small script to update it daily from GitHub and recompile it. I use that in NeoVim instead and it works near-instantly. Give it a try. I don't disagree that IDE support can look subpar but I'd also venture a guess that proper IDE support is very first-world problem. You won't find yourself working on projects with millions of lines in Elixir ever, and thus not having e.g. full-blown IDE refactoring has never been a problem for me or any other Elixir dev I know. All that being said, literally nothing I have ever saw was able to beat Golang's and OCaml's language servers. They just work and are amazingly fast to boot. It's simply a joy coding in those languages with their LS. Rust is trailing closely behind but it's also a fact that its LS is objectively slower -- still, they seem to have made a lot of strides on that front lately and it's much better compared to even one year ago.
      - answiftydev 3y ago
        The command line tooling is pretty good, the elixirls/ide integration is pretty poor compared to other languages I have worked with. Some trivial examples while learning live view. Using : in pattern matching brings up erlang modules, instead of the atom I used elsewhere in the file. html.heex and the ~H sigil can’t seem to support both html and elixir syntax intellsense at the same time. I also somehow got def in intellsense to not make a new function but instead autocomplete to def(). Finally, after hearing how great Ecto was I was hoping it could provide some sort of hints based on the names of tables/rows I had provided in the migrations.
      - jcpst 3y ago
        Sorry, can’t agree on that one. I like to play with elixir in my spare time, love the language. There is a ton of great tooling. But I use C# and Rider at work, and the IDE experience is light-years better.
  - ccday 3y ago
    I use IDEA and most typed languages I write (eg Java, Go, Python with annotations) have better support for things like automated refactoring, bug detection via static analysis, etc
    - weatherlight 3y ago
      Dialyzer gets you pretty far, Especially since Elixir is dynamically typed.
      - wofo 3y ago
        After spending 6 months working on an Elixir codebase, and spoiled by languages with proper IDE support, I'd say Dialyzer is nice... But doesn't get even close to what I'm used to. Sometimes the benefits of the BEAM and the OTP outweight these drawbacks, of course, but to me it sucked the joy out of programming (I'm very type oriented when writing and, more importantly, reading code).
        doctorpangloss 3y ago
        Personally I am most affected by language features that didn’t exist before September, 2021.
        ljlolel 3y ago
        Are you an AI?
        reilly3000 3y ago
        Are you?
        justinjlynn 3y ago
        That face when you realise that it's all Actual Intelligence and it's just some of it has extra steps.
rocketbop 3y ago
Discussed yesterday also. https://news.ycombinator.com/item?id=36576352 https://news.ycombinator.com/item?id=36576352
Pannoniae 3y ago
There seems to be a pattern of introducing static types into previously weakly typed or dynamically typed languages. I think this is because people have written many large projects in them, and without types, it's quite hard to enforce an API or document what to pass into it if there are no types. The drawbacks to statically typed languages have become way less significant since most of them have "var" or an equivalent which saves on typing.
- slondr 3y ago
  Elixir never really didn’t have a static type system, this is just improving it.
- weatherlight 3y ago
  It's also not your "standard static" type system. It's a new type system that novel using Set Theoretical Types. Which is kind of interesting. because if Elixir can get this working properly, it would also probably work for other Strong Dynamically Typed languages. Imagine if Typescript's type system if it were actually sound. The research paper is here if anyone wants to read it. https://www.irif.fr/_media/users/gduboc/elixir-types.pdf https://www.irif.fr/_media/users/gduboc/elixir-types.pdf
- srgpqt 3y ago
  Indeed, even C has caught up! #define let __auto_type
  - dlisboa 3y ago
    Wow, I learn something new every day! https://gcc.gnu.org/onlinedocs/gcc/Typeof.html https://gcc.gnu.org/onlinedocs/gcc/Typeof.html Having learned (old) C in college and taking a closer look at it lately, I was surprised how much you can make it look “modern”, what with _Generic, wchar_t, booleans and even this __auto_type. It seems like with a couple #define macros and some discipline you can make it look and behave more ergonomic.
- mvdtnz 3y ago
  "var" does not "save on typing", at least not in C#. A variable declared with var is still statically typed. Its type is just inferred from context. The compiler will assign it the most specific type possible from that context. That's the important point - this occurs at compile time, not runtime.
weatherlight 3y ago
Proposed type system described in more detail here. https://www.irif.fr/_media/users/gduboc/elixir-types.pdf https://www.irif.fr/_media/users/gduboc/elixir-types.pdf
- DonaldPShimoda 3y ago
  Ah, thanks for that, I was wondering where the details were! Adding this to my pile...
- riffraff 3y ago
  I seemed to remember one of the authors from some previous work on formalizing multimethod dispatch, so I looked him up again.. He seems to have written a ton of interesting stuff on PL theory! https://www.irif.fr/~gc/papers.en.html https://www.irif.fr/~gc/papers.en.html
  - Drup 3y ago
    Giuseppe Castagna is a very well known PL researcher, and very seasoned when it comes to gradual types and "structural" types (the static version of duck-typing), which seems like a great fit for Elixir.
yewenjie 3y ago
Is this type-system guaranteed to be sound? (Does type checking ensure no runtime type bugs?). Also, can it infer all the types if none of the types are actually annotated? Also, what is the novelty about this new type system?
- weatherlight 3y ago
  Yes. it's guaranteed to be sound. As per what makes it unique, from the paper: We present a gradual type system for Elixir, based on the framework of semantic subtyping [10, 19]. This framework, developed for and implemented by the CDuce programming language [3, 15], provides a type system centered on the use of settheoretic types (unions, intersections, negations) that satisfy the commutativity and distributivity properties of the corresponding set-theoretic operations [19]. The system is a polymorphic type system with local type inference, that is, functions are explicitly annotated with types that may contain type variables, but their applications do not require explicit instantiations: the system deduces the right instantiations of every type variable. It also features precise typing of pattern matching combined with type narrowing: the types of the capture variables of the pattern and of some variables of the matched expression are refined in the branches to take into account the results of pattern matching CDuce programming language: https://www.cduce.org https://www.cduce.org
  - tannhaeuser 3y ago
    I had to double-check that, knowing CDuce as an XML-oriented language from when XML was hip around almost twenty years ago - and indeed it's that language for manipulating XML. It's been a while but I thought the point was to experiment with static typing of XML transformations, but ultimately type inference complexity results hit a wall and weren't convincing from a practical PoV. But what do I know - after all, adding types on top of a language that isn't statically typed seems like a pointless exercise to me when there are plenty statically typed languages. I guess it might make sense for a Python code base that's gotten out of control maybe?
    - bcrosby95 3y ago
losvedir 3y ago
I've used Elixir professionally for 6 years and have been very impressed with how it's been managed. All additions seem very careful and deliberate. I can't think of any regression or issue I've had as the language and tooling and standard library have improved. Given that, I'm excited to see how this works out. Adding static types has the potential to be very disruptive but I trust the team to do it in a way that will work very well with existing Elixir apps and the BEAM VM.
- nerdponx 3y ago
  I'm interested to see how this affects Gleam.
  - weatherlight 3y ago
    I don't think it will. Elixir, if everything pans out, will be gradually typed. the new type system will be sound, but will be very different than other type systems. Gleam from Day 1 is going to be statically typed using a Hindley-Milner type system/Algorithm W. It's battle tested. If you come from a lang like Rust, OCaml, Standard ML, etc its type system is going to be very familiar to you.
    - Ndymium 3y ago
      Additionally, Gleam is very different as a language. Erlang is only one of its targets, another one is JavaScript (and I see many people just using it for that alone). I'm personally writing a static blog generator for myself that'll run on the Node target. So I don't think this will have too much effect on Gleam.
daxfohl 3y ago
Is set theory more useful than category theory for dynamic types? Seems like set theory is less constrained, like a set can be part of itself by nature, whereas category theory generally doesn't allow mixing containers and elements like that out of the box IIUC. Seems like category theory best suits Haskell and such where types are more precisely defined (something that could be an int or a bool needs an ADT wrapper), whereas set theory might make sense for completely dynamic types, where something could be an int or a bool or whatever else by nature. But I'm entirely unsure. Maybe it is completely unrelated to why set theory is used as a basis here. Just wondering.
- pizza 3y ago
  > A set has the least structure. It's a discrete category, with no morphisms other than identities. Conversely, the category of sets has the most structure, since its morphisms don't have to preserve any structure. https://twitter.com/BartoszMilewski/status/1674357272498110467 https://twitter.com/BartoszMilewski/status/16743572724981104...
  - climatologist 3y ago
    This is incorrect. The number of morphisms is not what makes mathematical objects more or less structured. What is correct is that the category of sets does not have constraints for morphisms between its objects. Bartosz is equating morphisms and "structure" which is not how most mathematicians think of what it means for a category or an object to be structured.
    - klysm 3y ago
      It seems incorrect to state that his perspective is categorically incorrect. The term “structure” lacks a precise definition and his interpretation isn’t completely invalid.
    - js8 3y ago
      He prefaces the statement with "my intuition tells me", so perhaps he is much less categorical (pun intended) about the claim than you interpret it.
querulous 3y ago
how does the type system handle `receive` in erlang/elixir? does it just require every `receive` clause have a catchall case (meaning every `receive` is any -> T) or does it only guarantee type checking in the absence of external messages?
- josevalim 3y ago
  When you receive, we will use the pattern and guards from the "receive" to lift type information, but we won't verify the messages between processes in our initial efforts. Personally, as future work, I am more interested in typing behaviours, because that's how most users define and interact with processes.
phtrivier 3y ago
As a very frequent nagger about the lack of type system of Elixir, this made my day: > The type system will extract type information from patterns and guards to 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. > 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. Congrats to them. I still wish it had been implemented 10 years ago, but, hey, that train has sailed a long while ago. (I know, trains dont sail. Or, as we say in Elixir-land, "** (MatchError) ...")
- pmontra 3y ago
  Elixir got traction as a Ruby on Rails replacement in combination with Phoenix. That was deliberate. The core modules and functions got names identical or close to their Ruby counterparts. It makes sense that they aimed a dynamically typed language to another dynamically typed language. If they aimed at Java developers they would have to add a type system since the beginning. That's extra work though. I got into Elixir because it is dynamically typed. I wouldn't have considered a statically typed one. Luckily I find enough customers with Ruby and Python. The last Elixir project was from a couple of years ago. I didn't have to use something statically typed since 2012, I think. Too tiring to write.
  - josevalim 3y ago
    Folks tend to understate the influence of Erlang and overstate the influence of Ruby on Elixir. In a nutshell: Elixir is dynamic because Erlang is dynamic. :) Ruby did influence the syntax and the names in the standard library, but the latter was also done in a more "democratic" fashion: I would look into Ruby, JavaScript, Clojure, Haskell, and choose a name that was common and closer reflected the semantics that would fit Elixir (for example, the term "protocol" come from Clojure). The most curious case is the "Regex" module (which is named Regexp in Ruby). I quickly noticed that both "regex" and "regexp" were very common, Erlang simply used "re", so I had no clear direction to lean towards. The decision came by getting the top 50 languages at the time and using Rosetta Code to pick the most common term (which was regex).

282 points by weatherlight 3y ago

Very excited to hear about this. Elixir is a fantastic language but tooling lags behind some other options, a type system should help with that.

weatherlight 3y ago
> tooling lags behind some other options. Just out of curiosity. What other options?
- totallywrong 3y ago
  Elixir leverages Erlang/OTP and the BEAM which is basically a whole platform for applications. Probably only the Java / JVM ecosystem is on par.
  - weatherlight 3y ago
    The tooling in the elixir ecosystem is excelent. The only lang/ecosystem that I think does a better job is maybe Rust.
    - dns_snek 3y ago
      I love Elixir, I use it daily, but I have to disagree. Elixir tooling is in my opinion one of the only sore spots of the ecosystem and its quality is seriously lagging behind the vast majority of other languages. When I say "tooling", I'm talking about language servers and overall editor support. As much as I appreciate the work the team has done, I think we have to be honest about the good and bad parts. ElixirLS has never worked quite right for me, or most other Elixir developers I know. It's often painfully slow to respond even in small project, it often gets stuck in obscure failures that require an editor reload to get it fully working again. If you run into any kind of issue with it, the boilerplate response it always: Try running `rm -rf .elixir_ls _build` which sometimes works, but usually not. Javascript, Typescript have immaculate tooling in this regard, same goes for Java, C#, Go, even Python (on IDE side, the package management situation is of course a dumpster fire). I'd go as far as to say that any language supported by Jetbrains has better tooling than Elixir does.
      - weatherlight 3y ago
        https://github.com/elixir-tools https://github.com/elixir-tools Check out next-ls aims to replace ElixirLS. https://www.elixir-tools.dev/next-ls/ https://www.elixir-tools.dev/next-ls/ There's a podcast/interview from its creator below. https://podcast.thinkingelixir.com/153 https://podcast.thinkingelixir.com/153
      - losvedir 3y ago
        I use VSCode at work on our Elixir codebases so I feel your pain trying to get ElixirLS working, though when it does work it's pretty good. However, on my personal laptop I've been trying out the Zed editor which has Elixir language server capabilities out of the box (not a user installed plugin) and haven't had any issues at all.
        sk0g 3y ago
        Haven't heard of Zed before, feels pretty snappy! Will try it out some more on other projects, though I can't tell how to set it up with PyEnv packages off the bat.
        dns_snek 3y ago
        > Zed editor macOS only, closed source, and VC funded :( I don't work on a Mac, so it's a non-starter for me, but I'd be very reluctant to switch my workflow to an early stage VC funded product because I don't like having my rug pulled.
      - pdimitar 3y ago
        > It's often painfully slow to respond even in small project I had that problem with NeoVim's Mason plugin that manages language servers, then I just cloned `elixir-ls` and made a super small script to update it daily from GitHub and recompile it. I use that in NeoVim instead and it works near-instantly. Give it a try. I don't disagree that IDE support can look subpar but I'd also venture a guess that proper IDE support is very first-world problem. You won't find yourself working on projects with millions of lines in Elixir ever, and thus not having e.g. full-blown IDE refactoring has never been a problem for me or any other Elixir dev I know. All that being said, literally nothing I have ever saw was able to beat Golang's and OCaml's language servers. They just work and are amazingly fast to boot. It's simply a joy coding in those languages with their LS. Rust is trailing closely behind but it's also a fact that its LS is objectively slower -- still, they seem to have made a lot of strides on that front lately and it's much better compared to even one year ago.
    - answiftydev 3y ago
      The command line tooling is pretty good, the elixirls/ide integration is pretty poor compared to other languages I have worked with. Some trivial examples while learning live view. Using : in pattern matching brings up erlang modules, instead of the atom I used elsewhere in the file. html.heex and the ~H sigil can’t seem to support both html and elixir syntax intellsense at the same time. I also somehow got def in intellsense to not make a new function but instead autocomplete to def(). Finally, after hearing how great Ecto was I was hoping it could provide some sort of hints based on the names of tables/rows I had provided in the migrations.
    - jcpst 3y ago
      Sorry, can’t agree on that one. I like to play with elixir in my spare time, love the language. There is a ton of great tooling. But I use C# and Rider at work, and the IDE experience is light-years better.
- ccday 3y ago
  I use IDEA and most typed languages I write (eg Java, Go, Python with annotations) have better support for things like automated refactoring, bug detection via static analysis, etc
  - weatherlight 3y ago
    Dialyzer gets you pretty far, Especially since Elixir is dynamically typed.
    - wofo 3y ago
      After spending 6 months working on an Elixir codebase, and spoiled by languages with proper IDE support, I'd say Dialyzer is nice... But doesn't get even close to what I'm used to. Sometimes the benefits of the BEAM and the OTP outweight these drawbacks, of course, but to me it sucked the joy out of programming (I'm very type oriented when writing and, more importantly, reading code).
      - doctorpangloss 3y ago
        Personally I am most affected by language features that didn’t exist before September, 2021.
        ljlolel 3y ago
        Are you an AI?
        reilly3000 3y ago
        Are you?
        justinjlynn 3y ago
        That face when you realise that it's all Actual Intelligence and it's just some of it has extra steps.

rocketbop 3y ago

Discussed yesterday also. https://news.ycombinator.com/item?id=36576352 https://news.ycombinator.com/item?id=36576352

Pannoniae 3y ago

There seems to be a pattern of introducing static types into previously weakly typed or dynamically typed languages. I think this is because people have written many large projects in them, and without types, it's quite hard to enforce an API or document what to pass into it if there are no types. The drawbacks to statically typed languages have become way less significant since most of them have "var" or an equivalent which saves on typing.

slondr 3y ago
Elixir never really didn’t have a static type system, this is just improving it.
weatherlight 3y ago
It's also not your "standard static" type system. It's a new type system that novel using Set Theoretical Types. Which is kind of interesting. because if Elixir can get this working properly, it would also probably work for other Strong Dynamically Typed languages. Imagine if Typescript's type system if it were actually sound. The research paper is here if anyone wants to read it. https://www.irif.fr/_media/users/gduboc/elixir-types.pdf https://www.irif.fr/_media/users/gduboc/elixir-types.pdf
srgpqt 3y ago
Indeed, even C has caught up! #define let __auto_type
- dlisboa 3y ago
  Wow, I learn something new every day! https://gcc.gnu.org/onlinedocs/gcc/Typeof.html https://gcc.gnu.org/onlinedocs/gcc/Typeof.html Having learned (old) C in college and taking a closer look at it lately, I was surprised how much you can make it look “modern”, what with _Generic, wchar_t, booleans and even this __auto_type. It seems like with a couple #define macros and some discipline you can make it look and behave more ergonomic.
mvdtnz 3y ago
"var" does not "save on typing", at least not in C#. A variable declared with var is still statically typed. Its type is just inferred from context. The compiler will assign it the most specific type possible from that context. That's the important point - this occurs at compile time, not runtime.

weatherlight 3y ago

Proposed type system described in more detail here. https://www.irif.fr/_media/users/gduboc/elixir-types.pdf https://www.irif.fr/_media/users/gduboc/elixir-types.pdf

DonaldPShimoda 3y ago
Ah, thanks for that, I was wondering where the details were! Adding this to my pile...
riffraff 3y ago
I seemed to remember one of the authors from some previous work on formalizing multimethod dispatch, so I looked him up again.. He seems to have written a ton of interesting stuff on PL theory! https://www.irif.fr/~gc/papers.en.html https://www.irif.fr/~gc/papers.en.html
- Drup 3y ago
  Giuseppe Castagna is a very well known PL researcher, and very seasoned when it comes to gradual types and "structural" types (the static version of duck-typing), which seems like a great fit for Elixir.

yewenjie 3y ago

Is this type-system guaranteed to be sound? (Does type checking ensure no runtime type bugs?). Also, can it infer all the types if none of the types are actually annotated? Also, what is the novelty about this new type system?

weatherlight 3y ago
Yes. it's guaranteed to be sound. As per what makes it unique, from the paper: We present a gradual type system for Elixir, based on the framework of semantic subtyping [10, 19]. This framework, developed for and implemented by the CDuce programming language [3, 15], provides a type system centered on the use of settheoretic types (unions, intersections, negations) that satisfy the commutativity and distributivity properties of the corresponding set-theoretic operations [19]. The system is a polymorphic type system with local type inference, that is, functions are explicitly annotated with types that may contain type variables, but their applications do not require explicit instantiations: the system deduces the right instantiations of every type variable. It also features precise typing of pattern matching combined with type narrowing: the types of the capture variables of the pattern and of some variables of the matched expression are refined in the branches to take into account the results of pattern matching CDuce programming language: https://www.cduce.org https://www.cduce.org
- tannhaeuser 3y ago
  I had to double-check that, knowing CDuce as an XML-oriented language from when XML was hip around almost twenty years ago - and indeed it's that language for manipulating XML. It's been a while but I thought the point was to experiment with static typing of XML transformations, but ultimately type inference complexity results hit a wall and weren't convincing from a practical PoV. But what do I know - after all, adding types on top of a language that isn't statically typed seems like a pointless exercise to me when there are plenty statically typed languages. I guess it might make sense for a Python code base that's gotten out of control maybe?
  - bcrosby95 3y ago

losvedir 3y ago

I've used Elixir professionally for 6 years and have been very impressed with how it's been managed. All additions seem very careful and deliberate. I can't think of any regression or issue I've had as the language and tooling and standard library have improved. Given that, I'm excited to see how this works out. Adding static types has the potential to be very disruptive but I trust the team to do it in a way that will work very well with existing Elixir apps and the BEAM VM.

nerdponx 3y ago
I'm interested to see how this affects Gleam.
- weatherlight 3y ago
  I don't think it will. Elixir, if everything pans out, will be gradually typed. the new type system will be sound, but will be very different than other type systems. Gleam from Day 1 is going to be statically typed using a Hindley-Milner type system/Algorithm W. It's battle tested. If you come from a lang like Rust, OCaml, Standard ML, etc its type system is going to be very familiar to you.
  - Ndymium 3y ago
    Additionally, Gleam is very different as a language. Erlang is only one of its targets, another one is JavaScript (and I see many people just using it for that alone). I'm personally writing a static blog generator for myself that'll run on the Node target. So I don't think this will have too much effect on Gleam.

daxfohl 3y ago

Is set theory more useful than category theory for dynamic types? Seems like set theory is less constrained, like a set can be part of itself by nature, whereas category theory generally doesn't allow mixing containers and elements like that out of the box IIUC. Seems like category theory best suits Haskell and such where types are more precisely defined (something that could be an int or a bool needs an ADT wrapper), whereas set theory might make sense for completely dynamic types, where something could be an int or a bool or whatever else by nature. But I'm entirely unsure. Maybe it is completely unrelated to why set theory is used as a basis here. Just wondering.

pizza 3y ago
> A set has the least structure. It's a discrete category, with no morphisms other than identities. Conversely, the category of sets has the most structure, since its morphisms don't have to preserve any structure. https://twitter.com/BartoszMilewski/status/1674357272498110467 https://twitter.com/BartoszMilewski/status/16743572724981104...
- climatologist 3y ago
  This is incorrect. The number of morphisms is not what makes mathematical objects more or less structured. What is correct is that the category of sets does not have constraints for morphisms between its objects. Bartosz is equating morphisms and "structure" which is not how most mathematicians think of what it means for a category or an object to be structured.
  - klysm 3y ago
    It seems incorrect to state that his perspective is categorically incorrect. The term “structure” lacks a precise definition and his interpretation isn’t completely invalid.
  - js8 3y ago
    He prefaces the statement with "my intuition tells me", so perhaps he is much less categorical (pun intended) about the claim than you interpret it.

querulous 3y ago

how does the type system handle `receive` in erlang/elixir? does it just require every `receive` clause have a catchall case (meaning every `receive` is any -> T) or does it only guarantee type checking in the absence of external messages?

josevalim 3y ago
When you receive, we will use the pattern and guards from the "receive" to lift type information, but we won't verify the messages between processes in our initial efforts. Personally, as future work, I am more interested in typing behaviours, because that's how most users define and interact with processes.

phtrivier 3y ago

As a very frequent nagger about the lack of type system of Elixir, this made my day: > The type system will extract type information from patterns and guards to 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. > 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. Congrats to them. I still wish it had been implemented 10 years ago, but, hey, that train has sailed a long while ago. (I know, trains dont sail. Or, as we say in Elixir-land, "** (MatchError) ...")

pmontra 3y ago
Elixir got traction as a Ruby on Rails replacement in combination with Phoenix. That was deliberate. The core modules and functions got names identical or close to their Ruby counterparts. It makes sense that they aimed a dynamically typed language to another dynamically typed language. If they aimed at Java developers they would have to add a type system since the beginning. That's extra work though. I got into Elixir because it is dynamically typed. I wouldn't have considered a statically typed one. Luckily I find enough customers with Ruby and Python. The last Elixir project was from a couple of years ago. I didn't have to use something statically typed since 2012, I think. Too tiring to write.
- josevalim 3y ago
  Folks tend to understate the influence of Erlang and overstate the influence of Ruby on Elixir. In a nutshell: Elixir is dynamic because Erlang is dynamic. :) Ruby did influence the syntax and the names in the standard library, but the latter was also done in a more "democratic" fashion: I would look into Ruby, JavaScript, Clojure, Haskell, and choose a name that was common and closer reflected the semantics that would fit Elixir (for example, the term "protocol" come from Clojure). The most curious case is the "Regex" module (which is named Regexp in Ruby). I quickly noticed that both "regex" and "regexp" were very common, Erlang simply used "re", so I had no clear direction to lean towards. The decision came by getting the top 50 languages at the time and using Rosetta Code to pick the most common term (which was regex).