9 ms·

Why Typing Erlang is Hard: Standard Erlang

134 points by leostera 6y ago

Joker_vD 6y ago
Interestingly enough, the article doesn't say anything about propagation of types, which is the crux of the type checking and what makes any typing system useful or useless, obnoxious or helpful. Consider the example from the article: % a good old list length counter count(A=[_|_]) -> count(A, 0). count([], C) -> C; count([_|T], C) -> count(T, C+1). What is the type of count/2? Arguably, it's "(list, any | number) -> any | number", which means that count/1 has type "list -> any | number". Well, that's bloody pointless, isn't it? What you probably want is "(list, any) -> any | (list, number) -> number" for count/2, so you could give count/1 its useful type "list -> number", but intersection function types are notoriously difficult to infer or typecheck, even with manual annotations.
- dnautics 6y ago
  If you drill down to the beam opcodes it should be possible to infer correctly that the type of count/2 can only take number in the second argument.
  - Joker_vD 6y ago
    No, count/2 can sometimes take non-numbers in the second argument, behold: 1> c(test_count). {ok,test_count} 2> test_count:count([], bang). bang
    - dnautics 6y ago
      Yeah, I mean that it will properly identify that the only time you can do that is when you have an empty list. The final spec will be (in elixir syntax): (nonempty_list, number -> number) | ([], any -> any) It should also be able to correctly infer that the count/1 function must be (nonempty_list -> pos_integer) | ([] -> 0)
      - Joker_vD 6y ago
        I am using an old version of erlang, so typer infers the following types: -spec count([any()],_) -> any(). -spec count([any(),...]) -> any(). If I unexport count/2, it infers -spec count([any(),...]) -> non_neg_integer(). -spec count([any()],non_neg_integer()) -> non_neg_integer().
        dnautics 6y ago
        I did say "should be able to" without regard to any of the existing type inference engines =D I'll be sure to make this as explicit test in Mavis Inference, which is the one I'm working on. https://github.com/ityonemo/mavis_inference/issues/47 https://github.com/ityonemo/mavis_inference/issues/47
    - yellowapple 6y ago
      I'd imagine that in this context (i.e. one where a 1-arity function initializes a tail-recursive 2-arity function) the 1-arity function is the only one that'd be exposed outside of the module, in which case you can know with reasonable certainty that only things within the current module will ever call it. If you really do need to export the 2-arity version, you could always do a meaningless addition to force it to typecheck to a number, like so: count([], C) -> C+0; count([_|T], C) -> count(T, C+1); Which should then result in the following: erl> c(test_count). {ok,test_count} erl> test_count:count([], bang). ** exception error: an error occurred when evaluating an arithmetic expression in function test_count:count/2 (test_count.erl, line 8) Or alternately, use guards (though in the context of BEAM-level introspection I haven't the slightest idea if this would produce an equivalent check): count([], C) when is_integer(C) -> C; count([_|T], C) when is_integer(C) -> count(T, C+1); Which then gets you a somewhat clearer error message: 10> c(test_count). {ok,test_count} 11> test_count:count([], bang). ** exception error: no function clause matching test_count:count([],bang) (test_count.erl, line 8)
      - Joker_vD 6y ago
        Yes, if you look at my reply to the sibling comment, you'll see that if count/2 is unexported, TypEr (apparently, that's the proper capitalization) infers the types with non_negative_integer(). In fact, I've just looked at the original TypEr paper [0], and wow, they use exactly this example in the section 6: "One might even jump to the conclusion that success typings are unnecessarily general and, as such, quite useless. However, notice that this success typing succinctly captures all possible applications of length_3 which will not result in a type error. [...] Still, we also find the situation sub-optimal and we will improve on it as explained below", and then they use exactly your proposal, recognizing that non-exported functions are only called from the exported functions, and perform dataflow analysis to constrain the types even further. [0] Tobias Lindahl and Konstantinos Sagonas, "Practical type inference based on success typings", https://www.it.uu.se/research/group/hipe/dialyzer/publications/succ_types.pdf https://www.it.uu.se/research/group/hipe/dialyzer/publicatio...
