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.
Plan
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
Hi I’m Piotrek and I’m gonna talk about refinement types.
As you all know, you can spend varying amounts of time coding one feature.
You can quickly prototype it in JavaScript or Python. Imagine that you’re sitting on a train and you pitch your services to a client in 1 hour. No types. No unit tests. It’s a proof of concept and you need to deploy ASAP.
After your successful pitch, you will want more control. You will consider moving towards the other end of the spectrum. Maybe you’ll even write it in Idris and prove it on a type-level. If it compiles, you’re certain your code does exactly what you want it to do.
You can use refinement types to move one stop towards this certainty and encode more information on the type-level for your compiler and your colleagues.
What are they, though?
Well, there’s a cool paper about them and an implementation for TypeScript
but our time is running so we’ll make do with a Wikipedia definition.
A type with a predicate. Damn, that’s easy! Let me try that.(write live)
and since we already know about nominal types and, as I’m aware, a lot of us are not big fans of classes:
How
What
Why
Plan
import { Brand } from 'nom-ts';import { Option, some, none } from 'fp-ts/lib/Option';
type Even = Brand<number, 'Even'>;const isEven = (x: unknown): x is Even => typeof x === 'number' && x % 2 === 0;const makeEven = (x: number): Option<Even> => isEven(x) ? some<Even>(x) : none;const Even = (x: number) => {