15 ms·

> if your code compiles, it probably works I'm always a little frustrated whenever I see this aphorism perpetuated since I think it gives the impression that a

> if your code compiles, it probably works I'm always a little frustrated whenever I see this aphorism perpetuated since I think it gives the impression that a static type system is doing more than it is actually doing. In type systems that are used outside of academia, the main thing your static types are doing is checking whether the shapes of your data and functions all line up. With some small exceptions, that's it: the compiler will tell you if your LEGOs fit together, but not if you've built a knife instead of a fork. I know what this aphorism is getting at, which is that in some domains and circumstances a lot of your bugs are "shape" errors, and it's gratifying when you're writing OCaml or Java and you can, say, refactor without hesitation, knowing the compiler will find even the most unused paths where you need to modify an invocation of your function. But it's been my and others' experience that there are many times where this isn't your most pressing concern, and could in fact be a pretty boring concern that you don't even want to pay the type annotation tax for. (I also think there's something to the idea that a static type system can instill too much confidence and encourage the pursuit of bad abstractions like 18-arg functions that can no longer be effectively reasoned about by an unaided human mind, but that's another topic.)

bgorman 6y ago
If you use a powerful type system like Ocamls's, your can make many error states unrepresentable. This is basically impossible to do in Java. Moreover, in OCaml it is idiomatic to use type inference everywhere except for interface files, so in practice you almost never annotate types.
sullyj3 6y ago
Type systems can encode proofs of properties that you want your data to have. For example, suppose you want to write a function that returns the first element of a list. head :: [a] -> a This is the type of a function "head" that takes a list of values of some arbitrary type a, and returns an a. if you feed this function an empty list, what will it do? You can reason from the type signature that the only thing it possibly can do is crash, since there's no way to produce a value of type a without knowing what a is in advance. head (h:_rest) = h head [] = error "Our function is badly behaved!" To ensure that our function never crashes, we can encode the fact that our list is nonempty in a datatype. data Nonempty a = Nonempty a [a] Ie, a nonempty list must contain a value of type a, and a (possible empty) list of as. Then instead of writing a function that crashes when it receives a nonempty list, we can write a function on nonempty lists that never crashes head :: Nonempty a -> a head (Nonempty x _rest) = x What I'm getting at is that, yes, this is just the "shape" of our data. But you can encode more interesting and valuable properties in that shape than might be apparent at first. There are many other interesting examples of using types to ensure that properties that we want to hold for our values, do in fact hold. Edit: I should probably add that "If it compiles it works" is absolutely not always true. It's more of a community in-joke than an actual belief. But it does turn out to be true surprisingly frequently.
- neolog 6y ago
  Sure, you can encode various properties in some languages, but it's not that common to actually do so.
  - sullyj3 6y ago
    In Haskell, it's both common and idiomatic. There's always a tradeoff between the usefulness of having static guarantees, and the complexity of the type system features that enable those guarantees. In some cases it's more trouble than it's worth to enforce certain static properties - you have to weigh the costs and benefits on a case by case basis. But it's nice to have the option, and Haskellers make use of it frequently.
    - heavenlyblue 6y ago
      You don’t need Haskell to do this however.
      - elbear 6y ago
        You need a type system that is expressive enough to allow you to encode logic in the types. Of course, Haskell is not only language with such a type system: PureScript, F#, Rust, OCaml, Scala have similar features, although not all.
    - tsimionescu 6y ago
      How many functions have you seen, in Haskell, that take Nonempty a versus taking [a]? There are reasons why this type of pattern doesn't scale well, and the Haskell designers knew it. Similarly, if they had defined head [a] -> Optional a, that would have produced complications of its own.
      - sullyj3 6y ago
        The general consensus in the community afaik, is that head :: [a] -> a in Prelude was a mistake, and the default should be to return a Maybe/Optional. Beginners are generally advised to avoid head, and all other partial functions in the Prelude, such as tail and the indexing operator, wherever possible, and rely on pattern matching instead, which is generally sufficient and more idiomatic for the relevant use cases. I agree that having the option to use a partial function is useful, escape hatches are important, but it shouldn't be the go to. Nonempty was just a simple example. You're right that it's not very commonly used (probably because it's not in Prelude), but the general culture of writing type safe interfaces and pushing guarantees to compile time %100 is a thing. A commonly used, more complicated example might be Servant, which is a web library which statically ensures your implementation meets an API spec.