skohan 6y ago
I really want to like Erlang because the priorities and USP's of the language are super compelling for a lot of use-cases. I tried to kick the tires on it a couple years ago, and what I found is that the error messages were just so vexing, and it took a minute to understand what they meant, even in toy examples. Maybe it gets better with time, or there is tooling to help with this, but it seemed a bit behind the times with the standard which has been set by more modern programming languages.
- cpursley 6y ago
  Give Elixir a spin.
  - deleted 6y ago
    [deleted]
  - dognotdog 6y ago
    I'd second that, Elixir does away with the sometimes vexing comma and dot syntax used for scoping. Also, it does have mutable variables. You do have to get to grips with pattern matching and processes as objects being such core concepts, but I found that once I got it, it is wonderful.
    - dnautics 6y ago
      Just to clarify: Values in elixir are still immutable. The core team will insist that variables are immutable but bindings are mutable, but in my mind variables are their bindings (there is not a third category distinct from the value and the lexical binding). I think there is huge debate as to whether this is good or bad - I think though you really really want to have mutable variables in the REPL. In your static code it's trivial to check for variable rebinding and be sure you're not doing it (credo makes this easy to set up)
      - wtetzner 6y ago
        Variables in Elixir are not mutable, they can just be rebound. Think 'let' in Scheme or ML.
huseyinkeles 6y ago
I'd recommend anyone who have troubles with outdatedness (?) of the Erlang, to try Elixir. It runs on Erlang virtual machine, very modern and pleasure to code in.
dnautics 6y ago
I'm currently actively working on a typechecking system for elixir (three packages: https://github.com/ityonemo/selectrix https://github.com/ityonemo/selectrix for compile-time interface, ../mavis for type logic, and ../mavis_inference for performing type inference on compiled code). The chief difficulties I am running into are: 1) How to do intersections on functions and maps (this is in the article): f(integer) -> integer is not usable as f(any) -> integer 2) not all of the erlang bytecode instructions are well documented 3) I still haven't figured out how to deal with circular dependencies at the module level. Erlang makes this easy in these ways: 1) compiled module structure is simple and the way branching works makes the mechanics of type inference trivial. 2) erlangs concurrency makes dealing with, for example in-module dependencies trivial 3) there are only a handful of types in erlang so, aside from functions, their subtyping relationships are very straightforward. Elixir makes this easy in these ways: 1) Typechecking structs can be more straightforward than records. 2) Writing a composable type logic (mavis) is super easy with elixir's protocols 3) I built (and am refining) a very easy dsl that makes creating and testing logic for the beam opcodes less of a hair-tearing experience: https://github.com/ityonemo/mavis_inference/blob/main/lib/type.inference/opcodes/gc_bif.ex https://github.com/ityonemo/mavis_inference/blob/main/lib/ty...
- FrankBro 6y ago
  I'm going to shill Gradualizer[1] in here as well. 1. I think you have to see typing as helpful information. Like: -spec add(integer(), integer()) -> integer(). add(A, B) -> A + B. Technically, nothing prevents add from accepting number() or float(). It's too much specification. 2. I was surprised how much there actually is but also disappointed that a lot of errors were in until OTP 23. Gradualizer also overrides some definitions [2] 3. Haven't encountered a problem with this yet with gradualizer, would need to test. [1] https://github.com/josefs/Gradualizer https://github.com/josefs/Gradualizer [2] https://github.com/josefs/Gradualizer/blob/master/priv/prelude/lists.specs.erl https://github.com/josefs/Gradualizer/blob/master/priv/prelu...
  - dnautics 6y ago
    Yeah, I had thought that development of Gradualizer had halted, glad to see it's not. Part of why I wanted to do Mavis is because I wanted to make it easy for developers to make their own custom overrides and ship it with their libraries, especially for Elixir protocols[0]. still haven't figured out how to architect that, but I have an idea. > I think you have to see typing as helpful information Indeed. Selectrix will allow you to chain your inference with fallbacks, so, maybe the first level is a fast cache, second level is checking files for user overrides, third level is dialyzer specs, fourth level is inference. I think it should also be possible to create an addon module with Mavis that lets you type inbound messages for GenServers, given a set of constraints (all possible calls and casts are present in the module itself as an API) [0] it's a big problem that in elixir, Enumerable protocol destroys typing information, so I want to make an typing override for Enumerable an "example" typing override system.
