4 ms·

HM style type inference is nice, but the root problem is that the static type system restricts you to a set of statements that it is able to verify at compile t

HM style type inference is nice, but the root problem is that the static type system restricts you to a set of statements that it is able to verify at compile time. This necessarily leads to code that prioritizes the needs of the compiler over those of the human reader. The more things you try to encode using the type system, the more complex your code becomes because proving something correct for all cases is typically significantly more difficult than just stating it and testing for the set of cases you care about. Furthermore, there is no way to verify that your type definitions themselves are correct. When you start moving program logic into types, the compiler cannot help you ensure that it's correct. Here's a fully typed insertion sort [1] written in Idris. It's over 260 lines long, and it takes non trivial amount of effort to understand it fully, and know that what it specifies is indeed what was intended. Meanwhile, I can trivially read and understand a 10 line Python version in its entirety. Of course, you could argue that it's an extreme case, and that in practice you probably wouldn't have such an exhaustive type specification. At that point you'd be agreeing that relaxing type constraints does provide a benefit, and we'd just be arguing about our respective levels of comfort. [1] https://github.com/davidfstr/idris-insertion-sort/blob/master/InsertionSort.idr https://github.com/davidfstr/idris-insertion-sort/blob/maste...

Drup 7y ago
This is really an apple to oranges comparison. What you linked is not an implementation of the insertion sort. It's a an implementation coupled with proof of correctness. Try to make a mechanize proof of correctness of your python code, and it'll be as long (or longer). If you just write an implementation in statically typed languages like OCaml, F#, Haskell, Typescript (or even Idris, if you go less crazy with the typing), and you can get it down to less 10 lines easily.
- yogthos 7y ago
  A proof of correctness is what static typing is fundamentally. The example I provided simply turns this up to 11. However, if you relax the constraint then you're losing benefits of statically checking properties at compile time. If you agree that having a 10 line version that does less checking is better than having a 260 line version that does, then you're agreeing that there is a cost associated with static checking. There are plenty of real world scenarios where static checking gets in the way even if you're not trying to encode complex properties using the type system. One problem is that static typing is at odds with modularization since type declarations are considered globally. For example, Ring HTTP abstraction in Clojure represents requests and responses as maps. Middleware functions [1] can update these maps to inject additional keys, or modify existing keys. These functions often live in separate libraries that know nothing about one another. A static type system precludes this since it would require you to provide a static declaration for every possible request and response map. [1] https://github.com/ring-clojure/ring/wiki/Middleware-Patterns https://github.com/ring-clojure/ring/wiki/Middleware-Pattern...
  - aidenn0 7y ago
    Static typing does not prevent this; the fact that static typed languages can parse freeform formats like JSON works as a simple example. If you statically prove that you check that they keys are there before using them, then the type system can be satisfied.
    - yogthos 7y ago
      You don't know what the keys are up front because each library is an independent module. Of course, you could just use Any type, but then you're not doing static typing.
      - aidenn0 7y ago
        Example: Module X expects the "foo" key, then write a function that checks if it has the foo key and returns a type Maybe(HasFoo). It's less good than just treating the type as the union of HasFoo and HasBar or whatever, but if you fully decouple, then you have to be able to handle the case in which the mapping lacks a foo key anyways, and this will statically froce you to.
        yogthos 7y ago
        But the point is that you don't know the totality of the keys up front. Module A might deal with keys X and Y, while module B deals with keys W and Z. These two modules know absolutely nothing about each other and they're developed by different people.
        aidenn0 7y ago
        Right, so Module A defines a "TypeA" (which describes a map containing keys X and Y) and Module B defines a "TypeB" (which describes a map containing keys W and Z) and they each define their respective functions that return a (Maybe Type A) and (Maybe Type B). If the map has keys X and Y then you will get a (Just Type A) and if it does not you will get (Nothing). The type system will then enforce that you handle the possibility of (Nothing) which is something you would need to do in a dynamically typed language as well. Remember, in the sense we are currently talking about[1], objects are untyped, it's variables that are typed. So there is no need to describe the type of this map that is passing around in concrete terms; it's perfectly cromulent to treat the map as a TypeA in one place and a TypeB in another place, so long as you ensure that the prerequisites for those types are satisfied by the object. It is true that it is usually preferable in statically typed languages to demonstrate that the map satisfies the requirements for TypeA before type erasure (i.e. at compile time), but if you want total decoupling, then that is not possible (since the requirement that the map have keys X and Y would need to be enforced outside of Module A). This does not mean that a type system cannot help you though. I think we are getting to the limits of what can be easily communicated via HN comments, so if you still don't understand, then perhaps I'll write a blog article explaining it more fully.