sfvisser 6y ago
It works two ways though, which I think is important. Yes, type systems check the shape of your data which is nice. However, when sufficiently experienced, the type system also guides the developer into good program design. Type systems for me are more a design tool than shape checker. The checker/inferencer helps me learn about assumptions I make about data in specific parts of my code, which allows me to remodel my data types to better fit my intent. This works cyclic until things just seem to ‘fit’. Personally at least, this allows me to write far more complicated applications than I would ever be able to do without types. And it’s just very hard for me to imagine this wouldn’t be the case for any other developer.
lmm 6y ago
> I'm always a little frustrated whenever I see this aphorism perpetuated since I think it gives the impression that a static type system is doing more than it is actually doing. In type systems that are used outside of academia, the main thing your static types are doing is checking whether the shapes of your data and functions all line up. With some small exceptions, that's it: the compiler will tell you if your LEGOs fit together, but not if you've built a knife instead of a fork. Disagree. You can and should be using your type system to express your system design. If it's important that your utensil has at least 3 prongs, it should only be constructible by passing at least 3 prongs; that much is trivial to do even in Java, yet alone a language with a decent (i.e. ML-family) typesystem.
FullyFunctional 6y ago
I frequently have to defend why I hate Python but the foremost reason is that lack of static typing (which also makes reading other peoples codes harder than it need be). Static typing, especially in a rich type system like, e.g. Haskell and Rust, doesn't guarantee you don't have bugs, but it almost guarantees the ones that remain are better bugs, that is, application level bugs. However in my experience, I can usually tell what kind of code will be correct once it passes and which might still have issues.
- tines 6y ago
  Absolutely. The more experience I have, the more repugnant dynamically typed languages seem to me (for domains where they fit, i.e. I'm not talking about untyped assembly or whatever).
- rxhernandez 6y ago
  Which is absolutely bizarre to me because most of my experience with Python has been with people who are effectively scientists who don't give a rats-ass about good coding practices and yet I rarely had issues with receiving the wrong type. Don't get me wrong though, I spent the first 10 years of programming with C and Java so I understand the comfort that a statically typed language provides. I just haven't found it to be a big enough issue over the past 7-8 years of programming in Python to really complain about it. Frankly, if you were to ask me what the top 3 sources of my headaches in Python are, number 1, 2, and 3 would be, receiving a None value when I expected something else; but that's an issue with most languages.
  - boloust 6y ago
    > Frankly, if you were to ask me what the top 3 sources of my headaches in Python are, number 1, 2, and 3 would be, receiving a None value when I expected something else Curious example, because that's absolutely something a sufficiently advanced and well-thought-out static type system can completely solve. You're right that the type systems of C and Java do not meet this bar, however.
    - 6y ago
pyrale 6y ago
> you don't even want to pay the type annotation tax for. 95% of annotations in the average haskell codebase are unneeded for compilation. People still write them, because they are a useful source of information when reading the code. So tell me, if you feel like you don't want to write down that one line of comment which happens to be checked against the compiler, I guess you probably don't write tests or documentation either?
- jstimpfle 6y ago
  > I guess you probably don't write tests or documentation either? Why would any experienced programmer make such a blanket statement? As always, it depends. Sometimes there is value in documentation (or whatever unchecked types in fancy languages), especially for stuff that is read a lot more, by other people, or yourself in the future. For a lot of stuff there is no point in writing documentation. For example, if the code is obvious and pedestrian. Or if you'll just throw away everything, or refactor a month later. And very often, writing documentation is not only a waste of time, but downright harmful, because code and documentation easily diverge. My personal advice (not just for documentation) is to strive on the side of doing as little as you can get away with, and only introduce structure and bureaucracy if there's a clear indication that it's required.
  - garethrowlands 6y ago
    The fact that code and types don't diverge can make types useful as documentation, albeit limited documentation. Ideally the compiler figures out the types so you don't have to. Haskellers often find this useful when they refactor a month later.
    - jstimpfle 6y ago
      Code and types can very much diverge if the types aren't checked by the compiler, as my parent poster indicated. Case in point: type aliases instead of (Haskell) newtypes. Type aliases (which are unchecked, unlike newtypes) can lead to exactly the kind of diverging that I alluded to. Look at the mess that is all the typedefs and defines in the Win32 API for example. It's extremely hard not to pass in the wrong typedefs, and there must be extremely few programmers who know which aliases are the same on every platform and which could change. Aside, newtypes (Or the equivalent in C for example, wrapping a single member in a struct) can be very annoying. I would advicse against this, just like I'd advise against using type aliases.
q3k 6y ago
Agreed. I have a strong background in 'bad' programming languages like Go, Python, C. Half a year ago I had a short stint at a Haskell shop and was thoroughly disillusioned. That particular 'writing against the compiler' approach lended itself to write-once, over complex type juggling code. Because why make it readable - if it compiles, it works, and if it works, there won't be any need to read it, right? Well, except you still get bugs, and then debugging anything is like making sense of brainfuck. Maybe smarter people than me can juggle a handful of types and operators simultaneously in their head - I can't. My favourite example of 'just because it compiles it doesn't mean it works is' Maybe [a]. I've had a colleague scratch their head for hours over something like this: userCount :: Foo -> Int userCount f = length $ getUsers f This compiled, but always returned 1. Why? Well, because turns out `getUsers` returned `Maybe [User]`, and not `[User]` as the programmer expected, and somewhat asserted in their mind with types. And it also turns out that in Haskell, `length` takes a `Foldable`, and `Maybe` is a `Foldable`. Thus, a `length` of a Maybe will gladly return 0 or 1, which makes perfect sense from the point of view of the type system, but zero sense when it comes to humans. Whoops.
- tome 6y ago
  The Foldable instance for Maybe is one of the biggest warts in Haskell. It's not limited to Haskell, by the way. def getUsers(f): return (logged_in_users(f), logged_out_users(f)) def userCount(f): return len(getUsers(f))
  - q3k 6y ago
    Sure, but Python and Python developers don’t hype up its type system to be the solution to all your programming woes :).
    - tome 6y ago
      I'm not sure what "Haskell developers" are saying, but this Haskell developer says "Haskell provides many tools that can be used to solve programming woes. One such tool is its strong and flexible types system (there are several other tools, such as immutability, functional style)."