Snitch-Thursday 6y ago
I'm watching Gleam[1] for my 'I want to learn Erlang but dont want to deal with having to do runtime type checks so I wish there was a Statically-Typed Erlang' dreams. [1] https://gleam.run/news/gleam-v0.12-and-gleam-otp-v0.1-released/ https://gleam.run/news/gleam-v0.12-and-gleam-otp-v0.1-releas...
- dnautics 6y ago
  I think that devon estes has a point that it is likely that trying to graft a foreign typesytem onto the BEAM is not a good idea. I'm glad someone is trying, though.
  - modernerd 6y ago
    I think the tweet was deleted but it's cached here, for others like me who had not seen Devon's take: https://webcache.googleusercontent.com/search?q=cache:JkQRkuQWRL8J:https://twitter.com/devoncestes/status/1307042045693956099+&cd=2&hl=en&ct=clnk&gl=at https://webcache.googleusercontent.com/search?q=cache:JkQRku...
    - tym0 6y ago
      Thanks for sharing. To save people a click the author of the tweet is opposed to adding a type system to Elixir not the BEAM, he seems to be seeing project like Gleam in a positive light.
- mastermind1014 6y ago
  Check out Caramel [1] as well - [1] https://github.com/AbstractMachinesLab/caramel https://github.com/AbstractMachinesLab/caramel
  - mikhailfranco 6y ago
    and Hamler too ... https://www.hamler-lang.org https://www.hamler-lang.org https://github.com/hamler-lang https://github.com/hamler-lang https://news.ycombinator.com/item?id=23491516 https://news.ycombinator.com/item?id=23491516
FrankBro 6y ago
I replied to your post on twitter but I highly recommend Gradualizer[1]. Discovered it last year and started using it. The refinement portion handles unions and guards very well. It's not perfect but I'm integrating it in our codebase with some interesting successes. I'm hoping more people use it on their codebase and can find any bugs they have with it so it can be improved further. [1] https://github.com/josefs/Gradualizer https://github.com/josefs/Gradualizer
sharno 6y ago
WhatsApp is supposed to release an Erlang typechecker this month, I thinking it’d be good to see how they handle this
- Ndymium 6y ago
  It has been delayed: https://elixirforum.com/t/facebook-is-writing-a-new-statically-typed-language-to-run-on-the-beam/29829/34?u=nicd https://elixirforum.com/t/facebook-is-writing-a-new-statical...
dmix 6y ago
> all sorts of pattern matching Outside of the famous builtin process model/BEAM (plus the subsequent ‘crash first’ style design of programs which adds resiliency) the pattern matching is what makes Erlang one of the best languages and the one thing I wish every new language copied. You kinda get it in Haskell and Rust with the maybe style pattern matching. Rust in particular makes good use of it. But it’s one thing I miss the most not writing Erlang/Elixir for a living... so far. It makes functions and data handling into these clean trees instead of conditionals (not to start a language flamewar but boo Golangs conditional obsession which seems to be the polar opposite in many ways for error handling, or at least it used to be I haven’t tried it recently). There’s a lot to like and learn from in Erlang. Static typing will give it wider adoption IMO. And I’m happy to see so many developers working on it.
- amw-zero 6y ago
  What’s special about Erlang pattern matching? Haskell and ML are at least equivalent.
  - qqwy 6y ago
    They are not equivalent, as Erlang/Elixir uses structural typing whereas Haskell/ML uses nominal typing. In Erlang you can define the following: equal(X, X) -> true; equal(_, _) -> false. In Haskell, the following does not compile: equal x x = True equal _ _ = False instead, we need to write something like equal x y | x == y = True | otherwise = False A subtle difference, but in some cases the structural semantics really do make patterns a lot cleaner (shorter without sacrificing readability). I think that this style of pattern-matching semantics is a consequence of Erlang's roots in Prolog, which works similarly (and not only checks for structural equivalence but even does unification when necessary).
noxplode 6y ago
Just in case anyone here missed or hasn't seen this news: Facebook is working on a statically typed Erlang. https://twitter.com/robertoaloi/status/1304085677252935681 https://twitter.com/robertoaloi/status/1304085677252935681
- ketzo 6y ago
  Wow, that's really exciting. I spent some time over this summer working on a toy project in Elixir and really enjoyed the language, but the bigger it got the more I felt the lack of all my familiar TypeScript tools. I look forward to seeing this soon.
