Types, and Why You Should Care

Types, and Why You Should Care - Yaron Minsky

  • Left: typed, Right: dynamicly typed
  • Performance

  • Typed Langs are faster
  • They give info for humans to understand.
    • Human Centered Computing

How Types Systems Hurt

  • Java is verbose :(
  • It slows you down. I can hack things together in Python but is slow to get done in Java

How Types Help!

  • In Python d2.get(key) gives you none. This is a logic error. You wrote something wrong.

  • In OCaml, this is now a type error! The compiler expected type: 'a option instead of Python's d2.get(key) which could have been none.

  • We can now handle all cases with pattern matching. If you miss an edge case, the compiler will tell you!

  • Strong Types:
    • Catch Errors: Less debugging! Many types of errors can be caught with a strong type system.
    • Have Less Surprises: Your thinking match what the code actually does. Types guide your thinking and let the compilers check the code matches your thinking!
    • Making Changes Doesn't Add New Bugs: Places where your code will affect and needs to be changed will be a type error!
  • "It feels like all the bugs go away! A lot of the bugs you spend a lot of time on feel like it vanishes in a puff of smoke."

Good Features in Type Systems

  • Type Inference:
  • Algebraic Data Types:
    • Product Type:
      • Structs, Record
      • This item AND this item AND this item
    • Sum Type:
      • Not common!
      • This item OR this item OR this item
      • Helps check you are handling all edge cases!
  • Garbage Collection:
    • In LISP 1950
    • Java 1990! 40 years.
    • Imagine Algebraic Data Types in 2060!

Product Types:

In C:

typedef struct {
   int    account_number;
   char   *first_name;
   char   *last_name;
   float  balance;
} account;

in F#:

type Contact = {
    Name: PersonalName 
    PrimaryContactInfo: ContactInfo
    SecondaryContactInfo: ContactInfo option

Sum Types: @TODO

More Advance

  • First Class Module
    • pass it around a function, store in a data structure
    • Generalized Algebraic Datatypes (GADT)
      • GADT of TCP of NASDAQ_message of add_order_message
      • TCP | UDP
      • Layers of OR and ANDS
      • GADT lets you do this without allocation

Adapting OCaml

  • Tooling isn't hot. You have to invest a lot into it.
    • Documentation
    • IDE features: Go to definition, auto-completion
  • We're not going to move fast and break things, we're
    • They have a focus on quality control - at their scale of money
  • Went from VBA/Excel to Java to OCaml

on F#

  • It's a car crash. Mixes Dotnet and OCaml
    • Adds complexity
    • OCaml is simple!

Gradual Typing

  • Making a language that does both is hard
  • Gradual Python, Typescript, Php to Hack
  • Can be unsound, it's not always right
  • Idiom of lipstick on a pig

On Testing

  • Types are good, testing is important too.
    • Many things tested manually will be caught for you by the type system.
    • It "snaps into place" testing a few examples encapsulate all the behavior