15

I keep reading stories from developers who state that once they are able to get the FP programs written in languages like Haskell, Ocaml, Elm and even Rust, to compile without errors, they are pretty sure that the programs will work correctly.

They usually state that it is mostly due to the type systems of those FP languages. So how do the type systems in FP languages like Haskell, Elm etc, differ from those in languages like Java, Delphi and C#?

I am familiar with the latter and aware of how the compilers catch errors when function signatures and parameter types don't match, but it seems that the type systems of FP languages extends to the kind of logic, operations or domains where calls to the procedures will work.

Can anyone give a good explanation?

UPDATE: With reference to What exactly makes the Haskell type system so revered (vs say, Java)?, I have to say that I don't understand the answers to that question. The answers seem targetted to those already familiar with functional programming.

  • I think it's because they're just skipping over many other attributes that functional languages do by default. Whether your code compiles or not, you probably have some level of immutability that is a given.. – JeffO Apr 19 '17 at 13:43
  • The question softwareengineering.stackexchange.com/questions/279316/… seems to be identical to mine, bu I find the answers incomprehensible. It just contains lots of new definitions which the OO programmer probably doesn't understand. I know I don't understand those terms – vfclists Apr 19 '17 at 16:46
  • 1
    @vfclists all the answers or just the top one, some of the lower answer are more approachable imho – jk. Apr 19 '17 at 17:58
  • I should point out, particularly for Haskell and Elm, and to a lesser extent Rust and O'Caml, most of what makes this possible has to do with the semantics of the language and much less to do with the type system. People stating that this is mostly due to the type system are incorrect, in my opinion. Indeed, Elm's type system is more or less completely subsumed by e.g. Java's or C#'s. – Derek Elkins Apr 20 '17 at 0:00
25

tl;dr summary: they are more powerful, more expressive, and most importantly, they don't lie.

There is an interesting correspondence between computer programs and logic systems. This was first noticed independently by Curry and Howard, and is now known as the Curry-Howard Isomorphism. In a certain mathematical sense, a program written in some programming language is isomorphic to a proof in some formal logic; a type in some programming language is isomorphic to a proposition in some formal logic: a proof is a program, and the formula it proves is the type for the program. The return type of a function corresponds to a theorem, the parameter types correspond to the hypotheses, and the function code corresponds to a proof that given the hypotheses, the theorem holds.

Since every type system gives rise to a system of logic (and every system of logic gives rise to a type system), we can look at different type systems by looking at the systems of logic they induce.

But I won't go deep into mathematical logic and type theory here, not the least because I am neither a logician nor a type theorist. I'll try to stay on the practical side.

Intuitively speaking, you want your type system to induce a system of logic that is consistent, i.e. that doesn't allow false theorems to be proven. The more inconsistent the system of logic induced by the type system is, the less useful the type system is as a proof of correctness of the code.

Now, let's look at a couple of (simplified) languages. Let's start with a language like Idris, for example. In Idris, when a function has a return type of String, it always returns a String. Now, you might say that's obvious, of course a function that is typed as String returns a String … but does it, really? Is it really that obvious?

Let's look at Java! Here's what a method typed as String can return in Java:

  • a String
  • null
  • an exception
  • and it can even not return at all (e.g. run into an infinite loop)
  • in addition to that, it can also return a "modified state of the world" (e.g. it can print a line of text to the console)

So, there are several ways for a method in Java to not return a String (either not return at all, return nothing, return something else, return something in addition, or several combinations of the above) even when its type says so.

I said above that there is a correspondence between programs and logic, and without going into the mathematical details of what all of this means, you can certainly imagine what happens when you try to prove something using a system of logic that allows you to "lie" like that!

A similar thing applies to the parameter types: a method that has a parameter of type String can also take null as an argument, and in addition to that, it can open a database connection, open a file, open a network connection, read from the console, use a random number generator, use reflection, all to get additional inputs, which do not show up in the parameter list.

This gets even more obvious when we throw Parametric Polymorphism (called Generics in Java) into the mix. Parametric Polymorphism means that functions know less about their types than when the types are concrete; ironically, this allows us, as the programmer, to know more about what the function does from just the types. A typical example that is often given to demonstrate the power of parametricity, is this mystery function:

mysteryFunc :: (a, b) → a

or in Java syntax:

<A, B> A mysteryFunc(Pair[A, B] p)

