Hacker News Reader

Comment by lgessler | Hacker News Reader

> 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.)

View on HN

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.

Sure, you can encode various properties in some languages, but it's not that common to actually do so.

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.

You don’t need Haskell to do this however.

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.

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.

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.

Well, since the Prelude was never changed to at least add an alternative headMaybe, perhaps it was not seen as a deep enough mistake.

Yes, I am aware that the Haskell community generally tries to push more guarantees to compile time, and that Haskell's ease of defining and using new types equivalent to existing ones but that signify some property helps a lot in this.

Still, there is some limit to this. For example, you have many libraries adding measurement units for Haskell, and many libraries doing linear algebra. But you won't find too many people doing linear algebra with measurement units, because the types of intermediate results explode too much (e.g. a type-safe unit-of-measurement matrix multiplication of 3x3 matrices has 18 type parameters, with complicated restrictions between them).

Definitely don't disagree!

What complications would it have produced? Eg Elm has `List.head : List a -> Maybe a` and it's just fine I think?

In practice I've found that it leads to writing code that you know is unreachable, but you can't prove it to the compiler.

If you know the list can't be empty, can't you prove that to the compiler by using a non-empty list type?

Good point! last time I used elm i didn't know what a nonempty list was.

> How many functions have you seen, in Haskell, that take Nonempty a versus taking [a]?

Most take Foldable or Traversable.

When it's relevant your functions can be specialized into Nonempty.

We've been using this approach in Typescript. It's more palatable than Haskell since you can express an array that has at least one element as a variadic tuple `[T, ... T]`. Having the possibility to encode invariants in types is very useful, although it gets harder at times since TS chokes when you push it to its limits. Note that this happens in an old Meteor codebase that was completely JS a year and a half ago.

I find these generally worth it because you can surface those aspects up to the function signature. It would be a lot nicer to have a function signature that shows the limits than it is to have a failure and have to open the docs for the library to see what the limits are.

If the code is sound, it should have the same complexity anyways. I.e. putting a non-empty requirement in the function signature is just as complex as adequately handling an empty array in the code.

My personal struggle is that statically typed languages are annoying to prototype (I don't care if it segfaults on my laptop, I want to validate my idea). My struggle is prototyping in something that I can easily transition to a strictly typed version. I'm curious to try prototyping in Javascript and adding types when I move to production.

I used to think Javascript was a great prototyping language. In fact I specifically practiced prototyping with it -- my github is littered with repo's for each of my prototypes -- I call them the Laundromat Demos. I would use the 70-80 minutes I had at the laundromat to write a prototype for a game in JS.

However I've tried something similar with Haskell. I think I prefer Haskell for prototyping these days. It turns out you can get a long way playing with the types. Often I spend more time prototyping the types and they guide me to the implementation which is often quite small.

It takes some training and work to get there but I think Haskell, for me, is a better prototyping language -- I don't have to deal with undefined, accidental prototype overloading, etc.

+1, I'm impressed how far these prototypes can get you, especially if there's an extra layer of correctness on top of the existing Haskell type signatures. For instance, LiquidHaskell [1] can naturally shift you towards implementing most of the necessary validation and parsing logic as part of your work on precise type signatures.

[1] https://www.youtube.com/watch?v=zCJV0xNY06o

Interesting correspondence between your comment and sfvisser's:

https://news.ycombinator.com/item?id=24716903

For the curious, I suggest reading Philp Wadler's "Theorems for free!" which explains how to derive a theorem for a given type. Practically, this helps compilers make certain optimizations based on the theorems it derives from the types.

Are you sure? https://lobste.rs/s/yyhu4w/real_problems_with_functional_lan...

Shouldn't head return "Maybe a", since the head of an empty list would be "None"? (Not sure if I got the Haskell terminology correct.)

In a better world it would. Currently it the head of an empty list crashes the program. Many people in the Haskell world are really salty about this but they don't want to break the API for it.

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.

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))

Sure, but Python and Python developers don’t hype up its type system to be the solution to all your programming woes :).

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)."

And Python provides readable syntax. Your example has an easy-to-spot bug, just from reading the code and knowing Python's semantics. Haskell's "programmable semicolon" ends up being a problem here because, thanks to typeclasses, the programmer usually does not know which semicolon they are programming under!

"Python provides many tools that can be used to solve programming woes. One such tool is its strong and readable syntax." Do you see how empty this sort of platitude is?

I didn't intend to make this into a competition between Haskell and Python.

I don't think that illustrates that promotion of the type system as a useful tool is an "empty platitude". A well constructed syntax is certainly a nice feature of a programming language. One might say a language like brainfuck does not have a syntax which makes the code easily readable, and therefore is the worse for it.

Similarly, one might say that a strong type system is a useful tool. That doesn't make it a panacea (and I don't think that this was the claim), but that doesn't mean one can't appreciate it as a good tool.

The problem with this comparison is that readable syntax is a subjective notion, whereas type system is an objective thing that can be evaluated based on its strictly defined boundaries - it's either possible or impossible to encode all required software specification with a provided type system, and if something is not possible, we know exactly what are these things that don't fit into the type system, and therefore we cannot rely on the compiler to prove their correctness.

Er, the difference here is that we're given the Python code for `getUsers` but not the Haskell code for it. That makes the error in Python obvious. The incorrect `userCount` in Python looks just as obviously correct as the incorrect `userCount` in Haskell; and conversely, if we were given the code for the Haskell `getUsers` (or even just the type signature!) the error would be just as easy to spot.

