"No, I didn't think about writing typed version of this program. You know, I'm not "disciplined" kind of person so
type discipline is (for now) pretty foreign to me. :) I have the strange feeling that types hampers programmer's
creativity."
The underlined sentence is a compact summary of the reluctance that programmers often feel in migrating to
statically typed languages – that they are losing something, a degree of freedom that the writer identifies as
hampering creativity.
Is this true? I will argue, to a degree – yes. A type checker for a functional language is in essence, an
inference engine; that is to say, it is the machine embodiment of some formal system of proof. What we know,
and have known since Godel's incompleteness proof [9] [11], is that the human ability to recognise truth
transcends our ability to capture it formally. In computing terms our ability to recognise something as correct
predates and can transcend our attempt to formalise the logic of our program. Type checkers are not smarter
than human programmers, they are simply faster and more reliable, and our willingness to be subjugated to them
arises from a motivation to ensure our programs work.
That said, not all type checkers are equal. The more rudimentary and limited our formal system, the more we
may have to compromise on our natural coding impulses. A powerful type system and inference engine can
mitigate the constraints placed on what Racketnoob terms our creativity. At the same time a sophisticated
system makes more demands of the programmer in terms of understanding. The invitation of adding types was
thus taken up by myself, and the journey to making this program type secure in Shen emphasises the conclusion
in this paragraph.
The underlined sentence is a compact summary of the reluctance that programmers often feel in migrating to statically typed languages – that they are losing something, a degree of freedom that the writer identifies as hampering creativity.
Is this true? I will argue, to a degree – yes. A type checker for a functional language is in essence, an inference engine; that is to say, it is the machine embodiment of some formal system of proof. What we know, and have known since Godel's incompleteness proof [9] [11], is that the human ability to recognise truth transcends our ability to capture it formally. In computing terms our ability to recognise something as correct predates and can transcend our attempt to formalise the logic of our program. Type checkers are not smarter than human programmers, they are simply faster and more reliable, and our willingness to be subjugated to them arises from a motivation to ensure our programs work.
That said, not all type checkers are equal. The more rudimentary and limited our formal system, the more we may have to compromise on our natural coding impulses. A powerful type system and inference engine can mitigate the constraints placed on what Racketnoob terms our creativity. At the same time a sophisticated system makes more demands of the programmer in terms of understanding. The invitation of adding types was thus taken up by myself, and the journey to making this program type secure in Shen emphasises the conclusion in this paragraph.