What does this do? What is the name of this function? Now, you might say, how can you know that from just the types, without any documentation, without the name, without the code, but the thing is: you can, thanks to parametricity. The function gets passed a pair of values, one of type a and one of type b. What can the function do? It can't return the second value, it is of the wrong type. It can't get a value of type a from somewhere else, because there is no "somewhere else" – if it wanted to get an a from a database, for example, it would have needed to take a DB handle as an argument. It cannot construct an a, because a is a type variable: the function doesn't know anything about a, and how is it going to construct something it doesn't know what it is?

So, the only possible thing it can do, is return the a it was passed – in other words, this is the fst function, which returns the first element of the pair it was passed.

There are other examples, e.g. a → a can only be the identity function, there is no other function that has this type.

Now, none of this is true in Java. The Java method can go and retrieve an A from a database, it can use reflection, it can do lots of other things.

If we assume not only such a "logical" type system, but also a "logical" programmer, it gets even more interesting. Let's take the following function type:

Bool → Bool

There are several things this function could do:

  1. return the boolean that was passed in
  2. ignore the boolean that was passed in and return a constant
  3. return the result performing some operation on the boolean that was passed in

Now, as you noticed, without parametricity, there is a lot less we can say about the function. However, there are a couple of things we can assume:

  1. This is just the identity function for booleans. It doesn't make sense that a programmer would write it that way. Either there is an already existing identity function in the standard library, then she would use that; or there isn't, and she really needs to write it herself, but since the function doesn't actually look at the value at all it doesn't care what type the value has, and it would have the more generic type a → a.
  2. Similar to above: if the function ignored its argument, there wouldn't be a need for the argument to be a boolean, and the type would be a → Bool.
  3. So, this leaves us with option #3: the function returns the result of some operation on the value; the only unary operation on booleans is negation, so this is the not function.

This is much less strong than our result for the fst function above, since it does not rely solely on the logic of the type system, but also on the "well-behavedness" of the programmer.

There are some important things that make all of this work:

  • Parametricity
  • Referential Transparency / Purity
  • Totality

Java doesn't have full Parametricity, there are things you can do with values even if you don't know their types, for example you can test for reference equality (==), you can convert it to a string, you can compute its hash code, you can cast it. Worst: you can get its class, then get that class's constructor, and construct a new one.

Java also doesn't have Referential Transparency / Purity (which essentially means that the value of an expression or the return value of a function depends only on its constituent sub-expressions or the input arguments to the function; it also means that any function call and any expression can be replaced with its value everywhere in the program (and vice versa) without changing the meaning of the program; intuitively, it means that functions and expressions cannot have side-effects). So, not only can Java construct a new a using reflection, for example, but it can also print to the console, mutate global state and do pretty much everything it pleases.

That's why when presented with a signature such as a → a, all we can say is "this could do literally anything, including launching the proverbial nuclear missiles".

Now, Haskell does have Parametricity and Referential Transparency, so in Haskell, we can say a lot more, specifically, we can say that if this function returns, then it is the identity function. IOW, it can either return its argument, or it cannot return at all (e.g. infinitely recurse). There is no other option. These are the only things it can do.

Idris, additionally, is Total, which simply means that functions are defined over all their argument values, i.e. they always return a value. This removes the last alternative, and means that a → a can only be the identity function. (Incidentally, this also means that Idris is not Turing-complete, but that is actually not a big deal: Idris is "Tetris-complete", meaning it can do I/O, it can do Foreign Function Calls, it can do interactivity.)

So, this is one piece of the puzzle: the fact that a program type checks tells you a whole lot more about the program than it does in e.g. Java. A function that has type String and type checks really does return a String and doesn't do anything else. This means that you can have a lot more trust in the types, and the types can tell you a whole lot more about the program.

We can say that, since types are theorems and programs are proof, we can have more confidence that the proof is correct.

The other piece of the puzzle is that type systems such as Haskell's or Idris's are much more expressive. So, not only can you have more trust in the proofs and the theorems, but the theorems you can write are also more "interesting"! I mean the fact that a function that claims to return a String really does return a String is a nice property to have in and of itself, but the statement "Hey, I return a string" is something you can also write in Java. (You just can't guarantee it's true.)

However, the type systems we are talking about here, can express much more interesting properties. At the extreme end of the scale are dependently-typed languages which can express any property that you can express using formal logic as a type, and then consequently type-check it. For example, in a dependently-typed language you can express the fact that a function that zips two lists preserves the lengths of the list, you can express the fact that a function that concatenates two lists returns a list whose length is the sum of the lengths of the input lists, you can express the fact that a function that sorts a list returns a list that is, in fact, sorted, has the same length, and the same elements as the input list.