cageface 6y ago
I find explicit null checking almost as valuable as static typing. Tests can cover a lot of the same ground as types but it’s very easy to have tests that don’t anticipate the nulls you only get in production.
boloust 6y ago
> I think it gives the impression that a static type system is doing more than it is actually doing This statement probably gets to the heart of the issue. A static type system isn't something that just "does things", nor can we conduct a proper analysis when the dialectic is reduced to "static vs dynamic". The first thing to realize is that there exists a spectrum in how much we encode in our type system. Even in weaker type systems like those of Go or Java, we can make illegal states unrepresentable, encode invariants, create typesafe abstractions, etc. Or we could just treat everything as object and not make any attempt to encode anything at all in the type system. In the former case, the aphorism "if your code compiles, it probably works", is more true than in the latter case. The next thing to realize is that the expressiveness of a type system places a ceiling on what can be usefully encoded in that type system. So in languages like Haskell, it's possible to get closer to the "if your code compiles, it probably works" ideal, than in a language with a weaker type system. But even in Haskell, it's possible to just write everything in IO and not make any attempt to encode your constraints in the type system. So in that sense, a type system is just a tool. If wielded effectively, it lets us offload a lot of work to the compiler in a sort of symbiotic back-and-forth. And some languages give us better static typing tools, to make that symbiosis more effective. But if we're not using simpler type systems to their fullest, we're not likely to be pushing against their limits, making it a lot harder to justify more advanced type systems. So "if your code compiles, it probably works" shouldn't be read as a statement of fact, but as an aspirational goal, one that we can move towards by more effective use of our tools.
jbotz 6y ago
> the compiler will tell you if your LEGOs fit together, but not if you've built a knife instead of a fork. OK, let's stretch that metaphor a bit. A powerful type system like Haskell's is really a way of both restricting which LEGO(tm) pieces you can use and designing custom new ones. So when you design and write software in truly idiomatic Haskell, after getting all your types lined up there is no way to make anything other than a fork.
higerordermap 6y ago
Not just shape of data, but the values that are allowed by data. I agree that it is an oversold fallacy and types get really clunky when pushed too far. But any worthy type system prevents lot of errors. This is not generally acclaimed by empirical studies claiming only 5% improvement because they are caught at compile time. Other benefits are enough to use a sufficiently good static type system, by the way, even for people that think type systems aren't better than TDD. * Better autocomplete * Better error highlighting - no need to run code or tests, IDE can highlight instantly. * No typos in variable names (can be achieved in some but not all dynamic languages) * Performance of compiled code
- vindarel 6y ago
  All 4 points why I like Lisp so much more than Python!
