Discussion on: Convince me that types are awesome

Imagine you have this function

def combine(a, b) = ???

how would you test this does what you think it should do? The way this is written combine can accept any a or b and can return anything

Now lets add some types

def combine(a: Int, b: Int): Int = ???

For your program to compile a and b must both be of type Int and combine must return an Int. This means rather than testing every possible input and output, you now only consider a tiny subset of the inputs/outputs you originally started with

Here's another example. This function is parametricly polymorphic in T (that's what the square brackets are saying), we must take a T and must return a T

def thing[T](a: T): T = ???

Can you think of an implementation other than this? Remember T can be anything, so the implementation must work for any possible T

def thing[T](a: T): T = a

I can't. And in fact the types have limited the space of implementations for this function down to just this and things like just throwing an exception or doing a side-effect.

Depending on your language you can go really far with this. In lots of FP languages OOP is never used and instead ad-hoc polymorphism (aka typeclasses) is preferred. The idea is really just an extension of the idea "my program won't even compile if the types don't work". If your language has higher kinds, you can meaningfully talk about things like IO and sequential/parallel computations. If you have a language like Idris with dependent types, you can do type-driven-development, where each time you compile your program you do a "proof of correctness" (note the quotes before you start yelling at me :) )