Hacker News Reader

Comment by dododo | Hacker News Reader

it's a matter of how much you put into the type system:

  add :: Integer -> Integer -> Integer
  add x y = x * y

in any moderately complicated code, you need to test. types only go so far.

View on HN

To supplement "it's a matter of how much you put into the type system":

This error can be caught if you put units of measure into type system. F# can do this, and addition function will have type int<a> -> int<a> -> int<a> while multiplication int<a> -> int<b> -> int<a * b>; for example, int<m/s> -> int<s> -> int<m> might be a function taking velocity and time, and returing distance. I think Haskell has libraries for this.

Similarily, add x y = x - y would be detected if (-) required a group, while (+) worked for monoids only.

However, it would be rather hard to create a type system detecting a typo in:

quadruple x = 3 * x

> it's a matter of how much you put into the type system:

It's also a matter of how much polymorphism you have. There are lots of functions `Integer -> Integer`; there is only one total function `a -> a`. (This is the parametricity theorem mentioned by sanxiyn in http://news.ycombinator.com/item?id=4215055 .)

There are lots of different functions `a -> a`. One could take a few cycles to complete, whereas others could take a day or week to complete. One could use a few bytes of space, whereas others could use megabytes or gigabytes.

I think that this is a different meaning of 'different' from the one usually recognised in computer science; it's my understanding that what usually matters is extensional equality (are the same outputs (eventually) produced for the same inputs?) rather than intensional equality (are those outputs produced in the same way?). Otherwise, all compiler transformations would be illegal.

(You could argue that a (correct) transformation that sends space usage way up may actually change even extension equality, in the sense that it could result in the transformed algorithm failing on a given piece of hardware when the original algorithm would have succeeded. However, my understanding is that the state of 'realistic' computer science, where hardware limitations are part of the reasoning, is in a much more primitive state than 'idealised' computer science.)

Opaque types like "Integer" don't give a lot of assurance, so either you get a stronger type system (Agda-style) or you have to test.

But complicated code may work with non-opaque types, and so it could still be reliable without tests.

Reply on news.ycombinator.com