5 ms·

invariants could be lifted into the type system Is there a reason this is only possible in Haskell, or does Haskell just make it super convenient / idiomatic?

pdpi 12y ago
The way I see it, immutability and purity are hard requirements for actually enforcing the contract, and a very robust type system is then a requirement to go from code that makes you want to shoot yourself in the head, to code that's incredibly expressive and easy to reason about. Haskell just happens to sit in that exact niche.
- marmaduke 12y ago
  immutability and purity are hard requirements I agree this is important. I have just started to move a project to Java from Python and see that immutability and purity are attainable for certain parts of the system but appear to cost a lot (leaning hard on use of interfaces, for example) in terms of readability.
yummyfajitas 12y ago
Haskell/Scala/etc makes it easy to nudge other developers into avoiding mistakes. A concrete example: I had a Scala system (build on Scalaz, which is a library providing Haskell for Scala), and one of our core types was DBTransaction[_] (a monad). A developer (a skeptic of the type system) was complaining to me about all the excess work he needed to go through, how he couldn't get properly construct a LazyStream[Foo] as a result of this. He wanted to construct a DBTransaction[LazyStream[Foo]], call runTransaction on it, and get the LazyStream[Foo] out. Then he was going to call f(lazyStream). The compiler just wouldn't allow this, so his "workaround" was to instead call lazyStream.map(f). Turns out this workaround prevented a runtime error. If he did get his LazyStream[Foo] out, generating the next element in the stream would have called resultSet.next() after closing the connection. This sort of thing happened quite often. People would complain that the type system made it harder for them to do what they wanted. They'd ask the FP "guru" types how to fix it and the "guru" would point out that what they wanted to do was fundamentally unsafe.
- marmaduke 12y ago
  So if I understand correctly, the real point is instead of programming defensively at runtime, you can do it in the type system. My main question is the extent to which this is possible in more conventional languages.
  - yummyfajitas 12y ago
    Yep - that's probably a fair way to describe it. It's of course possible in other statically typed languages, it's just not as easy. There are also some things that I'm not sure are reasonable at all in something like Java/C++ without writing a lot of code. For example: https://www.chrisstucchio.com/blog/2014/type_safe_vector_addition_with_dependent_types.html https://www.chrisstucchio.com/blog/2014/type_safe_vector_add...
    - marmaduke 12y ago
      Thanks for the link. I've been wondering how to lift N-D operations into the type system. If I write with NumPy x = r_[:n].reshape((3, -1, n/15))[:, :2].sum(axis=-1) a compiler could figure out that the shape of x is (3, 2) and allow y = x + randn(m, 1, 2) while forbidding z = y - r_[:7] With NumPy you have to wait for a runtime error, and only if the shapes can't be broadcast. We're not even talking correct use of dimensions, etc. I suppose this may have been tackled in Haskell in the Repa library, but I'd need to read papers like http://benl.ouroborus.net/papers/repa/repa-icfp2010.pdf http://benl.ouroborus.net/papers/repa/repa-icfp2010.pdf to know. Hence my question if we could lift this into the type system in a conventional language, but I don't think it's possible in a general way.
      - thinkpad20 12y ago
        I'm not sure what the notation you're using represents, but it looks like you're talking about matrices of a known size. What that's an example of is dependent types, where types can be parameterized by values, and not just types. For example, a (2D) matrix is parameterized by what it contains, and its dimensions. The former is a type but the latter are values. Without dependent types (or some subset of their capability) you can't represent this matrix type; you'd just have to check at runtime that no out-of-bounds access was occurring, so no; I don't think you could put this in a conventional language (without some crazy gymnastics, perhaps involving macros or similar). However, with dependent types, this is absolutely possible to statically guarantee that no out-of-bounds access will occur at runtime.
rprospero 12y ago
A toy example would be the following C code #include <math.h> double sine(double x){ reformat_hard_drive(); return sin(x); } which can be easily translated to Haskell sine x = do reformat_hard_drive return (sin x) So we can write the same stupid function in both languages. The bit that's specific to Haskell, as opposed to just any typed language, is that sine and sin have different types. sin is (Double -> Double) while sine is (Double -> IO Double), so swapping in sine for sin causes the code to fail to compile. Comparatively, you can drop in a random sine anywhere in your C code and the compiler will happily chug right along. While I've seen ways of implementing various invariant catching techniques like the Maybe type in C, I haven't seen anything that would catch the sine function. Now, as I said, this is a toy example. The real solution would be to fire whoever wrote the sine function. However, in larger systems, it can be translated into invariants such as declaring that a function cannot access the database or send packets on the network.