oltarasenko 6y ago
Great story! Really interesting experience!

134 points by leostera 6y ago

Interestingly enough, the article doesn't say anything about propagation of types, which is the crux of the type checking and what makes any typing system useful or useless, obnoxious or helpful. Consider the example from the article: % a good old list length counter count(A=[_|_]) -> count(A, 0). count([], C) -> C; count([_|T], C) -> count(T, C+1). What is the type of count/2? Arguably, it's "(list, any | number) -> any | number", which means that count/1 has type "list -> any | number". Well, that's bloody pointless, isn't it? What you probably want is "(list, any) -> any | (list, number) -> number" for count/2, so you could give count/1 its useful type "list -> number", but intersection function types are notoriously difficult to infer or typecheck, even with manual annotations.

dnautics 6y ago
If you drill down to the beam opcodes it should be possible to infer correctly that the type of count/2 can only take number in the second argument.
- Joker_vD 6y ago
  No, count/2 can sometimes take non-numbers in the second argument, behold: 1> c(test_count). {ok,test_count} 2> test_count:count([], bang). bang
  - dnautics 6y ago
    Yeah, I mean that it will properly identify that the only time you can do that is when you have an empty list. The final spec will be (in elixir syntax): (nonempty_list, number -> number) | ([], any -> any) It should also be able to correctly infer that the count/1 function must be (nonempty_list -> pos_integer) | ([] -> 0)
    - Joker_vD 6y ago
      I am using an old version of erlang, so typer infers the following types: -spec count([any()],_) -> any(). -spec count([any(),...]) -> any(). If I unexport count/2, it infers -spec count([any(),...]) -> non_neg_integer(). -spec count([any()],non_neg_integer()) -> non_neg_integer().
      - dnautics 6y ago
        I did say "should be able to" without regard to any of the existing type inference engines =D I'll be sure to make this as explicit test in Mavis Inference, which is the one I'm working on. https://github.com/ityonemo/mavis_inference/issues/47 https://github.com/ityonemo/mavis_inference/issues/47
  - yellowapple 6y ago
    I'd imagine that in this context (i.e. one where a 1-arity function initializes a tail-recursive 2-arity function) the 1-arity function is the only one that'd be exposed outside of the module, in which case you can know with reasonable certainty that only things within the current module will ever call it. If you really do need to export the 2-arity version, you could always do a meaningless addition to force it to typecheck to a number, like so: count([], C) -> C+0; count([_|T], C) -> count(T, C+1); Which should then result in the following: erl> c(test_count). {ok,test_count} erl> test_count:count([], bang). ** exception error: an error occurred when evaluating an arithmetic expression in function test_count:count/2 (test_count.erl, line 8) Or alternately, use guards (though in the context of BEAM-level introspection I haven't the slightest idea if this would produce an equivalent check): count([], C) when is_integer(C) -> C; count([_|T], C) when is_integer(C) -> count(T, C+1); Which then gets you a somewhat clearer error message: 10> c(test_count). {ok,test_count} 11> test_count:count([], bang). ** exception error: no function clause matching test_count:count([],bang) (test_count.erl, line 8)
    - Joker_vD 6y ago
      Yes, if you look at my reply to the sibling comment, you'll see that if count/2 is unexported, TypEr (apparently, that's the proper capitalization) infers the types with non_negative_integer(). In fact, I've just looked at the original TypEr paper [0], and wow, they use exactly this example in the section 6: "One might even jump to the conclusion that success typings are unnecessarily general and, as such, quite useless. However, notice that this success typing succinctly captures all possible applications of length_3 which will not result in a type error. [...] Still, we also find the situation sub-optimal and we will improve on it as explained below", and then they use exactly your proposal, recognizing that non-exported functions are only called from the exported functions, and perform dataflow analysis to constrain the types even further. [0] Tobias Lindahl and Konstantinos Sagonas, "Practical type inference based on success typings", https://www.it.uu.se/research/group/hipe/dialyzer/publications/succ_types.pdf https://www.it.uu.se/research/group/hipe/dialyzer/publicatio...

skohan 6y ago

I really want to like Erlang because the priorities and USP's of the language are super compelling for a lot of use-cases. I tried to kick the tires on it a couple years ago, and what I found is that the error messages were just so vexing, and it took a minute to understand what they meant, even in toy examples. Maybe it gets better with time, or there is tooling to help with this, but it seemed a bit behind the times with the standard which has been set by more modern programming languages.

