haspar.us

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

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.


Edited 6 times
  1. 27dd30bMar 06, 2020Link video of my refinement types talk
  2. 2422f6aFeb 27, 2020Get rid of "pl-PL/" from meetup links
  3. c958448Feb 17, 2020Link to extended-15-minutes branch
  4. 7e2cac2Feb 14, 2020Add KTUG#5 to refinement-types.mdx
  5. 09d182eJan 28, 2020Add what,why,how and new pitch for KTUG#5
  6. 793358dDec 27, 2019Move talks/* to speaking/