Refinement Types Lightning Talk

Sep 25, 2019 · WrocTypeScriptKraków TUG

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


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


Lightning talk with VSCode, Quokka and browser as software.


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


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


  • 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.

Edited 2 times
  1. 49a3e89Sep 14, 2020More work on brain-style notes
  2. 5b51651Sep 13, 2020Initial work on Brain-style notes