For example, the Idris standard library has a Vect type that is a list that also carries its length in the type. Here's the type of the append function:

app : Vect n a -> Vect m a -> Vect (n + m) a

As you can see, the collection is not only parameterized over its element type (like e.g. a Vect<A> in Java), but also over its size, which is a runtime value! Imagine a Vect<A, n> in Java that is instantiated like new Vect<String, 3> … pretty crazy, huh? Dependently-typed languages are called "dependently-typed" because static types can depend on runtime values – this is the ultimate in expressive power, and essentially blurs (or rather obliterates) the distinction between Automated Theorem Proving and programming: a type can express anything that logic can express, which means everything you would normally write in a formal specification document, you can instead write as a type. And if the program compiles, then it is at the same time also a correctness-proof of its implementation wrt. the specification.

However, not all languages are dependently-typed. Most other type systems, such as Haskell's or ML's lie somewhere in between. But still, there are some interesting things that can be done with types. For example, there is a company called Galois in the US that does interesting things with Haskell; among other things they have a document management and document sharing platform for government organizations where they have encoded the rules for distributing classified documents into the Haskell type system. You literally cannot write code that accidentally (or even purposefully) leaks classified documents or distributes them to the wrong people: it simply wouldn't compile, it would be a type error.

So, there you have it:

  1. the types are more reliable in that they actually ensure that what they claim is true
  2. the types are more expressive in that you can claim more interesting properties
  • A bool->bool function which ignores its input and always returns true or false may be passed to code that expects a bool->bool function; such code might not be able to accept a function which didn't have any declared parameters. – supercat Apr 19 '17 at 19:09
  • 1
    @supercat I don't understand what you mean: a function which didn't have any declared parameters wouldn't be a Bool->Bool function; it would be a ()->Bool function. – ShreevatsaR Apr 19 '17 at 20:43
  • @ShreevatsaR: My point is that a function which is declared as bool->bool but ignores its parameter and always returns false could be passed to a function that expects a bool->bool function, which would not be the case for a ()->bool function. Unless I misread what you were trying to say, you seemed to be suggesting that a function which ignored its argument would be equivalent to one which simply didn't take an argument in the first place. Or does a->bool have a meaning different from ()->bool? – supercat Apr 19 '17 at 21:06
  • 3
    @supercat: Yes, a → Bool is a polymorphic function which takes an a and returns a Bool, () → Bool is a function which has no arguments and returns a Bool; they are completely different. – Jörg W Mittag Apr 19 '17 at 21:09
  • 3
    This is the most gangster answer in the history of stack. Great stuff and thank you @JörgWMittag – Jamie Strauss Apr 10 '18 at 6:15
9

Mostly what functional languages do a lot better is put more of the program under the purview of the type system. For example, what's the return value of a for loop? In an imperative style, you use for loops all over the place and the type checker can't help you at all with them. In contrast, in a functional style you would use a map, filter, fold, or even recursion instead of the for loop, all of which have very strong type semantics.

If you avoided impure functions and imperative loops in an "imperative" language, you would have a similar experience to people programming in "functional" languages, as far as typechecked programs tending to work, although your program would be more verbose than one written in a language designed to be written in a functional style.

  • 1
    This is a good answer but I feel it's a bit incomplete without touching upon the lack of null in the type system and maybe how ADTs differ from inheritance. – Doval Apr 19 '17 at 17:09
  • This answer illustrates why I find the answer to the similar question so difficult to understand. I don't know what makes a function impure and don't understand how a type declaration in a FP differs from one in an OO language that will lead to more correct programming, unless the functions applied to the type are used by the compiler to type it further. – vfclists Apr 19 '17 at 17:13
  • Are there any articles with side by side comparisons show how the typing of FP languages will support correctness better than with an OO language? – vfclists Apr 19 '17 at 17:15
  • @vfclists ok so there are a lot of new concepts for you to grasp, luckily you are already on a site that has explanations of them ;) – jk. Apr 19 '17 at 19:15
4

First of all, though Haskell is far and away my No.1 language, let's be clear that it's an exaggeration to say everything which compiles is correct. New code quite often does something weird even if it compiles. However:

Parametricity

If (idiomatically written) Haskell compiles and you've tested it sucessfully for any single scenario, then it usually also works with all possible inputs of the correct type. And thanks to parametric polymorphism, you can often take code which eventually does some rather tricky task, but test it in a “dumbed down” form that's easier to analyse. The type system then guarantees that the production variant will work in the same way as the test.

