5 ms·

> Then how do you explain the existence of e.g. Idris or Dotty? Have fun convincing people to port their existing Haskell and Scala programs to Idris and Dotty

> Then how do you explain the existence of e.g. Idris or Dotty? Have fun convincing people to port their existing Haskell and Scala programs to Idris and Dotty, respectively. In particular, Idris is not even remotely similar to Haskell beyond the syntax - it even uses a different evaluation strategy! > They don't feel like a workaround. They feel like a nice way of modelling my problems that has the properties that I want. The trouble with Haskell and Scala-like higher-kinded type constructors is that they are merely parameterized by other type constructors, rather than by entire structures. (It is as if, in mathematics, all functors were functors from Set!) Haskell and Scala attempt to remedy this situation using type classes, i.e., identifying every type constructor `T` with a canonical structure whose carrier is `T`. But, what if you need to use two different algebraic structures, both having `T` as their carrier? For example, say you need to use maps whose keys are lexicographically ordered strings, as well as maps whose keys are colexicographically ordered strings. Do you create a `newtype` wrapper as in Haskell? Or do you use different implicits in different contexts, and risk conflating maps created in one context with maps created in the other? This problem doesn't exist in ML, because functors allow you to parameterize entire structures by other entire structures, not just their carriers. > Maybe there are other ways, but if those other ways work then why aren't we seeing them in industry? What do I know. Ask the industry, not me. > I use a combination of trusting the compiler's typechecking, Trust is neither here nor there. Without concrete type safety theorems (“such and such doesn't happen in a typable program”), you don't even know what type checking is supposed to buy you. > sticking to the scalazzi safe subset and enforcing with linters etc., manual review of recursion (limiting the cases where it occurs as far as possible) and fast and loose reasoning. That's a perfectly fine set of software development practices, but it's not verification. > I don't have a proof of soundness, but plenty of verification systems don't have that. Then all you have is a fancy linter. > More to the point, there's nothing fundamental about Scala that makes it impossible to incorporate linear algebra without array bounds checks at runtime into the language. Um, the inability to statically verify array index manipulation using Scala's type system? > "Without array bounds checks at runtime" is not a real requirement. Not paying the runtime cost of superfluous runtime checks is absolutely a real requirement in my current job. > More to the point, there's nothing fundamental about Scala that makes it impossible to incorporate linear algebra without array bounds checks at runtime into the language. It can't be implemented as an ordinary library in the existing Scala language without relying on unsafe features (e.g., a C FFI). Doing this safely requiers bona fide dependent types - in spite of their name, so-called “path-dependent types” are just fancy first-class existentials.

lmm 9y ago
Thanks for the reply > Without concrete type safety theorems (“such and such doesn't happen in a typable program”), you don't even know what type checking is supposed to buy you. What kind of safety theorem should I be looking for? I mean, what I generally want is something like "if an expression of type A evaluates, the result will be a valid thing of type A i.e. a value constructed by one of the constructors I defined for values of type A". Or perhaps it would be better expressed via elimination - "if I provide eliminators for all my constructors for type A then I can eliminate any expression of type A". I kind of want a "the system will never magic up an A out of nowhere" result, but AIUI I can never get that because I can't have a proof of consistency of the system, no? > Doing this safely requiers bona fide dependent types - in spite of their name, so-called “path-dependent types” are just fancy first-class existentials. What is it that we can't do currently? I mean, I can define a natural number type, I can convert between values and types in both directions. I can't use ad-hoc polymorphism with a type defined at runtime (the types I form at runtime must be phantom) but I wouldn't expect to do that in well-behaved code in the first place? The only way I can see for a type to ever get into code, in any language, is either through a literal or a cast, and both those approaches are open to me in Scala. What am I missing?
- catnaroek 9y ago
  > What kind of safety theorem should I be looking for? I mean, what I generally want is something like "if an expression of type A evaluates, the result will be a valid thing of type A i.e. a value constructed by one of the constructors I defined for values of type A". This is probably sufficient for a Coq-style proof assistant, but from a general-purpose programming language I expect more. See below. > I kind of want a "the system will never magic up an A out of nowhere" result, but AIUI I can never get that because I can't have a proof of consistency of the system, no? A type system can and should guarantee that you can't create values of a (positive) type other than by using the type's introuction forms. > What is it that we can't do currently? (0) The obvious: Be sure your program won't attempt to read from or write to a close file. (1) Obtain an arbitrary integer `n`. Test once whether it is a valid array index. If the test succeeds, use `n` arbitrarily often as an array index, without any further bounds-checking. (2) Obtain three `foo.Index` values `a,b,c`. Test once whether the arrays `foo` and `bar` have the same length. Use `a,b,c` arbitrarily often as values of type `bar.Index`, without any further bounds-checking. etc. etc. etc. > The only way I can see for a type to ever get into code, in any language, is either through a literal or a cast, and both those approaches are open to me in Scala. Are those casts safe without runtime checks? --- In any case, at some point using types for program verification offers diminishing returns. We have to accept the possibility that maybe it's us, not type checkers, who have to verify our programs.

lmm 9y ago

Thanks for the reply > Without concrete type safety theorems (“such and such doesn't happen in a typable program”), you don't even know what type checking is supposed to buy you. What kind of safety theorem should I be looking for? I mean, what I generally want is something like "if an expression of type A evaluates, the result will be a valid thing of type A i.e. a value constructed by one of the constructors I defined for values of type A". Or perhaps it would be better expressed via elimination - "if I provide eliminators for all my constructors for type A then I can eliminate any expression of type A". I kind of want a "the system will never magic up an A out of nowhere" result, but AIUI I can never get that because I can't have a proof of consistency of the system, no? > Doing this safely requiers bona fide dependent types - in spite of their name, so-called “path-dependent types” are just fancy first-class existentials. What is it that we can't do currently? I mean, I can define a natural number type, I can convert between values and types in both directions. I can't use ad-hoc polymorphism with a type defined at runtime (the types I form at runtime must be phantom) but I wouldn't expect to do that in well-behaved code in the first place? The only way I can see for a type to ever get into code, in any language, is either through a literal or a cast, and both those approaches are open to me in Scala. What am I missing?

catnaroek 9y ago
> What kind of safety theorem should I be looking for? I mean, what I generally want is something like "if an expression of type A evaluates, the result will be a valid thing of type A i.e. a value constructed by one of the constructors I defined for values of type A". This is probably sufficient for a Coq-style proof assistant, but from a general-purpose programming language I expect more. See below. > I kind of want a "the system will never magic up an A out of nowhere" result, but AIUI I can never get that because I can't have a proof of consistency of the system, no? A type system can and should guarantee that you can't create values of a (positive) type other than by using the type's introuction forms. > What is it that we can't do currently? (0) The obvious: Be sure your program won't attempt to read from or write to a close file. (1) Obtain an arbitrary integer `n`. Test once whether it is a valid array index. If the test succeeds, use `n` arbitrarily often as an array index, without any further bounds-checking. (2) Obtain three `foo.Index` values `a,b,c`. Test once whether the arrays `foo` and `bar` have the same length. Use `a,b,c` arbitrarily often as values of type `bar.Index`, without any further bounds-checking. etc. etc. etc. > The only way I can see for a type to ever get into code, in any language, is either through a literal or a cast, and both those approaches are open to me in Scala. Are those casts safe without runtime checks? --- In any case, at some point using types for program verification offers diminishing returns. We have to accept the possibility that maybe it's us, not type checkers, who have to verify our programs.