Refinements with Flow

gcanti
gcanti
Aug 5, 2016 · 2 min read

A refinement type is a type endowed with a predicate which must hold for all instances of the refined type

For example the type Integer can be defined as the pair

Integer = ( number, (n) => n % 1 === 0 )

where number is the refined type and (n) => n % 1 === 0 is the predicate.

This is a proof of concept, the goal here is to implement refinements without boxing values.

The idea

A refinement has the following blueprint (where A is the refined type)

// myrefinement.js
  • calling the function refinement should be the only legal way to get an instance of R
  • the class IsR must not be exported. If the constructor is not exported then users of the library that defined R can’t accidentally build a value v of type R (unless they voluntarily do an unsafe cast with ((v: any): R) which should be avoided)
  • collisions between two refinements of the same refined type A are not possible because of their corresponding nominal IsR types

A first example, integers

// integer.js

Let’s see how you can use the integer.js module

import type { Integer } from './integer.js'
import { integer } from './integer.js'

So an Integer is a number but a number is not an Integer. Nice.

Polymorphic refinements

The refined type A can be polymorfic (e.g. Array<*>).

Let’s define a refinement which represents a non empty array

// nonEmptyArray.js

Usage

import type { NonEmptyArray } from './nonEmptyArray.js'
import { nonEmptyArray } from './nonEmptyArray.js'

Drawbacks

Every refinement type is also an Object

function foo(x: Object) { ... }

Welcome to a place where words matter. On Medium, smart voices and original ideas take center stage - with no ads in sight. Watch

Follow all the topics you care about, and we’ll deliver the best stories for you to your homepage and inbox. Explore

Get unlimited access to the best stories on Medium — and support writers while you’re at it. Just $5/month. Upgrade

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store