08-15 6y ago
> static types are ... checking whether the shapes of your data and functions all line up They definitely do more than that in Haskell. You can define distinct types with the same "shape", and the `newtype` keyword specifically creates a new type that has the same "shape" as an existing one, but is nominally distinct. This nominal typing, as it's called, allow you to express intent in types. Type checking then doesn't just check whether "shapes" line up, but also whether your intentions line up. If you express contradictory intentions, you probably made a mistake. Practically speaking, if the only types ever used in a Haskell program are `Int`, `Float`, `Char` and nested lists of those, all the type checker can ever do is tell me when I miscount square brackets or forget a `fromIntegral`. Those programs never run on the first attempt.
guenthert 6y ago
Yes, I'm somewhat puzzled that static typing seems so important to some, while it clearly only prevents one class of errors (and depending on the language, even that only to some extend, e.g. it's still possible to initialize enumeration class instances with invalid values in C++). I'd have expected that Eiffel's pre- and post-condition or design by contract in general, would have gained more traction with those who care about eliminating possible sources of programmer errors.
dirkt 6y ago
> you don't even want to pay the type annotation tax for. You won't understand those aphorisms as long as think of "type annotation" as something useless, "tax-like". I know where you come from, in languages like Java it is a tax - you repeatedly write long-winded types in different places. With type inference, that changes. You have a REPL (or IDE integration) that you can just ask for the inferred type as soon as you write a function. Then you look at it, you think about if it expresses what you want the function to do (that already catches some errors), you copy-and-paste it, make it a bit prettier, and bam, type annotation is done. It's even on an extra line, you don't have to attach it to arguments. Or, you design with types ("test first style", think of the type annotation as a test). You first write down the type, then you write the function, and you see if the type checker agrees. If it doesn't, you probably found a bug. Or your idea of what the function should do was wrong (has also happened to me). And everyone who uses that system does know that type checks are very dumb checks. They only help against dumb errors. But the majority of bugs are dumb bugs (at least the majority of my bugs) - misspellings, you forget to write out some part, etc. Those get caught. The hard bugs won't - that's what tests are for. (And automated testing is again simpler in the presence of types, see Quickcheck). > and encourage the pursuit of bad abstractions like 18-arg functions It never does. 18-arg functions are just unwieldy. If your function grows to that point, refactor (or rather, refactor long before that). And again, the type systems helps with refactoring. (Yes, I know I won't convince you, this debate has been going on for at least 30 years. OTOH, it doesn't hurt to see the opinion on the other side).

bgorman 6y ago

If you use a powerful type system like Ocamls's, your can make many error states unrepresentable. This is basically impossible to do in Java. Moreover, in OCaml it is idiomatic to use type inference everywhere except for interface files, so in practice you almost never annotate types.

sullyj3 6y ago

Type systems can encode proofs of properties that you want your data to have. For example, suppose you want to write a function that returns the first element of a list. head :: [a] -> a This is the type of a function "head" that takes a list of values of some arbitrary type a, and returns an a. if you feed this function an empty list, what will it do? You can reason from the type signature that the only thing it possibly can do is crash, since there's no way to produce a value of type a without knowing what a is in advance. head (h:_rest) = h head [] = error "Our function is badly behaved!" To ensure that our function never crashes, we can encode the fact that our list is nonempty in a datatype. data Nonempty a = Nonempty a [a] Ie, a nonempty list must contain a value of type a, and a (possible empty) list of as. Then instead of writing a function that crashes when it receives a nonempty list, we can write a function on nonempty lists that never crashes head :: Nonempty a -> a head (Nonempty x _rest) = x What I'm getting at is that, yes, this is just the "shape" of our data. But you can encode more interesting and valuable properties in that shape than might be apparent at first. There are many other interesting examples of using types to ensure that properties that we want to hold for our values, do in fact hold. Edit: I should probably add that "If it compiles it works" is absolutely not always true. It's more of a community in-joke than an actual belief. But it does turn out to be true surprisingly frequently.

