3 ms·

Different type system with different goals. Gleam uses a modified version of the Hindley-Milner Type system. (Which is a rock solid tested type system.) A Set

Different type system with different goals. Gleam uses a modified version of the Hindley-Milner Type system. (Which is a rock solid tested type system.) A Set theoretical type system is more expressive(which suits the dynamic nature or Elixir better.) You can do Union and Intersection Types, and Negation Types, among other things, that you can't do with a HM type system. but it comes at the cost of how fast the program can be typed. HM types systems have amazing type inference capabilities and do so at O(n). Im not sure what the time complexity of the algorithm they are using to do the type checking for Elixir programs, but I bet it's more expensive than that. (Which is probably why they are rolling out the type system slowly.)

tiffanyh 2y ago
Does Gleam check types at compile-time? And Elixir check types at run-time? (If at run-time, would that mean it would slow down your entire app as a result?)
- arrowsmith 2y ago
  Elixir checks at compile time.
- bo0tzz 2y ago
  My understanding is that the BEAM vm already has some (optional) runtime typechecks in the form of guards, which this new typesystem will also add for you automatically. And that these guards are actually used to speed things up, for example by JITing more optimized code.
  - throwawaymaths 2y ago
    So inserting those type checks automatically will cause regressions because those checks are not free at runtime, and there are cases where the JIT will look at the code and not bother optimizing.
    - dub_gui 2y ago
      To clarify, the type-checker does not modify compilation to the beam at all. Instead, it takes into account the predicted runtime checks to inject more static types into its analysis. For instance, without even introducing annotations, if a function head has a guard `is_boolean(x)`, using the + operator on x within that function would lead to a type error.
      - throwawaymaths 2y ago
        exactly. The potential performance regression of guards is exactly why the elixir typechecker doesn't insert them. I guess I hadn't made that point clear in my comment. IIRC The elixir guides talks about excessive typechecking being a code smell.
- davydog187 2y ago
  Both the Elixir and Gleam type systems run at compile time (and whenever you recompile during development) There are no plans for runtime checking AFAIK
nerdponx 2y ago
> A Set theoretical type system is more expressive(which suits the dynamic nature or Elixir better.) You can do Union and Intersection Types, and Negation Types, among other things, that you can't do with a HM type system. but it comes at the cost of how fast the program can be typed. I doubt that Python's static type hints existing within a formal mathematical framework, but it's interesting that intersection types have been under consideration for a long time now: https://github.com/python/typing/issues/213 https://github.com/python/typing/issues/213
cobbal 2y ago
HM is worst-case exponential, but it just happens to have good performance in practice.
throwawaymaths 2y ago
It's also not clear that an h-m type system is what people want. For example, checking json inputs in gleam will always either be awkward or behind a "marshaller for me but not for thee" sort of inside-ball stuff, and the interface with other members of the beam ecosystem will be poor. It is possible to build a set theoretic type system without these problems, but I don't see these cases being handled by elixir's type system, either.

tiffanyh 2y ago

Does Gleam check types at compile-time? And Elixir check types at run-time? (If at run-time, would that mean it would slow down your entire app as a result?)

arrowsmith 2y ago
Elixir checks at compile time.
bo0tzz 2y ago
My understanding is that the BEAM vm already has some (optional) runtime typechecks in the form of guards, which this new typesystem will also add for you automatically. And that these guards are actually used to speed things up, for example by JITing more optimized code.
- throwawaymaths 2y ago
  So inserting those type checks automatically will cause regressions because those checks are not free at runtime, and there are cases where the JIT will look at the code and not bother optimizing.
  - dub_gui 2y ago
    To clarify, the type-checker does not modify compilation to the beam at all. Instead, it takes into account the predicted runtime checks to inject more static types into its analysis. For instance, without even introducing annotations, if a function head has a guard `is_boolean(x)`, using the + operator on x within that function would lead to a type error.
    - throwawaymaths 2y ago
      exactly. The potential performance regression of guards is exactly why the elixir typechecker doesn't insert them. I guess I hadn't made that point clear in my comment. IIRC The elixir guides talks about excessive typechecking being a code smell.
davydog187 2y ago
Both the Elixir and Gleam type systems run at compile time (and whenever you recompile during development) There are no plans for runtime checking AFAIK

nerdponx 2y ago

> A Set theoretical type system is more expressive(which suits the dynamic nature or Elixir better.) You can do Union and Intersection Types, and Negation Types, among other things, that you can't do with a HM type system. but it comes at the cost of how fast the program can be typed. I doubt that Python's static type hints existing within a formal mathematical framework, but it's interesting that intersection types have been under consideration for a long time now: https://github.com/python/typing/issues/213 https://github.com/python/typing/issues/213

cobbal 2y ago

HM is worst-case exponential, but it just happens to have good performance in practice.

throwawaymaths 2y ago

It's also not clear that an h-m type system is what people want. For example, checking json inputs in gleam will always either be awkward or behind a "marshaller for me but not for thee" sort of inside-ball stuff, and the interface with other members of the beam ecosystem will be poor. It is possible to build a set theoretic type system without these problems, but I don't see these cases being handled by elixir's type system, either.