cpursley 6y ago
Give Elixir a spin.
- deleted 6y ago
  [deleted]
- dognotdog 6y ago
  I'd second that, Elixir does away with the sometimes vexing comma and dot syntax used for scoping. Also, it does have mutable variables. You do have to get to grips with pattern matching and processes as objects being such core concepts, but I found that once I got it, it is wonderful.
  - dnautics 6y ago
    Just to clarify: Values in elixir are still immutable. The core team will insist that variables are immutable but bindings are mutable, but in my mind variables are their bindings (there is not a third category distinct from the value and the lexical binding). I think there is huge debate as to whether this is good or bad - I think though you really really want to have mutable variables in the REPL. In your static code it's trivial to check for variable rebinding and be sure you're not doing it (credo makes this easy to set up)
    - wtetzner 6y ago
      Variables in Elixir are not mutable, they can just be rebound. Think 'let' in Scheme or ML.

huseyinkeles 6y ago

I'd recommend anyone who have troubles with outdatedness (?) of the Erlang, to try Elixir. It runs on Erlang virtual machine, very modern and pleasure to code in.

dnautics 6y ago

I'm currently actively working on a typechecking system for elixir (three packages: https://github.com/ityonemo/selectrix https://github.com/ityonemo/selectrix for compile-time interface, ../mavis for type logic, and ../mavis_inference for performing type inference on compiled code). The chief difficulties I am running into are: 1) How to do intersections on functions and maps (this is in the article): f(integer) -> integer is not usable as f(any) -> integer 2) not all of the erlang bytecode instructions are well documented 3) I still haven't figured out how to deal with circular dependencies at the module level. Erlang makes this easy in these ways: 1) compiled module structure is simple and the way branching works makes the mechanics of type inference trivial. 2) erlangs concurrency makes dealing with, for example in-module dependencies trivial 3) there are only a handful of types in erlang so, aside from functions, their subtyping relationships are very straightforward. Elixir makes this easy in these ways: 1) Typechecking structs can be more straightforward than records. 2) Writing a composable type logic (mavis) is super easy with elixir's protocols 3) I built (and am refining) a very easy dsl that makes creating and testing logic for the beam opcodes less of a hair-tearing experience: https://github.com/ityonemo/mavis_inference/blob/main/lib/type.inference/opcodes/gc_bif.ex https://github.com/ityonemo/mavis_inference/blob/main/lib/ty...

FrankBro 6y ago
I'm going to shill Gradualizer[1] in here as well. 1. I think you have to see typing as helpful information. Like: -spec add(integer(), integer()) -> integer(). add(A, B) -> A + B. Technically, nothing prevents add from accepting number() or float(). It's too much specification. 2. I was surprised how much there actually is but also disappointed that a lot of errors were in until OTP 23. Gradualizer also overrides some definitions [2] 3. Haven't encountered a problem with this yet with gradualizer, would need to test. [1] https://github.com/josefs/Gradualizer https://github.com/josefs/Gradualizer [2] https://github.com/josefs/Gradualizer/blob/master/priv/prelude/lists.specs.erl https://github.com/josefs/Gradualizer/blob/master/priv/prelu...
- dnautics 6y ago
  Yeah, I had thought that development of Gradualizer had halted, glad to see it's not. Part of why I wanted to do Mavis is because I wanted to make it easy for developers to make their own custom overrides and ship it with their libraries, especially for Elixir protocols[0]. still haven't figured out how to architect that, but I have an idea. > I think you have to see typing as helpful information Indeed. Selectrix will allow you to chain your inference with fallbacks, so, maybe the first level is a fast cache, second level is checking files for user overrides, third level is dialyzer specs, fourth level is inference. I think it should also be possible to create an addon module with Mavis that lets you type inbound messages for GenServers, given a set of constraints (all possible calls and casts are present in the module itself as an API) [0] it's a big problem that in elixir, Enumerable protocol destroys typing information, so I want to make an typing override for Enumerable an "example" typing override system.

Snitch-Thursday 6y ago