neolog 6y ago
Sure, you can encode various properties in some languages, but it's not that common to actually do so.
- sullyj3 6y ago
  In Haskell, it's both common and idiomatic. There's always a tradeoff between the usefulness of having static guarantees, and the complexity of the type system features that enable those guarantees. In some cases it's more trouble than it's worth to enforce certain static properties - you have to weigh the costs and benefits on a case by case basis. But it's nice to have the option, and Haskellers make use of it frequently.
  - heavenlyblue 6y ago
    You don’t need Haskell to do this however.
    - elbear 6y ago
      You need a type system that is expressive enough to allow you to encode logic in the types. Of course, Haskell is not only language with such a type system: PureScript, F#, Rust, OCaml, Scala have similar features, although not all.
  - tsimionescu 6y ago
    How many functions have you seen, in Haskell, that take Nonempty a versus taking [a]? There are reasons why this type of pattern doesn't scale well, and the Haskell designers knew it. Similarly, if they had defined head [a] -> Optional a, that would have produced complications of its own.
    - sullyj3 6y ago
      The general consensus in the community afaik, is that head :: [a] -> a in Prelude was a mistake, and the default should be to return a Maybe/Optional. Beginners are generally advised to avoid head, and all other partial functions in the Prelude, such as tail and the indexing operator, wherever possible, and rely on pattern matching instead, which is generally sufficient and more idiomatic for the relevant use cases. I agree that having the option to use a partial function is useful, escape hatches are important, but it shouldn't be the go to. Nonempty was just a simple example. You're right that it's not very commonly used (probably because it's not in Prelude), but the general culture of writing type safe interfaces and pushing guarantees to compile time %100 is a thing. A commonly used, more complicated example might be Servant, which is a web library which statically ensures your implementation meets an API spec.

sfvisser 6y ago

It works two ways though, which I think is important. Yes, type systems check the shape of your data which is nice. However, when sufficiently experienced, the type system also guides the developer into good program design. Type systems for me are more a design tool than shape checker. The checker/inferencer helps me learn about assumptions I make about data in specific parts of my code, which allows me to remodel my data types to better fit my intent. This works cyclic until things just seem to ‘fit’. Personally at least, this allows me to write far more complicated applications than I would ever be able to do without types. And it’s just very hard for me to imagine this wouldn’t be the case for any other developer.

lmm 6y ago

> I'm always a little frustrated whenever I see this aphorism perpetuated since I think it gives the impression that a static type system is doing more than it is actually doing. In type systems that are used outside of academia, the main thing your static types are doing is checking whether the shapes of your data and functions all line up. With some small exceptions, that's it: the compiler will tell you if your LEGOs fit together, but not if you've built a knife instead of a fork. Disagree. You can and should be using your type system to express your system design. If it's important that your utensil has at least 3 prongs, it should only be constructible by passing at least 3 prongs; that much is trivial to do even in Java, yet alone a language with a decent (i.e. ML-family) typesystem.

FullyFunctional 6y ago

I frequently have to defend why I hate Python but the foremost reason is that lack of static typing (which also makes reading other peoples codes harder than it need be). Static typing, especially in a rich type system like, e.g. Haskell and Rust, doesn't guarantee you don't have bugs, but it almost guarantees the ones that remain are better bugs, that is, application level bugs. However in my experience, I can usually tell what kind of code will be correct once it passes and which might still have issues.