UK-AL 7y ago
That code includes a proof of correctness. A stronger form of verification than tests.
- yogthos 7y ago
  Yes, and my point is that there is a large cost associated with having such a proof.
  - mcguire 7y ago
    What is the cost associated with not having such a proof?
    - keymone 7y ago
      Not that high apparently, as there is no conclusive evidence for it.
    - yogthos 7y ago
      https://news.ycombinator.com/item?id=20330727 https://news.ycombinator.com/item?id=20330727
  - the_af 7y ago
    Don't forget that you also pay hidden costs when you forgo static proofs. It may be that you need to write more explicit tests by hand, or that you pay for the lack of verification with increased run time errors in production.
    - yogthos 7y ago
      Sure, however nobody has been shown that one approach is more costly than the other in practice. The most recent research available is the replication of the large scale GitHub study [1]. The relative effects of language choice on code quality is less than 1%. The main finding is that language choice hardly matters at all. On the other hand, we can easily measure the effects of factors like sleep [2], overwork [3], and happiness [4] on code quality. If static typing was an actual factor, we’d see exactly the same kinds of effects. There’s nothing wrong with enjoying static typing, but there’s simply no evidence that it plays any role past personal preference. Different people solve problems in different ways, and have different pain points. It's entirely possible that each type discipline appeals to different mindsets. That is a value in itself. [1] https://arxiv.org/abs/1901.10220 https://arxiv.org/abs/1901.10220 [2] https://arxiv.org/pdf/1805.02544.pdf https://arxiv.org/pdf/1805.02544.pdf [3] http://web.archive.org/web/20090824001133/http://www.curt.org/pdf/156.pdf http://web.archive.org/web/20090824001133/http://www.curt.or... [4] http://neverworkintheory.org/2014/05/01/happy-sw-devs-solve-problems-better.html http://neverworkintheory.org/2014/05/01/happy-sw-devs-solve-...
lalaithion 7y ago
insert x [] = [x] insert x (y:ys) = if x > y then y:(insert x ys) else x:y:ys insertSort xs = foldr insert [] xs Three lines of Haskell, fully statically typed. Yes, Idris' proofs are verbose. They're also a perfect validation of the properties that need to be proven, better than any test case in the world.
- yogthos 7y ago
  Your version doesn't provide the same guarantees. It doesn't even guarantee that the same items are returned as the ones that were provided as arguments. So, you appear to be agreeing that relaxing static typing constraints results in code that's easier to understand. Unfortunately, Haskell type system can result in baroque code in many cases as well. The whole reason monads are so prevalent in Haskell is due to the fact that the type system tracks side effects. Here's an example of a problem this introduces from the core.async library. https://groups.google.com/forum/#!topic/clojure/wccacRJIXvg https://groups.google.com/forum/#!topic/clojure/wccacRJIXvg When I first wrote the core.async go macro I based it on the state monad. It seemed like a good idea; keep everything purely functional. However, over time I've realized that this actually introduces a lot of incidental complexity. And let me explain that thought. What are we concerned about when we use the state monad, we are shunning mutability. Where do the problems surface with mutability? Mostly around backtracking (getting old data or getting back to an old state), and concurrency. In the go macro transformation, I never need old state, and the transformer isn't concurrent. So what's the point? Recently I did an experiment that ripped out the state monad and replaced it with mutable lists and lots of atoms. The end result was code that was about 1/3rd the size of the original code, and much more readable. So more and more, I'm trying to see mutability through those eyes: I should reach for immutable data first, but if that makes the code less readable and harder to reason about, why am I using it? If Clojure had Haskell type system, the monad approach would be the only option resulting in code that's harder to reason about.

Drup 7y ago

This is really an apple to oranges comparison. What you linked is not an implementation of the insertion sort. It's a an implementation coupled with proof of correctness. Try to make a mechanize proof of correctness of your python code, and it'll be as long (or longer). If you just write an implementation in statically typed languages like OCaml, F#, Haskell, Typescript (or even Idris, if you go less crazy with the typing), and you can get it down to less 10 lines easily.

yogthos 7y ago
A proof of correctness is what static typing is fundamentally. The example I provided simply turns this up to 11. However, if you relax the constraint then you're losing benefits of statically checking properties at compile time. If you agree that having a 10 line version that does less checking is better than having a 260 line version that does, then you're agreeing that there is a cost associated with static checking. There are plenty of real world scenarios where static checking gets in the way even if you're not trying to encode complex properties using the type system. One problem is that static typing is at odds with modularization since type declarations are considered globally. For example, Ring HTTP abstraction in Clojure represents requests and responses as maps. Middleware functions [1] can update these maps to inject additional keys, or modify existing keys. These functions often live in separate libraries that know nothing about one another. A static type system precludes this since it would require you to provide a static declaration for every possible request and response map. [1] https://github.com/ring-clojure/ring/wiki/Middleware-Patterns https://github.com/ring-clojure/ring/wiki/Middleware-Pattern...
- aidenn0 7y ago
  Static typing does not prevent this; the fact that static typed languages can parse freeform formats like JSON works as a simple example. If you statically prove that you check that they keys are there before using them, then the type system can be satisfied.
  - yogthos 7y ago
    You don't know what the keys are up front because each library is an independent module. Of course, you could just use Any type, but then you're not doing static typing.
    - aidenn0 7y ago
      Example: Module X expects the "foo" key, then write a function that checks if it has the foo key and returns a type Maybe(HasFoo). It's less good than just treating the type as the union of HasFoo and HasBar or whatever, but if you fully decouple, then you have to be able to handle the case in which the mapping lacks a foo key anyways, and this will statically froce you to.
      - yogthos 7y ago
        But the point is that you don't know the totality of the keys up front. Module A might deal with keys X and Y, while module B deals with keys W and Z. These two modules know absolutely nothing about each other and they're developed by different people.
        aidenn0 7y ago
        Right, so Module A defines a "TypeA" (which describes a map containing keys X and Y) and Module B defines a "TypeB" (which describes a map containing keys W and Z) and they each define their respective functions that return a (Maybe Type A) and (Maybe Type B). If the map has keys X and Y then you will get a (Just Type A) and if it does not you will get (Nothing). The type system will then enforce that you handle the possibility of (Nothing) which is something you would need to do in a dynamically typed language as well. Remember, in the sense we are currently talking about[1], objects are untyped, it's variables that are typed. So there is no need to describe the type of this map that is passing around in concrete terms; it's perfectly cromulent to treat the map as a TypeA in one place and a TypeB in another place, so long as you ensure that the prerequisites for those types are satisfied by the object. It is true that it is usually preferable in statically typed languages to demonstrate that the map satisfies the requirements for TypeA before type erasure (i.e. at compile time), but if you want total decoupling, then that is not possible (since the requirement that the map have keys X and Y would need to be enforced outside of Module A). This does not mean that a type system cannot help you though. I think we are getting to the limits of what can be easily communicated via HN comments, so if you still don't understand, then perhaps I'll write a blog article explaining it more fully.

