4 ms·

The problem all extant typing systems for message passing (in particular session types) have is that they cannot really deal well with data dependent patterns

The problem all extant typing systems for message passing (in particular session types) have is that they cannot really deal well with data dependent patterns of message passing. Erlang's mailbox-based message passing is especially prone to data dependent patterns of message passing. Yes, you can add enough expressive power to the typing system to make this work (e.g. dependent types), but then it stops being pragmatically viable, as far as we know in 2019.

AnaniasAnanas 8y ago
Claiming that dependent types are not pragmatically viable is quite a bold claim, would you mind backing it up? My experience with them so far has been more than great.
- YorkshireSeason 8y ago
  Nothing bold about it, here is some evidence. - No type inference, since that's not decidable for dependent types. - In most industrial software engineering, getting the specifications is a big problem, whence agile methods. Without detailed specifications early on in a software project's lifecycle, what's the point of paying the price for type dependency when you don't even use it. - Relatedly, dependent types don't solve the oracle problem in software engineering: i.e. where do you get the specs from and how do you know that your specs (in this case types) are correct rather than false? - Rewriting & refactoring code becomes much more expensive, because you now also have to rewrite / refactor the specifications. (This is already a reason why post-Java, exception specifications have been abandoned) - No widely used programming language offers full dependent types (yes I'm aware of Scala's path dependent types and Haskell's forays into dependency), and that despite dependent types are at least half a century old [1]. So it's not like programming language designers don't know about them. - Dependent types have really only been worked out beyond research prototypes for functional languages, not e.g. for message passing concurrency. My experience with them so far has been more than great. I'd be interested to learn what non-trivial code you've written in dependently typed programming languages. By non-trivial, I mean: industrial code, say > 20k LoCs, at least 3 programmers involved, specification changed over time. Specification was not fully available at the start of the project. [1] N. de Bruijn, Automath, a language for mathematics.
  - AnaniasAnanas 8y ago
    > - No type inference, since that's not decidable for dependent types. You can still have type inference, it just won't be able to infer the type of all valid terms, in which case you just have to add a manual annotation. This is not a strange concept, this is what haskell does for example with higher ranked types. > getting the specifications is a big problem You do not need to specify what the whole program will do (in fact you can use a language with dependent types without having to specify anything at all) - that being said, people usually specify the behavior of specific functions in the program. > - Relatedly, dependent types don't solve the oracle problem in software engineering: i.e. where do you get the specs from and how do you know that your specs (in this case types) are correct rather than false? I thought that the point of erlang having dependent types would be to make data-dependent code easier, not to specify the behavior of functions. But yes, this is correct, and this holds true with every proof assistant that I am aware, not only with the ones that use dependent types. > because you now also have to rewrite / refactor the specifications This is a great thing actually - I would consider it a bug if my function after a refactoring did something that went against its specification, with dependent types I can have the compiler warn me about it. But again, you are not forced to write a specification. Dependent types only add possibilities without removing anything. > So it's not like programming language designers don't know about them. I would argue that most programming language designers are not familiar with type theory. There are thousands of languages, one does not need to be a genius to make one. Heck, two of the most popular languages (C and Go) do not even have parametric polymorphism, not to mention that generics were added in Java only in 2004. In addition to that pretty much no popular language has proper support for higher order types either. > industrial code, 20k LoCs, at least 3 programmers involved, specification changed over time. Specification was not fully available at the start of the project. In that case, none. Though I would argue that your standards are too high, after all just the fact that I have not worked in the software industry excludes anything that I have made. As for LoC, I would not use it to measure the scale of a project. With Java for example even the most trivial program can easily reach thousands of lines.
    - YorkshireSeason 8y ago
      most programming language designers are not familiar with type theory. SPJ, Odersky, Leroy, Hejlsberg, Syme et al are familiar with type theory, it's not rocket science. parametric polymorphism There are well-rehearsed reasons for excluding PP. I don't agree with them, but those choices were not made from ignorance. I have not worked in the software industry I invite you to change this, and once you have a few years of industrial programming experience, to reconsider.

AnaniasAnanas 8y ago

Claiming that dependent types are not pragmatically viable is quite a bold claim, would you mind backing it up? My experience with them so far has been more than great.

YorkshireSeason 8y ago
Nothing bold about it, here is some evidence. - No type inference, since that's not decidable for dependent types. - In most industrial software engineering, getting the specifications is a big problem, whence agile methods. Without detailed specifications early on in a software project's lifecycle, what's the point of paying the price for type dependency when you don't even use it. - Relatedly, dependent types don't solve the oracle problem in software engineering: i.e. where do you get the specs from and how do you know that your specs (in this case types) are correct rather than false? - Rewriting & refactoring code becomes much more expensive, because you now also have to rewrite / refactor the specifications. (This is already a reason why post-Java, exception specifications have been abandoned) - No widely used programming language offers full dependent types (yes I'm aware of Scala's path dependent types and Haskell's forays into dependency), and that despite dependent types are at least half a century old [1]. So it's not like programming language designers don't know about them. - Dependent types have really only been worked out beyond research prototypes for functional languages, not e.g. for message passing concurrency. My experience with them so far has been more than great. I'd be interested to learn what non-trivial code you've written in dependently typed programming languages. By non-trivial, I mean: industrial code, say > 20k LoCs, at least 3 programmers involved, specification changed over time. Specification was not fully available at the start of the project. [1] N. de Bruijn, Automath, a language for mathematics.
- AnaniasAnanas 8y ago
  > - No type inference, since that's not decidable for dependent types. You can still have type inference, it just won't be able to infer the type of all valid terms, in which case you just have to add a manual annotation. This is not a strange concept, this is what haskell does for example with higher ranked types. > getting the specifications is a big problem You do not need to specify what the whole program will do (in fact you can use a language with dependent types without having to specify anything at all) - that being said, people usually specify the behavior of specific functions in the program. > - Relatedly, dependent types don't solve the oracle problem in software engineering: i.e. where do you get the specs from and how do you know that your specs (in this case types) are correct rather than false? I thought that the point of erlang having dependent types would be to make data-dependent code easier, not to specify the behavior of functions. But yes, this is correct, and this holds true with every proof assistant that I am aware, not only with the ones that use dependent types. > because you now also have to rewrite / refactor the specifications This is a great thing actually - I would consider it a bug if my function after a refactoring did something that went against its specification, with dependent types I can have the compiler warn me about it. But again, you are not forced to write a specification. Dependent types only add possibilities without removing anything. > So it's not like programming language designers don't know about them. I would argue that most programming language designers are not familiar with type theory. There are thousands of languages, one does not need to be a genius to make one. Heck, two of the most popular languages (C and Go) do not even have parametric polymorphism, not to mention that generics were added in Java only in 2004. In addition to that pretty much no popular language has proper support for higher order types either. > industrial code, 20k LoCs, at least 3 programmers involved, specification changed over time. Specification was not fully available at the start of the project. In that case, none. Though I would argue that your standards are too high, after all just the fact that I have not worked in the software industry excludes anything that I have made. As for LoC, I would not use it to measure the scale of a project. With Java for example even the most trivial program can easily reach thousands of lines.
  - YorkshireSeason 8y ago
    most programming language designers are not familiar with type theory. SPJ, Odersky, Leroy, Hejlsberg, Syme et al are familiar with type theory, it's not rocket science. parametric polymorphism There are well-rehearsed reasons for excluding PP. I don't agree with them, but those choices were not made from ignorance. I have not worked in the software industry I invite you to change this, and once you have a few years of industrial programming experience, to reconsider.