tines 6y ago
Absolutely. The more experience I have, the more repugnant dynamically typed languages seem to me (for domains where they fit, i.e. I'm not talking about untyped assembly or whatever).
rxhernandez 6y ago
Which is absolutely bizarre to me because most of my experience with Python has been with people who are effectively scientists who don't give a rats-ass about good coding practices and yet I rarely had issues with receiving the wrong type. Don't get me wrong though, I spent the first 10 years of programming with C and Java so I understand the comfort that a statically typed language provides. I just haven't found it to be a big enough issue over the past 7-8 years of programming in Python to really complain about it. Frankly, if you were to ask me what the top 3 sources of my headaches in Python are, number 1, 2, and 3 would be, receiving a None value when I expected something else; but that's an issue with most languages.
- boloust 6y ago
  > Frankly, if you were to ask me what the top 3 sources of my headaches in Python are, number 1, 2, and 3 would be, receiving a None value when I expected something else Curious example, because that's absolutely something a sufficiently advanced and well-thought-out static type system can completely solve. You're right that the type systems of C and Java do not meet this bar, however.
  - 6y ago

pyrale 6y ago

> you don't even want to pay the type annotation tax for. 95% of annotations in the average haskell codebase are unneeded for compilation. People still write them, because they are a useful source of information when reading the code. So tell me, if you feel like you don't want to write down that one line of comment which happens to be checked against the compiler, I guess you probably don't write tests or documentation either?

jstimpfle 6y ago
> I guess you probably don't write tests or documentation either? Why would any experienced programmer make such a blanket statement? As always, it depends. Sometimes there is value in documentation (or whatever unchecked types in fancy languages), especially for stuff that is read a lot more, by other people, or yourself in the future. For a lot of stuff there is no point in writing documentation. For example, if the code is obvious and pedestrian. Or if you'll just throw away everything, or refactor a month later. And very often, writing documentation is not only a waste of time, but downright harmful, because code and documentation easily diverge. My personal advice (not just for documentation) is to strive on the side of doing as little as you can get away with, and only introduce structure and bureaucracy if there's a clear indication that it's required.
- garethrowlands 6y ago
  The fact that code and types don't diverge can make types useful as documentation, albeit limited documentation. Ideally the compiler figures out the types so you don't have to. Haskellers often find this useful when they refactor a month later.
  - jstimpfle 6y ago
    Code and types can very much diverge if the types aren't checked by the compiler, as my parent poster indicated. Case in point: type aliases instead of (Haskell) newtypes. Type aliases (which are unchecked, unlike newtypes) can lead to exactly the kind of diverging that I alluded to. Look at the mess that is all the typedefs and defines in the Win32 API for example. It's extremely hard not to pass in the wrong typedefs, and there must be extremely few programmers who know which aliases are the same on every platform and which could change. Aside, newtypes (Or the equivalent in C for example, wrapping a single member in a struct) can be very annoying. I would advicse against this, just like I'd advise against using type aliases.

q3k 6y ago

Agreed. I have a strong background in 'bad' programming languages like Go, Python, C. Half a year ago I had a short stint at a Haskell shop and was thoroughly disillusioned. That particular 'writing against the compiler' approach lended itself to write-once, over complex type juggling code. Because why make it readable - if it compiles, it works, and if it works, there won't be any need to read it, right? Well, except you still get bugs, and then debugging anything is like making sense of brainfuck. Maybe smarter people than me can juggle a handful of types and operators simultaneously in their head - I can't. My favourite example of 'just because it compiles it doesn't mean it works is' Maybe [a]. I've had a colleague scratch their head for hours over something like this: userCount :: Foo -> Int userCount f = length $ getUsers f This compiled, but always returned 1. Why? Well, because turns out `getUsers` returned `Maybe [User]`, and not `[User]` as the programmer expected, and somewhat asserted in their mind with types. And it also turns out that in Haskell, `length` takes a `Foldable`, and `Maybe` is a `Foldable`. Thus, a `length` of a Maybe will gladly return 0 or 1, which makes perfect sense from the point of view of the type system, but zero sense when it comes to humans. Whoops.

tome 6y ago
The Foldable instance for Maybe is one of the biggest warts in Haskell. It's not limited to Haskell, by the way. def getUsers(f): return (logged_in_users(f), logged_out_users(f)) def userCount(f): return len(getUsers(f))
- q3k 6y ago
  Sure, but Python and Python developers don’t hype up its type system to be the solution to all your programming woes :).
  - tome 6y ago
    I'm not sure what "Haskell developers" are saying, but this Haskell developer says "Haskell provides many tools that can be used to solve programming woes. One such tool is its strong and flexible types system (there are several other tools, such as immutability, functional style)."

cageface 6y ago

I find explicit null checking almost as valuable as static typing. Tests can cover a lot of the same ground as types but it’s very easy to have tests that don’t anticipate the nulls you only get in production.

boloust 6y ago

