> exist in your head if you're implementing a function like max(a, b)

surely, you have an idea of what you're using that function for, while you're writing it.

The compiler is doing a check to see if the function makes some minimal logical sense (ala, a typecheck), but it cannot read your mind. But this implies the types are actually an actualization of the thoughts in your head, in a formal manner.

The type is encoded in the name of the function.

Is a pretty bad system because you say "won't even exist in your head" but I dont even know if I should pass it integers, floats a srtring. Or what it will return.

Because inside the abstraction max it doesn't represent a width or height, they are just numbers (or just some "comparable things"). But outside the abstraction, at some level, you'll definitely know what a and b are.