I think your last two points are important. I'll paraphrase and enumerate:
If something's too trivial, types are less obviously useful. As things get hard, types show benefits
With Maths "I'm free to pick (without extra effort) the notion of 'type' that's most useful for the problem at hand."
I think these are related. If you're writing a URI processor, you might be thinking in terms of email types, web types, telnet types, etc. An overly simple compiler might force you into the uniformity of the "String" type. That makes the compiler's idea types pretty useless. There are (at least) two easy ways to change the world to make types useful:
Make the program requirements bigger. If you have to deal with complex numbers as well as URIs, (and if the compiler can tell the difference), maybe types might start to be useful again.
Make the compiler better. By which I mean, "make the type system closer to the one in your head". Maybe you could have functions parse :: String -> [Email + Web + Telnet], and (filter isWeb) :: [Web + X for all X] -> [Web] (I've used "+" as type union here)
Almost the inverse of (2) is learning to encode whatever you're thinking into the type system of a language you know well.
I'm afraid I'm about to waffle a bit - I'll come back to (1) and (2) at the end, but I need to be clear about what I think a type is first:
I claim that all programmers have "types" in their head when they're programming. I don't claim that all programmers have "haskell types" in their head. I believe that in modern computer science, the definition of "static type" is "any property that can be known about piece of code without running it". Examples include:
"Will this code ever segfault?"
"Will this code ever try to divide by 0?"
"Will a malformed URL ever be passed into the http library?"
"Can there ever be information leakage of any kind from any of the variables marked 'high security' into any of the variables marked 'low security'?"
Some types can be checked by some compilers, while others can't (compilers do exist that can statically check each of the above statements). If there's something you want to know (presuming that it can be known - see the halting problem) about your code that can't be checked, I believe that to be the fault of the compiler. Given two otherwise identical compilers, where one can statically check if my code will ever segfault and the other cannot, I'll choose the first one. The problem is that they're rarely "otherwise identical", so we come to making engineering compromises. What information can the compiler give you? How valuable is that information? What freedom do you lose in exchange for that information? How valuable is that freedom?
Hold that thought for a moment - I'll come back to it in the next comment...
![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
no subject
I think these are related. If you're writing a URI processor, you might be thinking in terms of email types, web types, telnet types, etc. An overly simple compiler might force you into the uniformity of the "String" type. That makes the compiler's idea types pretty useless. There are (at least) two easy ways to change the world to make types useful:
Almost the inverse of (2) is learning to encode whatever you're thinking into the type system of a language you know well.
I'm afraid I'm about to waffle a bit - I'll come back to (1) and (2) at the end, but I need to be clear about what I think a type is first:
I claim that all programmers have "types" in their head when they're programming. I don't claim that all programmers have "haskell types" in their head. I believe that in modern computer science, the definition of "static type" is "any property that can be known about piece of code without running it". Examples include:
Some types can be checked by some compilers, while others can't (compilers do exist that can statically check each of the above statements). If there's something you want to know (presuming that it can be known - see the halting problem) about your code that can't be checked, I believe that to be the fault of the compiler. Given two otherwise identical compilers, where one can statically check if my code will ever segfault and the other cannot, I'll choose the first one. The problem is that they're rarely "otherwise identical", so we come to making engineering compromises. What information can the compiler give you? How valuable is that information? What freedom do you lose in exchange for that information? How valuable is that freedom?
Hold that thought for a moment - I'll come back to it in the next comment...