http://www.lambdassociates.org/blog/bipolar.htm

In particular, unit tests cannot guarantee the absence of behavior. As an example, Haskell can use its static type system to say, "this function (and any functions it uses) is guaranteed to be pure". Or you can say, "this function (and any functions it uses) is guaranteed to only use certain side effects, but other side effects do not happen".

Languages like Idris go even further and can guarantee that a function terminates (never goes into an infinite loop)!

As another example, Haskell has Software Transactional Memory, and it uses the static type system to guarantee that arbitrary I/O cannot occur, which is important because the transaction might be retried multiple times.

I don't remember which language it was in, but I remember reading about a language that used static types to guarantee that exceptions are always handled. In other words, you will never have an uncaught exception.

Nulan uses its static type system to make a distinction between blocking impure functions and non-blocking impure functions. In JavaScript, there's a big difference between blocking and non-blocking, both in terms of behavior and performance. By using the static type system, it's possible to say "this function (and any functions it uses) is always blocking, and never non-blocking".

As you are aware, Rust uses its static type system to guarantee that pointers are always used correctly, and that data races cannot occur, even with concurrency.

But the biggest reason I like static types is because they make refactoring easier. Let's say you have a type that represents a person. So you have a name property, age property, etc.

Now let's say you want to add in a new property. Some of the existing functions will need to change to accommodate this new property. Without static types, you need to carefully go through your entire code base and find the functions which use the type, and then change their behavior to work with the new property.

Unit tests won't help you with that, because the unit tests are all testing the old properties, not the new property. So in the end, you have no choice but to just bite the bullet and spend a significant amount of time searching through the code and making the changes.

But with static types, it's as simple as adding the new property, compiling, fixing any type errors, compiling, fixing any type errors, etc.

Each type error tells you the file and line where the error occurs, making it easy to fix. You don't need to search through your code to find the places which need fixing: the type system does that for you. And after all the type errors are fixed, it's basically guaranteed that your code is correct.

Another example: a function used to always return a result, but now you need to change it so that it can potentially fail. So anybody that uses that function now has to account for the possibility of failure. With a static type system, you simply make the change and fix the type errors.

With unit tests, you better hope that you have 100% code coverage, because you're going to need it to find all of the functions which need to be changed. And don't forget that the unit tests need to be updated, and you probably need to add in new tests as well. That takes time, in addition to the time spent fixing the code.

So the end result is that it's faster and easier to refactor with a static type system, and it's more likely to be correct as well.

So I think static types and unit tests complement each other: they can both do things that the other cannot. Static types can make guarantees that unit tests cannot, and static types also remove some of the burden from unit tests, which speeds up development without sacrificing correctness.

On the other hand, unit tests can make certain guarantees that static types cannot. So in the end, I think you need both.

P.S. Static typing also helps tremendously with things like smart IDEs. I think Unison is a really cool example of that:

Typeclasses are amazing. They're similar to multimethods, but more powerful, and they have the same performance as regular functions.

You can use them to solve the expression problem, giving you a huge amount of flexibility, power, and conciseness. Or you can use them to create dynamically scoped variables which actually work correctly (unlike dynamic variables in most languages).

The thing is, typeclasses are only possible with static types. They're the main reason I changed Nulan to be statically typed.

----

By the way, I would like to point out that the static type systems in languages like Haskell is very different from the static type systems in other languages like C, C++, or Java. So even if you like/dislike one of them, you might end up liking the other. I used to lump all of the static type systems together, but I think that's a mistake.

"There have been two really clean, consistent models of programming so far: the C model and the Lisp model. These two seem points of high ground, with swampy lowlands between them. As computers have grown more powerful, the new languages being developed have been moving steadily toward the Lisp model. A popular recipe for new programming languages in the past 20 years has been to take the C model of computing and add to it, piecemeal, parts taken from the Lisp model, like runtime typing and garbage collection." (http://www.paulgraham.com/rootsoflisp.html)

Let's keep chatting offline. There might be issues I run into that you know how to deal with, or vice versa. Can you send me an email? My address is on my profile.

Edit 16 minutes later: I've gotten Arc running on Windows. Here are the instructions I followed:

0. Install Racket and Git like above.

1. Open Git Bash from the Windows menu and run this command:

    git clone https://github.com/arclanguage/anarki

    (current-directory (find-system-path 'home-dir))
    (current-directory "anarki")
    (load "boot.scm")
    (tl)

  tl: undefined;
    cannot reference undefined identifier
      context...:
        C:\Program Files\Racket\collects\racket\private\misc.rkt:87:7
    tl: undefien

> I've installed racket-6.4-i386-win32 and Git-2.7.4-32-bit

> (current-directory (find-system-path 'home-dir))

> (current-directory "anarki")

> (require "boot.scm")

> (tl)

Rtl: undefined; cannot reference undefined identifier context...: C:\Program Files\Racket\collects\racket\private\misc.rkt:87:7

> stdin::107: read: unexpected `)'

  context...:

   C:\Program Files\Racket\collects\racket\private\misc.rkt:87:7

In my experience, the bug doesn't occur as long as the text I'm pasting has a newline at the end. Maybe you could try that. That is, instead of just selecting the text you want to copy, select a blank line after it too.

Alternatively, you could type everything by hand instead of pasting... but that sounds pretty painful. Hopefully you don't have to resort to that.

Programming is my life. I like to think I'm a master of it. But I'm completely alone. Also I hate my jobs, I hate big companies, I hate bullshit, I hate TDD, I hate code reviews, I hate estimations; it's a pain man.

Poker, while definitely not as deep as software, is the exact opposite. They do TDD? I take money. They do code reviews? I take money. bullshit? a fountain of money...

I'm constantly looking for people to hack with as well. Some ideas:

a) We could work on anarki. For example, try out the latest version sometime when you have time and let me know if mktemp broke again on Windows. Help kinnard and me expand the install instructions for Anarki to Windows. Neither of us knows how to run Arc there, so this would be very valuable. These small-ish ideas might be the start of a larger project.