head :: [a] -> 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!"
data Nonempty a = Nonempty a [a]
head :: Nonempty a -> a
head (Nonempty x _rest) = x
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.
head :: [a] -> a
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.
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).
Most take Foldable or Traversable.
When it's relevant your functions can be specialized into Nonempty.
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.
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.
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
def getUsers(f):
return (logged_in_users(f), logged_out_users(f))
def userCount(f):
return len(getUsers(f))"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?
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.
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())
def get_users(f) -> List:
return logged_in_users(f) + logged_out_users(f)
def user_count(f) -> int:
return len(get_users())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)But, if that really is the reason for Maybe [a] over [a], I'd still prefer Either SomeUsefulErrorType [a].
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).
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 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.
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.
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.
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?
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.
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.
> 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.
> 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.
That means most of the type annotations written exist because developers find them useful for documentation.
Doesn't it cause unintended API breaks because type changed from, say, a single type to union type, without changing any annotations?
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.
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.
Moreover, in OCaml it is idiomatic to use type inference everywhere except for interface files, so in practice you almost never annotate types.
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 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).
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 codeOK, 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.
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.
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'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.)