> I think it gives the impression that a static type system is doing more than it is actually doing This statement probably gets to the heart of the issue. A static type system isn't something that just "does things", nor can we conduct a proper analysis when the dialectic is reduced to "static vs dynamic". The first thing to realize is that there exists a spectrum in how much we encode in our type system. Even in weaker type systems like those of Go or Java, we can make illegal states unrepresentable, encode invariants, create typesafe abstractions, etc. Or we could just treat everything as object and not make any attempt to encode anything at all in the type system. In the former case, the aphorism "if your code compiles, it probably works", is more true than in the latter case. The next thing to realize is that the expressiveness of a type system places a ceiling on what can be usefully encoded in that type system. So in languages like Haskell, it's possible to get closer to the "if your code compiles, it probably works" ideal, than in a language with a weaker type system. But even in Haskell, it's possible to just write everything in IO and not make any attempt to encode your constraints in the type system. So in that sense, a type system is just a tool. If wielded effectively, it lets us offload a lot of work to the compiler in a sort of symbiotic back-and-forth. And some languages give us better static typing tools, to make that symbiosis more effective. But if we're not using simpler type systems to their fullest, we're not likely to be pushing against their limits, making it a lot harder to justify more advanced type systems. So "if your code compiles, it probably works" shouldn't be read as a statement of fact, but as an aspirational goal, one that we can move towards by more effective use of our tools.

jbotz 6y ago

> the compiler will tell you if your LEGOs fit together, but not if you've built a knife instead of a fork. OK, let's stretch that metaphor a bit. A powerful type system like Haskell's is really a way of both restricting which LEGO(tm) pieces you can use and designing custom new ones. So when you design and write software in truly idiomatic Haskell, after getting all your types lined up there is no way to make anything other than a fork.

higerordermap 6y ago

Not just shape of data, but the values that are allowed by data. I agree that it is an oversold fallacy and types get really clunky when pushed too far. But any worthy type system prevents lot of errors. This is not generally acclaimed by empirical studies claiming only 5% improvement because they are caught at compile time. Other benefits are enough to use a sufficiently good static type system, by the way, even for people that think type systems aren't better than TDD. * Better autocomplete * Better error highlighting - no need to run code or tests, IDE can highlight instantly. * No typos in variable names (can be achieved in some but not all dynamic languages) * Performance of compiled code

vindarel 6y ago
All 4 points why I like Lisp so much more than Python!

08-15 6y ago

> static types are ... checking whether the shapes of your data and functions all line up They definitely do more than that in Haskell. You can define distinct types with the same "shape", and the `newtype` keyword specifically creates a new type that has the same "shape" as an existing one, but is nominally distinct. This nominal typing, as it's called, allow you to express intent in types. Type checking then doesn't just check whether "shapes" line up, but also whether your intentions line up. If you express contradictory intentions, you probably made a mistake. Practically speaking, if the only types ever used in a Haskell program are `Int`, `Float`, `Char` and nested lists of those, all the type checker can ever do is tell me when I miscount square brackets or forget a `fromIntegral`. Those programs never run on the first attempt.

guenthert 6y ago

Yes, I'm somewhat puzzled that static typing seems so important to some, while it clearly only prevents one class of errors (and depending on the language, even that only to some extend, e.g. it's still possible to initialize enumeration class instances with invalid values in C++). I'd have expected that Eiffel's pre- and post-condition or design by contract in general, would have gained more traction with those who care about eliminating possible sources of programmer errors.

dirkt 6y ago

> you don't even want to pay the type annotation tax for. You won't understand those aphorisms as long as think of "type annotation" as something useless, "tax-like". I know where you come from, in languages like Java it is a tax - you repeatedly write long-winded types in different places. With type inference, that changes. You have a REPL (or IDE integration) that you can just ask for the inferred type as soon as you write a function. Then you look at it, you think about if it expresses what you want the function to do (that already catches some errors), you copy-and-paste it, make it a bit prettier, and bam, type annotation is done. It's even on an extra line, you don't have to attach it to arguments. Or, you design with types ("test first style", think of the type annotation as a test). You first write down the type, then you write the function, and you see if the type checker agrees. If it doesn't, you probably found a bug. Or your idea of what the function should do was wrong (has also happened to me). And everyone who uses that system does know that type checks are very dumb checks. They only help against dumb errors. But the majority of bugs are dumb bugs (at least the majority of my bugs) - misspellings, you forget to write out some part, etc. Those get caught. The hard bugs won't - that's what tests are for. (And automated testing is again simpler in the presence of types, see Quickcheck). > and encourage the pursuit of bad abstractions like 18-arg functions It never does. 18-arg functions are just unwieldy. If your function grows to that point, refactor (or rather, refactor long before that). And again, the type systems helps with refactoring. (Yes, I know I won't convince you, this debate has been going on for at least 30 years. OTOH, it doesn't hurt to see the opinion on the other side).