Discussion! Practical Aspects of Types

Notes on why type theory is important

Pete discussed his experience with writing the Cardelli type checker.

• Js implementation first, found several bugs that were type errors while writing it. Got it working, but he found it unstatisying.
• Haskell implementation he found really made him understand it.
• made the point that types give you faster feedback on programming errors

Leo

• Brought up the exploratory phase of programming, showed us an example of a mud ball in action.
• an example of the figure out what your program will do and how to structure it by writing an example. In that context, figuring out a clean high level design is an unnecessary complexity as the problem is still being understood.
• most people who say they like untyped better don't understand what a typed language is

Ben

• Python module packaging, language has no clean construct for doing something he wanted that is available in Haskell.
• brought up the Haskell lens module as an example of something that might not have happened without type systems, also the parser combinator.
• Python library APIs are often bad, but Haskell library APIs are often good. This could be because types make people think more clearly about boundaries and concept separation.

Chris

• "I would murder for a type system", when discussing cases where deep inside a Lua code base it becomes unclear what the type of a variable is. Figuring that out means trawling the execution path and the rest of the code base, types would fix all of that.
• put out the idea that maybe untyped is easier to write with, but types can make for better code overall.
• Milner's quote that types are the leaven of programming

Dann

• Gave an alternative viewpoint on Ben's lens example saying that lens was more a reflection on the fact that modifying internal state in a functional language is hard and it is more of a workaround than an important discovery. Ben tended to agree.
• we can say a program is sound or well-typed which is one aspect of type checking and inference, but types also impact the developers thought process so it is not some abstract math exercise even though some of the sections of the type theory papers do read that way.

Scott

• Can type systems help with packaging a library for distribution? I think we decided yes, as they more precisely specify interfaces, but only so much, can't solve all problems.
• The motivations for studying type theory come from very different places, Martin-Loef type theory aims to understand the foundations of mathematics, Cardelli wants to pragmatically write programs better, but they both arrive at some similar ideas. Dann then mentioned that Church, Turing and others probably considered themselves mathematicians, computer scientist may have been an insult.