Refinement Types Lightning Talk

Duration: 5 minutes or 15 minutes
Slides: https://github.com/hasparus/refinement-types-in-typescript
Follow-up post: https://haspar.us/refinement-types/
Original notes: Dropbox Paper

Pitch

I’m gonna explain what refinement types are, geek out about a research paper that adds them to the TypeScript type system, and live-code a userland refinement type you can already use in your codebase.

What, Why, and How

How?

Lightning talk with VSCode, Quokka and browser as software.

What?

Refinement types are easy. Use them to encode more info on the type level.

Why?

Encoding information on the type level helps you write less bugs.

Outline

• Why and when should I type stronger?
  • JS without JSDoc vs Idris proofs
  • Refinement types are one step further into bulletproof programs.
• Refined TypeScript
• It’s not rocket science
• You can do it yourself
  • Live demo
• Libraries with refinements

I gave an extended (15 min) version of this talk at Kraków TypeScript User Group #5. The slides are on the are on the extended-15-minutes branch.

You can find the video here. The quality is pretty bad, though.