I'm watching Gleam[1] for my 'I want to learn Erlang but dont want to deal with having to do runtime type checks so I wish there was a Statically-Typed Erlang' dreams. [1] https://gleam.run/news/gleam-v0.12-and-gleam-otp-v0.1-released/ https://gleam.run/news/gleam-v0.12-and-gleam-otp-v0.1-releas...

dnautics 6y ago
I think that devon estes has a point that it is likely that trying to graft a foreign typesytem onto the BEAM is not a good idea. I'm glad someone is trying, though.
- modernerd 6y ago
  I think the tweet was deleted but it's cached here, for others like me who had not seen Devon's take: https://webcache.googleusercontent.com/search?q=cache:JkQRkuQWRL8J:https://twitter.com/devoncestes/status/1307042045693956099+&cd=2&hl=en&ct=clnk&gl=at https://webcache.googleusercontent.com/search?q=cache:JkQRku...
  - tym0 6y ago
    Thanks for sharing. To save people a click the author of the tweet is opposed to adding a type system to Elixir not the BEAM, he seems to be seeing project like Gleam in a positive light.
mastermind1014 6y ago
Check out Caramel [1] as well - [1] https://github.com/AbstractMachinesLab/caramel https://github.com/AbstractMachinesLab/caramel
- mikhailfranco 6y ago
  and Hamler too ... https://www.hamler-lang.org https://www.hamler-lang.org https://github.com/hamler-lang https://github.com/hamler-lang https://news.ycombinator.com/item?id=23491516 https://news.ycombinator.com/item?id=23491516

FrankBro 6y ago

I replied to your post on twitter but I highly recommend Gradualizer[1]. Discovered it last year and started using it. The refinement portion handles unions and guards very well. It's not perfect but I'm integrating it in our codebase with some interesting successes. I'm hoping more people use it on their codebase and can find any bugs they have with it so it can be improved further. [1] https://github.com/josefs/Gradualizer https://github.com/josefs/Gradualizer

sharno 6y ago

WhatsApp is supposed to release an Erlang typechecker this month, I thinking it’d be good to see how they handle this

Ndymium 6y ago
It has been delayed: https://elixirforum.com/t/facebook-is-writing-a-new-statically-typed-language-to-run-on-the-beam/29829/34?u=nicd https://elixirforum.com/t/facebook-is-writing-a-new-statical...

dmix 6y ago

> all sorts of pattern matching Outside of the famous builtin process model/BEAM (plus the subsequent ‘crash first’ style design of programs which adds resiliency) the pattern matching is what makes Erlang one of the best languages and the one thing I wish every new language copied. You kinda get it in Haskell and Rust with the maybe style pattern matching. Rust in particular makes good use of it. But it’s one thing I miss the most not writing Erlang/Elixir for a living... so far. It makes functions and data handling into these clean trees instead of conditionals (not to start a language flamewar but boo Golangs conditional obsession which seems to be the polar opposite in many ways for error handling, or at least it used to be I haven’t tried it recently). There’s a lot to like and learn from in Erlang. Static typing will give it wider adoption IMO. And I’m happy to see so many developers working on it.

amw-zero 6y ago
What’s special about Erlang pattern matching? Haskell and ML are at least equivalent.
- qqwy 6y ago
  They are not equivalent, as Erlang/Elixir uses structural typing whereas Haskell/ML uses nominal typing. In Erlang you can define the following: equal(X, X) -> true; equal(_, _) -> false. In Haskell, the following does not compile: equal x x = True equal _ _ = False instead, we need to write something like equal x y | x == y = True | otherwise = False A subtle difference, but in some cases the structural semantics really do make patterns a lot cleaner (shorter without sacrificing readability). I think that this style of pattern-matching semantics is a consequence of Erlang's roots in Prolog, which works similarly (and not only checks for structural equivalence but even does unification when necessary).

noxplode 6y ago

Just in case anyone here missed or hasn't seen this news: Facebook is working on a statically typed Erlang. https://twitter.com/robertoaloi/status/1304085677252935681 https://twitter.com/robertoaloi/status/1304085677252935681

ketzo 6y ago
Wow, that's really exciting. I spent some time over this summer working on a toy project in Elixir and really enjoyed the language, but the bigger it got the more I felt the lack of all my familiar TypeScript tools. I look forward to seeing this soon.

oltarasenko 6y ago

Great story! Really interesting experience!