4 ms·

> figure out what extensions are needed to write practical programs in it, at first in an ad-hoc way, then figure out a way to make that extension in a sound, c

> figure out what extensions are needed to write practical programs in it, at first in an ad-hoc way, then figure out a way to make that extension in a sound, compatible way, then finally form a new clean formal language that accommodates these extensions. This is not possible, and the history of Haskell, Scala, and to a lesser extent OCaml, is precisely the evidence for it. > Not my experience. I've found HKT and dependent types extremely useful in practice; In practice, most uses of HKTs or even term-level HOFs are just bad workarounds for (0) The lack of a proper hierarchical module system, allowing type components to be shared by fibration. (1) The lack of properly designed data structure libraries with decoupled concerns. For example, you need traversals and folds to manipulate sets and maps, but you don't need them to manipulate search trees (i.e., trees that allow you to do binary search, rather than ADTs that might use binary search under the covers). > they give me a simple way to directly encode the business properties I care about verifying. Do you actually verify them? How exactly do you verify Scala programs in the absence of a formal semantics for Scala? > Not at all convinced that e.g. Idris-style totality is "unacceptable". What's the problem with it? “There is no largest class of recognizably terminating programs.” https://mail.haskell.org/pipermail/haskell-cafe/2003-May/004343.html https://mail.haskell.org/pipermail/haskell-cafe/2003-May/004... > Certainly my practical Scala experience is that it's good for everything. One thing that I find useful, due to my current job, is numerical linear algebra without array bounds checks at runtime. Have fun doing this in Scala.

lmm 9y ago
> This is not possible, and the history of Haskell, Scala, and to a lesser extent OCaml, is precisely the evidence for it. Then how do you explain the existence of e.g. Idris or Dotty? > In practice, most uses of HKTs or even term-level HOFs are just bad workarounds for > (0) The lack of a proper hierarchical module system, allowing type components to be shared by fibration. They don't feel like a workaround. They feel like a nice way of modelling my problems that has the properties that I want. Maybe there are other ways, but if those other ways work then why aren't we seeing them in industry? > Do you actually verify them? How exactly do you verify Scala programs in the absence of a formal semantics for Scala? Any verification method has a false-negative rate. I use a combination of trusting the compiler's typechecking, 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. Maybe I'm missing something, because there always seems to be some disconnect in these conversations: as far as I can see any method that lets you associate logical deductions to your program and mechanically verify that those deductions are legitimate is verification, and I can certainly do that with propositions-as-types in the Scala type system. I don't verify the faithfulness of the compiled code, but many verification systems don't do that either. I don't have a proof of soundness, but plenty of verification systems don't have that. > “There is no largest class of recognizably terminating programs.” Sure. But not all recognisably terminating programs are important or useful. To form a terminating language we have to have a finite limit on how many levels of nested 'eval' we can do at compile time, sure (though I see no reason we can't form a parameterized family of languages and pass the "depth" as a compiler argument). That's irritating, but it's a big jump to "unacceptable" > One thing that I find useful, due to my current job, is numerical linear algebra without array bounds checks at runtime. Have fun doing this in Scala. "Without array bounds checks at runtime" is not a real requirement. The real requirement would be something like "using x amount of CPU" or, ultimately, "at cost of no more than $y". FWIW I did numerical linear algebra in Scala in production at a previous job; the benefits outweighed the costs. 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. Yes the current implementation doesn't do it, but that's a contingent fact about the current implementation, not something fundamental.
- catnaroek 9y ago
  > 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

> This is not possible, and the history of Haskell, Scala, and to a lesser extent OCaml, is precisely the evidence for it. Then how do you explain the existence of e.g. Idris or Dotty? > In practice, most uses of HKTs or even term-level HOFs are just bad workarounds for > (0) The lack of a proper hierarchical module system, allowing type components to be shared by fibration. They don't feel like a workaround. They feel like a nice way of modelling my problems that has the properties that I want. Maybe there are other ways, but if those other ways work then why aren't we seeing them in industry? > Do you actually verify them? How exactly do you verify Scala programs in the absence of a formal semantics for Scala? Any verification method has a false-negative rate. I use a combination of trusting the compiler's typechecking, 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. Maybe I'm missing something, because there always seems to be some disconnect in these conversations: as far as I can see any method that lets you associate logical deductions to your program and mechanically verify that those deductions are legitimate is verification, and I can certainly do that with propositions-as-types in the Scala type system. I don't verify the faithfulness of the compiled code, but many verification systems don't do that either. I don't have a proof of soundness, but plenty of verification systems don't have that. > “There is no largest class of recognizably terminating programs.” Sure. But not all recognisably terminating programs are important or useful. To form a terminating language we have to have a finite limit on how many levels of nested 'eval' we can do at compile time, sure (though I see no reason we can't form a parameterized family of languages and pass the "depth" as a compiler argument). That's irritating, but it's a big jump to "unacceptable" > One thing that I find useful, due to my current job, is numerical linear algebra without array bounds checks at runtime. Have fun doing this in Scala. "Without array bounds checks at runtime" is not a real requirement. The real requirement would be something like "using x amount of CPU" or, ultimately, "at cost of no more than $y". FWIW I did numerical linear algebra in Scala in production at a previous job; the benefits outweighed the costs. 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. Yes the current implementation doesn't do it, but that's a contingent fact about the current implementation, not something fundamental.

catnaroek 9y ago
> 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.