To make this code clearer:

    def get_users(f) -> Tuple[List, List]:
       return (logged_in_users(f), logged_out_users(f))

    def user_count(f) -> int:
       return len(get_users())

Now it's clear this is just wrong code. To fix it:

    def get_users(f) -> List:
       return logged_in_users(f) + logged_out_users(f)

    def user_count(f) -> int:
       return len(get_users())

That doesn't really "fix it". Even assuming there are no other callers of `get_users` that you might be breaking here (possibly silently, since lists and tuples in Python have overlapping interfaces), you're making `get_users` less useful by dropping structure that at least someone, at some point, thought was useful.

Also, you should annotate the type of your lists :)

  def get_users(f) -> Tuple[List[User], List[User]]:
    return (logged_in_users(f), logged_out_users(f))

  def user_count(f) -> int:
    logged_in_users, logged_out_users = get_users()
    return len(logged_in_users) + len(logged_out_users)

That's why Lisp has multiple return values, which are different from returning a tuple. It's great for refactoring. (https://lispcookbook.github.io/cl-cookbook/functions.html#mu...)

Why does getUsers return Maybe [a] in the first place? It should be [a]. You can also implement your own version of length that works only with iterables of your choice. The language allows leveraging type constraints to achieve this, the fact that your team didn't use it doesn't indicate an inherent flaw in the type system you've been provided with. And if you want to go an extra mile, use liquid-base instead of base.

There is a substantive difference between "couldn't get any users because of an error" (Nothing) and "succeeded but found no users" (Just []).

But, if that really is the reason for Maybe [a] over [a], I'd still prefer Either SomeUsefulErrorType [a].

`Either` would be much better, no?

No, because `Either` is a `Foldable`, too.

I know, not what you meant. But a custom sum type would not only allow you to return multiple different failure cases, you also wouldn't give it a `Foldable` instance with surprising semantics.

Plain old data types are seriously underrated these days.

Right, so we essentially say that the provided example doesn't refute the "it works if it compiles" slogan. It just works according to the provided specification expressed in the types, and it so happened that the specification was not specific enough.

My specification doesn't make a distinction between absent users and possible error responses because I assume that errors will be processed elsewhere and the getUsers function is applied as part of the "safe core" interface that is not concerned about error handling. If the specification was more precise (even more precise than in your suggestion, for instance, getUsers :: SafeIterable a => Foo -> a and length :: SafeIterable a => a -> Integer ), it would work differently.

The issue in the example has to do with the clarity of the intent encoded in the type signature, not the inherent issue of the type system that cannot guarantee safe runtime of the example. That's why I mentioned type constraints for specific iterables as a possible solution to the encoding problem.

A better example of the compiled-but-not-working case would be something that currently cannot be expressed well by the type system, something like async exceptions or access to closed resources (will be covered by linear types soon).

Of course, "if it compiles it works" depends on you designing good types.

Haskell will never stop you from representing every value as String, and just throwing exceptions if the strings do not convert back, for example.

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.

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).

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.

> 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.

Is null even a type though? If not, then it would seem it's not a static type system that's solving it; it's something else entirely solving it (whether or not that something is contained in that specific type system).

The issue with null, as commonly implemented, is that null is a value that inhabits all types. So in that sense it is a defect of the type system.

In Common Lisp, T is the "any" type (which makes sense there, as type specifiers can be formed using unions using (or type-A type-B ...) lists), the value NIL is the sole instance of the type NULL.

Receiving a None or Nothing or a NULL or similar is something a type system can paper over or, more politely, force you to add code to ward off but there's something happening in the actual data, if not the real world, which is causing that non-value to be present and the type system can't fix that.

But is the issue receiving a null or is it how unexpected the null is? Assuming that functions always can return null is way too tedious, so in practice my issue with dynamic languages like Python is that I'm never sure whether a function can actually return null.

> 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?

> 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.

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.

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.

Curious to know what led you to interpret this:

> which happens to be checked against the compiler

as:

> the types aren't checked by the compiler, as my parent poster indicated.

(also type aliases are still checked. The check is less useful, but it's still a check)

> Why would any experienced programmer make such a blanket statement?

Because type annotations are less work than tests or documentation, don't suffer from falling out of sync like doc does, and because experience shows that haskell users typically find it useful to write types despite it not being necessary to compile. It would be surprising to skip types but invest in writing more complicated means of documenting and testing the software.

maybe I misread. I went with

> 95% of annotations in the average haskell codebase are unneeded for compilation

Like type aliases. They are not distinct types, so the compiler doesn't (can't) check that you're using the "right" name.

What I mean is that these annotations are going to prevent compilation if you get them wrong, but the compiler's type inference is good enough that you only need to provide types when there is ambiguity.

That means most of the type annotations written exist because developers find them useful for documentation.

> Ideally the compiler figures out the types so you don't have to.

Doesn't it cause unintended API breaks because type changed from, say, a single type to union type, without changing any annotations?

If that change goes through your whole program without causing any breakage, from Haskell's point of view it's a good change.

If you have an API that exposes data to external systems, that may cause an integration breakage, indeed. That is why Haskell users like to use libs like Servant, which let you specify your API as a type. This way, if you change your system, your API has to change aswell.

Another benefit of Servant is that you can generate swagger and clients for other languages easily, which your users can use in their own build to get type safety too.

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.

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.

> 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.

> 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).

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.

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

All 4 points why I like Lisp so much more than Python!

> 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.

> 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.

> 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.

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.

Reply on news.ycombinator.com