Against the definition of types

Re:Against the definition of types by saosebastiao on Thursday May 14, 2015 @04:28PM (#9547388)

This was a great essay. Type systems are one of the holy wars of programming, and I don't think there will ever be a truce. I think it is is great to see some writing that explains why that occurs, and how to think about the situation. It is also interesting to see some things that I haven't thought about: Type systems can encode effects that could free the programmer from thinking about locks? Dependent Type Systems can perform program synthesis? Where can I find out more?

I know anonymous predictions from nobodies on the internet are completely uninteresting, but I can totally envision this as one of the essays that gets linked hundreds of times over the next decade or two on the front page of HN with a (2015) in the title.

[ Parent | on HN ]

Re:Against the definition of types by tpetricek on Thursday May 14, 2015 @07:48PM (#9548216)

If nothing else, your anonymous prediction pleased the author :-). Thank you!

[ Parent | on HN ]

Re:Against the definition of types by tel on Thursday May 14, 2015 @04:44PM (#9547476)

Dependent type literature will answer both of your questions relatively quickly. Also look at "proof search" in that context.

[ Parent | on HN ]

Re:Against the definition of types by andrewchambers on Thursday May 14, 2015 @07:33PM (#9548166)

I personally think a truce is coming with python3 static typing. As long as type systems have an 'any' type which is the default, then dynamic languages and do everything.

[ Parent | on HN ]