Skip to content

Instantly share code, notes, and snippets.

@briancavalier briancavalier/type-nat.js
Last active Aug 19, 2018

Embed
What would you like to do?
Flow type-level naturals and addition
// @flow
// Type-level naturals
type Zero = 0
interface Succ {
<N>(N): [1, N]
}
// Hey look, we can do type-level pattern matching
// with function-variant interfaces
interface Pred {
(Zero): Zero,
<N>([1, N]): N
}
// Now we can get crazy and implement addition
interface Add {
<N>(Zero, N): N,
<N>(N, Zero): N,
<N, M>(N, [1, M]): $Call<Add, [1, N], M>
}
type One = $Call<Succ, Zero>
type Two = $Call<Succ, One>
type Three = $Call<Add, One, Two>
type TwoMinus1 = $Call<Pred, Two>
type OneMinus1 = $Call<Pred, TwoMinus1>
// Let's construct some values to prove these types
let one: One = [1, 0]
let oneAlso: TwoMinus1 = one
let zeroAlso: OneMinus1 = 0
let three: Three = [1, [1, [1, 0]]]
@frontsideair

This comment has been minimized.

Copy link

commented Apr 10, 2018

For some reason, $Call<Add, One, Two> accepts anything other than Zero. I tried to fiddle with it but couldn't fix it. See a repro. If you replace one of the operands with Zero it fails as expected though.

Of course it's not a bug report, just an observation.

@briancavalier

This comment has been minimized.

Copy link
Owner Author

commented Apr 16, 2018

Yeah, I'm sure this is pushing flow's limits. I've run into several other situations, especially around $Call and union types, where inference breaks down, and flow starts accepting things it shouldn't.

@frontsideair

This comment has been minimized.

Copy link

commented Apr 16, 2018

Since it's not Flow's intended purpose, I'm almost sure it would get a wontfix if submitted as an issue. I'm considering getting in the codebase and sending fixes, but I'm not sure if it can be done since these kinds of errors don't really give confidence.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.