So that's one aspect of the power or Hindley-Milner type systems: they hide complexity when it isn't needed, allowing you to “inject” the complexity only when it is needed. Type inference is crucial here. It's actually a bit similar to dynamic or otherwise duck-typed languages (Python, C++ templates) in that regard... with the difference that the actual instantiation-dispatch is not eventually handled by some kind of type...is, template specialisation, dynamic_cast etc. (which can lead to surprisingly different behaviour for different instantiations and, in the dynamic case, fail if you pass different-type values in a single structure that should be homogenously type). And certainly not by weakly-typed coercions, which are either unsafe and slow (JavaScript, PHP) or horribly unsafe (C). Instead,

  1. Full parametricity means that all types must be handled the same way. A function forall a . [a] -> [a] can only reorder elements, but never mess with the elements themselves. Such a function, if you've tested it only with integers as [Int] -> [Int], is thus guaranteed to behave the same way no matter what elements are contained.
    Now, that's in principle also possible by simply storing opaque references. A C function

    void reorder(void** ptrs, int arrLength)
    

    can also never actually use those values, only (destructively) reorder them. However, in imperative languages this is really limited to so simple examples. As soon as you e.g. want to store stuff in differently-shaped structures, it's not enough to have one single array lying around. But if you rewrap these values in, say, a tree, you will never be able to do anything with them without first casting them back to a concrete type – which you've hopefully have well tracked, but the compiler can't help you with that.

  2. If, in Haskell, you do need to actually do something with the generically-typed values contained in a parametric container, there's a well-controlled mechanism for this: type classes. A type class C overloads some simple, basic operations over different types, grouped together in such a way that it's clear how the methods must play together. These “laws” can then be used when you write generic code (say, a function f :: C a => [a] -> [a]), to prove that it will always actually behave correctly. Because the laws are so abstract, it's clear (if not always easy) what you need to prove when adding support for a new type. The proof that, in addition to all these elementary methods, also f will work correctly comes then from the type system.

    Simple example, the Ord class of all comparable types a:

    class Ord a where
      (<) :: a -> a -> Bool
      ...
    

    gives rise to the function sort :: Ord a => [a] -> [a]. The law in this case is just the strict-weak-ordering property, which in other language is generally added as a comment to the sorting function. Well, in Haskell, these kind of laws need only be mentioned once, in the type class. This again reduces the amount of testing to be done.

Interfaces

This will be a bit hand-wavy. The thing is, types basically matter whenever something passes through a well-specified interface. Now, functional programming styles do that all the time: you pass data explicitly in as arguments, and retrieve results as return values. There is no hidden state that somehow also gets passed around, mutated, changed its structure in a way that's not reflected in the types.

And this comes in our advantage in mainly one way: code that once worked correctly will not suddenly go wrong if you change it slightly. The reason being, any change (change of the kind that actually becomes necessary when maintaining a real project – migration to a different library etc.; I'm not talking silly program-logical mistakes, those happen mostly when writing new code) will usually cause some local values to have different types. Now, that is traditionally a nightmare:

  • In procedural, strongly typed languages, it means you need to change hundreds of type declarations. Hopefully the compiler will actually show the right spots (in my experience, it will more often show mistakes in completely irrelevant spots!), but even if you've found the spots it's still often not easy to determine what changes you actually need to make. Often, you also need to change some control flow in the process. Lots of work, and lots of mistakes you can make in the process. It's also quite common to actually do unnecessary work, because type errors showed up in places that would have worked fine, but only after you've changed the types elsewhere.

  • In dynamic languages, you don't see any problems at first. Only, the test suite will go berserk. But even small unit tests can often not show you what's actually wrong, only that something is wrong.

Now, OO encapsulation does a decent job of avoiding these problems, but at the prize of quite some boilerplate and often also efficiency.

Hindley-Milner languages don't need this, because they have smart type inference: local bindings generally don't need any type annotations at all, the compiler will determine it. If some library type changed, the compiler will take that into account, change all relevant local bindings, and only show up an error if the new types really can't be reconciled with the old code. At the same time, explicit top-level signatures prevent errors from turning up far away from the actual cause.


Further reading:

https://github.com/Gabriel439/post-rfc/blob/master/sotu.md#maintenance

Not the answer you're looking for? Browse other questions tagged or ask your own question.