4 ms·

Eqwalizer: A Type-Checker for Erlang

86 points by hasheddan 4y ago

throwawaymaths 4y ago
Did they really implement the type system in scala!!? (If someone knows better I'd love to know! The readme is awful short on details)
- emptysea 4y ago
  Yeah that’s interesting. Flow uses OCaml, ditto for their Python type checker. Hack is C++, and Relay uses Rust. (Although I think some of the other type checkers are migrating from OCaml to Rust). Curious about the perf implications with using a JVM language for a compiler vs native.
  - throwawaymaths 4y ago
    Forget about perf. Who wants to import a separate stack to get a sidecar tool. Separately, if you're an elixir user this would mean you can't easily hook it into say compiler callbacks (though if I'm reading this code directly it reads Erlang ast -- I tried doing a typechecker for elixir ast, and decided that reading bytecode was a better choice since it's simpler)
    - throwaway81523 4y ago
      Starting with bytecode seems harder because you no longer know what the expression terms are. So they are harder (impossible?) to typecheck.
      - throwawaymaths 4y ago
        You type the registers as data flows through them. It's easier, trust me. Both Erlang and especially elixir puts a whole lot of sugar on top of the low level instructions which can make reasoning about data structures harder. And as a bonus it works with all beam languages.
        throwaway81523 4y ago
        Hmm ok, I'll take your word for it. There is another issue too though, which is that the BEAM itself is being replaced with a native-code VM. I don't know if the compiler for that starts with bytecode.
        throwawaymaths 4y ago
        I think you're confused. Not architecture (x86, arm) bytecode, BEAM bytecode. Erlang compiles down to An intermediate bytecode like java does.
throwaway81523 4y ago
I'm surprised Erlang fits into that strict static model. I have thought it better to make a language that is typed from the get-go, that compiles to BEAM. That has been done at least a few times: Purescript has a BEAM back end, and there was something called Alpaca that is more ML-like.
- rkangel 4y ago
  The leading contender for type safe languages on the BEAM at the moment seems to be Gleam: https://gleam.run/ https://gleam.run/ It's looking very promising Adding a type checker to Erlang does make some sense, in the same way that adding types to Python makes sense. It adds to the checking in areas where you're added types while allowing perfect interop with the rest of the world.
patrec 4y ago
Interesting. My limited experimentation suggests to me that dialyzer is completely useless for non-toy code. As in you run it on some mid-sized type-annotated code and you get to powercycle your linux-box, because dialyzer's gonna gobble up so many dozen gigabytes of RAM that linux's braindamaged memory management will soon swap your machine to death. So would be nice to see some competition in this space.
- throwaway81523 4y ago
  I found dialyzer usable in a moderate sized VM (idr the exact size). The issue that I had with it is that it left too many errors undetected. It was better than nothing though.

86 points by hasheddan 4y ago

Did they really implement the type system in scala!!? (If someone knows better I'd love to know! The readme is awful short on details)

emptysea 4y ago
Yeah that’s interesting. Flow uses OCaml, ditto for their Python type checker. Hack is C++, and Relay uses Rust. (Although I think some of the other type checkers are migrating from OCaml to Rust). Curious about the perf implications with using a JVM language for a compiler vs native.
- throwawaymaths 4y ago
  Forget about perf. Who wants to import a separate stack to get a sidecar tool. Separately, if you're an elixir user this would mean you can't easily hook it into say compiler callbacks (though if I'm reading this code directly it reads Erlang ast -- I tried doing a typechecker for elixir ast, and decided that reading bytecode was a better choice since it's simpler)
  - throwaway81523 4y ago
    Starting with bytecode seems harder because you no longer know what the expression terms are. So they are harder (impossible?) to typecheck.
    - throwawaymaths 4y ago
      You type the registers as data flows through them. It's easier, trust me. Both Erlang and especially elixir puts a whole lot of sugar on top of the low level instructions which can make reasoning about data structures harder. And as a bonus it works with all beam languages.
      - throwaway81523 4y ago
        Hmm ok, I'll take your word for it. There is another issue too though, which is that the BEAM itself is being replaced with a native-code VM. I don't know if the compiler for that starts with bytecode.
        throwawaymaths 4y ago
        I think you're confused. Not architecture (x86, arm) bytecode, BEAM bytecode. Erlang compiles down to An intermediate bytecode like java does.

throwaway81523 4y ago

I'm surprised Erlang fits into that strict static model. I have thought it better to make a language that is typed from the get-go, that compiles to BEAM. That has been done at least a few times: Purescript has a BEAM back end, and there was something called Alpaca that is more ML-like.

rkangel 4y ago
The leading contender for type safe languages on the BEAM at the moment seems to be Gleam: https://gleam.run/ https://gleam.run/ It's looking very promising Adding a type checker to Erlang does make some sense, in the same way that adding types to Python makes sense. It adds to the checking in areas where you're added types while allowing perfect interop with the rest of the world.

patrec 4y ago

Interesting. My limited experimentation suggests to me that dialyzer is completely useless for non-toy code. As in you run it on some mid-sized type-annotated code and you get to powercycle your linux-box, because dialyzer's gonna gobble up so many dozen gigabytes of RAM that linux's braindamaged memory management will soon swap your machine to death. So would be nice to see some competition in this space.

throwaway81523 4y ago
I found dialyzer usable in a moderate sized VM (idr the exact size). The issue that I had with it is that it left too many errors undetected. It was better than nothing though.