[hansvm]

I mean, there are (2^32)^(2^32) functions matching (int)->int, and many of them are both important and vastly more complicated if you ramrod them into a "types uniquely define behavior" mindset. Such issues become more common as code grows more complicated. You can alleviate a ton of problems by using the type system to assert a list is sorted or a string is HTML-escaped or whatever, but the general case is both very much not solved and not reasonably solvable.

[Laaas]

In practice, all simple behaviour you want can be expressed succinctly. If you want it to have complex behaviour, the type is complex. This is no different from using natural language to describe the problem. If for example we want it to implement multiplication, how would we do that? We'd operate not on built-in integers (which have the operation already), but e.g. on an explicit list of bits. Let's make the list length indexed. We get `mult : Vec n Bool -> Vec m Bool -> Vec (n + m) Bool` This is not enough to constrain it. We add `mult 1 n = n`, `mult n m = mult m n`, `mult 0 n = 0`, `mult n (mult m o) = mult (mult n m) o`, and finally, `mult n (add m o) = add (mult n m) (mult n o)`. This uniquely characterises multiplication on the natural numbers.

In natural language, it might suffice to say "implement multiplication", but this is because it _knows_ what multiplication is beforehand. If it did not, and only knew how to code, you would effectively have to restate the exact same properties. This will more often be the case when you're not dealing with trivial examples.

[imtringued]

I'm sure the demoscene could do a lot with that signature.