202206281449 Types, and why you should care

From a talk¹ by Yaron Minsky of Jane Street.

Typed vs. Untyped

• Untyped — scripting, lightweight, friendly, and slow.
• Typed — Serious, professional, unfriendly, verbose, and fast.

Some definitions

• Values — data, things
• Variables — can be different values, part of the lexical portion of the language
• Expression — composed out of variables, values, and other things
• Types — categorization system for values; groups values into named groups; strings, integers etc.
• In untyped language, values have types
• In typed languages, values, variables, and expressions all have types. (For instance, variable is typed when it always contains a variable of that type)

Why types?

• Make programs faster, typically through compilation/interpretation loop having “hints” and more information.
  • V8 for instance can be super fast, within a factor of 3 or so from a compiled language (but this is through herculean effort of thousands of people over tens of years and complicated things like tracing compilers and things)
  • This is predictable performance vs V8
• Make programs more understandable

So why don’t people always use them?

• Often make programs more verbose — when the language doesn’t have a convenient way to express something, it’s difficult to express it at all or in a good way
  • Gain concision back by expressiveness and type inference
• Can cause confusion
• Can create learning barriers
• Can slow you down.
  • All in, I think they definitely help you be a better and more efficient/effective programmer, but definitely for small things or prototyping.
• Interfere with your plan

Types help to

• Improve performance
• Detect errors
  • Can find real semantic bugs and misunderstandings when using types to model your system
• Communicate your intent and model your system. It’s documentation that is always true
• Guide refactoring (and make it easy to keep a working thing working after refactoring)
• Enforcing invariants about your program
• Inform your tools and IDE

The middle road

• Don’t judge by their worst face (typed and untyped languages)
• Don’t forget about their trade offs even if you love them
• Learn about them!

Q&A Session:

• Sum types and Algebraic Data Types are awesome, more languages should have them
• Modules are powerful in the SML family and
• GADTs are cool. Seems like it’d be really good for modeling ASTs or something, but are super good for systems programming and high performance things like modeling memory layout and whatnot.
• Get better at type-ful design. Using the type system to model and encode structure so that things are super easy to understand, communicate, and use. They’re easier to meta-reason about too (e.g. everywhere this library is used, this must be true)
• Lots of pain associated with the minority nature of OCaml. There’s just not a lot since not a lot of people use it.
• Use GADTs for refining something as layers of “ors” and “ands” that moves from “binary -> message -> udp packet -> nasdaq message” or something without any allocation or anything: purely types.
• Gradual typing is tricky to do well. Hard to put a different paradigm or discipline onto something, making it non-idiomatic, and whatnot. It’s big and complicated to design these things well.
• Type systems may “slow you down in the small and speed you up in the large”. Type systems can also help you move slower in the sense that you model, think, and work at a more correct level.
• You can use types to reduce the number of tests that need to run and focus on the best, most valuable testing that should be done. Type systems amplify the power of tests.