UK-AL 7y ago

That code includes a proof of correctness. A stronger form of verification than tests.

yogthos 7y ago
Yes, and my point is that there is a large cost associated with having such a proof.
- mcguire 7y ago
  What is the cost associated with not having such a proof?
  - keymone 7y ago
    Not that high apparently, as there is no conclusive evidence for it.
  - yogthos 7y ago
    https://news.ycombinator.com/item?id=20330727 https://news.ycombinator.com/item?id=20330727
- the_af 7y ago
  Don't forget that you also pay hidden costs when you forgo static proofs. It may be that you need to write more explicit tests by hand, or that you pay for the lack of verification with increased run time errors in production.
  - yogthos 7y ago
    Sure, however nobody has been shown that one approach is more costly than the other in practice. The most recent research available is the replication of the large scale GitHub study [1]. The relative effects of language choice on code quality is less than 1%. The main finding is that language choice hardly matters at all. On the other hand, we can easily measure the effects of factors like sleep [2], overwork [3], and happiness [4] on code quality. If static typing was an actual factor, we’d see exactly the same kinds of effects. There’s nothing wrong with enjoying static typing, but there’s simply no evidence that it plays any role past personal preference. Different people solve problems in different ways, and have different pain points. It's entirely possible that each type discipline appeals to different mindsets. That is a value in itself. [1] https://arxiv.org/abs/1901.10220 https://arxiv.org/abs/1901.10220 [2] https://arxiv.org/pdf/1805.02544.pdf https://arxiv.org/pdf/1805.02544.pdf [3] http://web.archive.org/web/20090824001133/http://www.curt.org/pdf/156.pdf http://web.archive.org/web/20090824001133/http://www.curt.or... [4] http://neverworkintheory.org/2014/05/01/happy-sw-devs-solve-problems-better.html http://neverworkintheory.org/2014/05/01/happy-sw-devs-solve-...

lalaithion 7y ago

insert x [] = [x] insert x (y:ys) = if x > y then y:(insert x ys) else x:y:ys insertSort xs = foldr insert [] xs Three lines of Haskell, fully statically typed. Yes, Idris' proofs are verbose. They're also a perfect validation of the properties that need to be proven, better than any test case in the world.

yogthos 7y ago
Your version doesn't provide the same guarantees. It doesn't even guarantee that the same items are returned as the ones that were provided as arguments. So, you appear to be agreeing that relaxing static typing constraints results in code that's easier to understand. Unfortunately, Haskell type system can result in baroque code in many cases as well. The whole reason monads are so prevalent in Haskell is due to the fact that the type system tracks side effects. Here's an example of a problem this introduces from the core.async library. https://groups.google.com/forum/#!topic/clojure/wccacRJIXvg https://groups.google.com/forum/#!topic/clojure/wccacRJIXvg When I first wrote the core.async go macro I based it on the state monad. It seemed like a good idea; keep everything purely functional. However, over time I've realized that this actually introduces a lot of incidental complexity. And let me explain that thought. What are we concerned about when we use the state monad, we are shunning mutability. Where do the problems surface with mutability? Mostly around backtracking (getting old data or getting back to an old state), and concurrency. In the go macro transformation, I never need old state, and the transformer isn't concurrent. So what's the point? Recently I did an experiment that ripped out the state monad and replaced it with mutable lists and lots of atoms. The end result was code that was about 1/3rd the size of the original code, and much more readable. So more and more, I'm trying to see mutability through those eyes: I should reach for immutable data first, but if that makes the code less readable and harder to reason about, why am I using it? If Clojure had Haskell type system, the monad approach would be the only option resulting in code that's harder to reason about.