pdpi 12y ago

The way I see it, immutability and purity are hard requirements for actually enforcing the contract, and a very robust type system is then a requirement to go from code that makes you want to shoot yourself in the head, to code that's incredibly expressive and easy to reason about. Haskell just happens to sit in that exact niche.

marmaduke 12y ago
immutability and purity are hard requirements I agree this is important. I have just started to move a project to Java from Python and see that immutability and purity are attainable for certain parts of the system but appear to cost a lot (leaning hard on use of interfaces, for example) in terms of readability.

yummyfajitas 12y ago

Haskell/Scala/etc makes it easy to nudge other developers into avoiding mistakes. A concrete example: I had a Scala system (build on Scalaz, which is a library providing Haskell for Scala), and one of our core types was DBTransaction[_] (a monad). A developer (a skeptic of the type system) was complaining to me about all the excess work he needed to go through, how he couldn't get properly construct a LazyStream[Foo] as a result of this. He wanted to construct a DBTransaction[LazyStream[Foo]], call runTransaction on it, and get the LazyStream[Foo] out. Then he was going to call f(lazyStream). The compiler just wouldn't allow this, so his "workaround" was to instead call lazyStream.map(f). Turns out this workaround prevented a runtime error. If he did get his LazyStream[Foo] out, generating the next element in the stream would have called resultSet.next() after closing the connection. This sort of thing happened quite often. People would complain that the type system made it harder for them to do what they wanted. They'd ask the FP "guru" types how to fix it and the "guru" would point out that what they wanted to do was fundamentally unsafe.

marmaduke 12y ago
So if I understand correctly, the real point is instead of programming defensively at runtime, you can do it in the type system. My main question is the extent to which this is possible in more conventional languages.
- yummyfajitas 12y ago
  Yep - that's probably a fair way to describe it. It's of course possible in other statically typed languages, it's just not as easy. There are also some things that I'm not sure are reasonable at all in something like Java/C++ without writing a lot of code. For example: https://www.chrisstucchio.com/blog/2014/type_safe_vector_addition_with_dependent_types.html https://www.chrisstucchio.com/blog/2014/type_safe_vector_add...
  - marmaduke 12y ago
    Thanks for the link. I've been wondering how to lift N-D operations into the type system. If I write with NumPy x = r_[:n].reshape((3, -1, n/15))[:, :2].sum(axis=-1) a compiler could figure out that the shape of x is (3, 2) and allow y = x + randn(m, 1, 2) while forbidding z = y - r_[:7] With NumPy you have to wait for a runtime error, and only if the shapes can't be broadcast. We're not even talking correct use of dimensions, etc. I suppose this may have been tackled in Haskell in the Repa library, but I'd need to read papers like http://benl.ouroborus.net/papers/repa/repa-icfp2010.pdf http://benl.ouroborus.net/papers/repa/repa-icfp2010.pdf to know. Hence my question if we could lift this into the type system in a conventional language, but I don't think it's possible in a general way.
    - thinkpad20 12y ago
      I'm not sure what the notation you're using represents, but it looks like you're talking about matrices of a known size. What that's an example of is dependent types, where types can be parameterized by values, and not just types. For example, a (2D) matrix is parameterized by what it contains, and its dimensions. The former is a type but the latter are values. Without dependent types (or some subset of their capability) you can't represent this matrix type; you'd just have to check at runtime that no out-of-bounds access was occurring, so no; I don't think you could put this in a conventional language (without some crazy gymnastics, perhaps involving macros or similar). However, with dependent types, this is absolutely possible to statically guarantee that no out-of-bounds access will occur at runtime.

rprospero 12y ago

A toy example would be the following C code #include <math.h> double sine(double x){ reformat_hard_drive(); return sin(x); } which can be easily translated to Haskell sine x = do reformat_hard_drive return (sin x) So we can write the same stupid function in both languages. The bit that's specific to Haskell, as opposed to just any typed language, is that sine and sin have different types. sin is (Double -> Double) while sine is (Double -> IO Double), so swapping in sine for sin causes the code to fail to compile. Comparatively, you can drop in a random sine anywhere in your C code and the compiler will happily chug right along. While I've seen ways of implementing various invariant catching techniques like the Maybe type in C, I haven't seen anything that would catch the sine function. Now, as I said, this is a toy example. The real solution would be to fire whoever wrote the sine function. However, in larger systems, it can be translated into invariants such as declaring that a function cannot access the database or send packets on the network.