5 ms·

Agreed, I loved working in Elixir but hated the typespecs. Felt like it was a lot of work for only a little benefit. It's not typing that I don't like but the w

Agreed, I loved working in Elixir but hated the typespecs. Felt like it was a lot of work for only a little benefit. It's not typing that I don't like but the way it's implemented in Elixir felt like it was very hard to get correct quickly. Very fiddly and time consuming. About the 10th time Dialyzer broke the build for no easily discernible reason, I wanted to scrap it.

dnautics 6y ago
I wouldn't go so far as to say they aren't useful. I find dialyzer is not awful at finding mistakes that I make. I have thought about this a lot (I'm writing a static typechecking library for Elixir) and really the problem is the dialyzer typesystem. Almost all of the problems stem from the root fact that there isn't a granular concept of how to treat functions in the type system. What does `(int, int) -> int` mean? Dialyzer does not have a good answer for that question. Mind you I am not a "PL theory" type of guy, I do have a math degree, but my PhD is in the sciences, so I am more approaching this issue from a "discovering what would be truly useful" perspective more than "applying an existing typesystem to the BEAM", which is I think in line with the traditional pragmatism of the BEAM ecosystem.
- lpil 6y ago
  > What does `(int, int) -> int` mean? This is an interesting question. Do you have any thoughts on what a better answer to that question might mean? Or languages you think do better here? Thank you
  - dnautics 6y ago
    Here's my thought: let's go with a simpler one: int -> int "I guarantee that if you send me an int then i will return you an int without crashing" In elixirland: `IO.inspect/1` would satisfy this, as would `Kernel.-/1`. The interesting thing is that `any -> int` is then a subtype of `int -> int` and we need a new type `_ -> int` which is "any one-arity function that emits int". Then types become a statement of "resistance to crashing" in the BEAM vm, which I think is the useful thing that people are looking for. I don't have answers to everything; I don't know how to deal with a function that generates random numbers from 1 to 20 and crashes on 13, for example. We should have a discussion about this! I'll reach out on another channel.
    - tom_mellior 6y ago
      I have no skin in this game, but: > "I guarantee that if you send me an int then i will return you an int without crashing" This is a much stronger guarantee than you get in any language except very specialized ones. Coq, for example (not just not crashing, but also guaranteed termination). But even in Haskell an Int -> Int function can crash or decide not to terminate. Reading more into a type opens up cans of worms that are hard to solve.
      - lpil 6y ago
        I think you can usefully tackle this problem without too much difficulty. At least, within a langauge like Gleam you can. An effects tracking system can be used to determine things such as use of FFI, `assert`, recursion, and side effects. With these statements like "this function does not crash" is easy, and "this function does not diverge" is also possible, though it will not detect all functions that do not diverge.
      - dnautics 6y ago
        Ok so aside from well known out of control things like another process telling the vm to brutal_kill you, cosmic arrays, or miscodes, OS interactions, oom errors or nif panics (the last three which bring down the whole VM anyways, so who cares), the crashing surface error for a BEAM process is extremely well defined. The only no_returns otherwise are loops and hibernates. Hibernates are explicit. You might have a hard time analyzing the tail-calls to figure out an ultimate type that captures a no_return loop, but I think ignoring that condition would not be horrible for a BEAM type system (along the same lines as the random number crash scenario that I described).
        tom_mellior 6y ago
        > Ok so aside from well known out of control things like another process telling the vm to brutal_kill you, cosmic arrays, or miscodes [...] the crashing surface error for a BEAM process is extremely well defined. I'm not sure what you're saying. Crashing "miscodes" (like pattern match failures) are a thing, no? A "well defined" thing, but not one that a type system that doesn't include proper theorem proving will save you from.
devoutsalsa 6y ago
As dumb as this sounds... you can use typespecs as documentation even if you never run dializer. We do this at work in a legacy code base that would be painful to dialyze without errors, but it makes new code nicer to look at.
- warmwaffles 6y ago
  I use it exactly for this. Just use typespecs as a hint to the person looking at the code as to what is expected to be passed.
  - bcrosby95 6y ago
    If you never do anything but read them... why not documentation?
    - slindz 6y ago
      Terseness.
      - devoutsalsa 6y ago
        Yup. One could write "It takes a string as an argument & reverses it". Or one could write "String.reverse(()". For any non trivial case, such as weird options, you'll normally write documentation anyway.
    - warmwaffles 6y ago
      I do both. All to help me in the future as much as possible when I come back scratching my head.
- rkangel 6y ago
  Isn't there a big risk the typespecs are wrong then?

dnautics 6y ago

I wouldn't go so far as to say they aren't useful. I find dialyzer is not awful at finding mistakes that I make. I have thought about this a lot (I'm writing a static typechecking library for Elixir) and really the problem is the dialyzer typesystem. Almost all of the problems stem from the root fact that there isn't a granular concept of how to treat functions in the type system. What does `(int, int) -> int` mean? Dialyzer does not have a good answer for that question. Mind you I am not a "PL theory" type of guy, I do have a math degree, but my PhD is in the sciences, so I am more approaching this issue from a "discovering what would be truly useful" perspective more than "applying an existing typesystem to the BEAM", which is I think in line with the traditional pragmatism of the BEAM ecosystem.

lpil 6y ago
> What does `(int, int) -> int` mean? This is an interesting question. Do you have any thoughts on what a better answer to that question might mean? Or languages you think do better here? Thank you
- dnautics 6y ago
  Here's my thought: let's go with a simpler one: int -> int "I guarantee that if you send me an int then i will return you an int without crashing" In elixirland: `IO.inspect/1` would satisfy this, as would `Kernel.-/1`. The interesting thing is that `any -> int` is then a subtype of `int -> int` and we need a new type `_ -> int` which is "any one-arity function that emits int". Then types become a statement of "resistance to crashing" in the BEAM vm, which I think is the useful thing that people are looking for. I don't have answers to everything; I don't know how to deal with a function that generates random numbers from 1 to 20 and crashes on 13, for example. We should have a discussion about this! I'll reach out on another channel.
  - tom_mellior 6y ago
    I have no skin in this game, but: > "I guarantee that if you send me an int then i will return you an int without crashing" This is a much stronger guarantee than you get in any language except very specialized ones. Coq, for example (not just not crashing, but also guaranteed termination). But even in Haskell an Int -> Int function can crash or decide not to terminate. Reading more into a type opens up cans of worms that are hard to solve.
    - lpil 6y ago
      I think you can usefully tackle this problem without too much difficulty. At least, within a langauge like Gleam you can. An effects tracking system can be used to determine things such as use of FFI, `assert`, recursion, and side effects. With these statements like "this function does not crash" is easy, and "this function does not diverge" is also possible, though it will not detect all functions that do not diverge.
    - dnautics 6y ago
      Ok so aside from well known out of control things like another process telling the vm to brutal_kill you, cosmic arrays, or miscodes, OS interactions, oom errors or nif panics (the last three which bring down the whole VM anyways, so who cares), the crashing surface error for a BEAM process is extremely well defined. The only no_returns otherwise are loops and hibernates. Hibernates are explicit. You might have a hard time analyzing the tail-calls to figure out an ultimate type that captures a no_return loop, but I think ignoring that condition would not be horrible for a BEAM type system (along the same lines as the random number crash scenario that I described).
      - tom_mellior 6y ago
        > Ok so aside from well known out of control things like another process telling the vm to brutal_kill you, cosmic arrays, or miscodes [...] the crashing surface error for a BEAM process is extremely well defined. I'm not sure what you're saying. Crashing "miscodes" (like pattern match failures) are a thing, no? A "well defined" thing, but not one that a type system that doesn't include proper theorem proving will save you from.

devoutsalsa 6y ago

As dumb as this sounds... you can use typespecs as documentation even if you never run dializer. We do this at work in a legacy code base that would be painful to dialyze without errors, but it makes new code nicer to look at.

warmwaffles 6y ago
I use it exactly for this. Just use typespecs as a hint to the person looking at the code as to what is expected to be passed.
- bcrosby95 6y ago
  If you never do anything but read them... why not documentation?
  - slindz 6y ago
    Terseness.
    - devoutsalsa 6y ago
      Yup. One could write "It takes a string as an argument & reverses it". Or one could write "String.reverse(()". For any non trivial case, such as weird options, you'll normally write documentation anyway.
  - warmwaffles 6y ago
    I do both. All to help me in the future as much as possible when I come back scratching my head.
rkangel 6y ago
Isn't there a big risk the typespecs are wrong then?