Last active
August 19, 2018 02:02
-
-
Save briancavalier/f8ffefc2432adfb9798ccaccf07820f3 to your computer and use it in GitHub Desktop.
Flow type-level naturals and addition
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| // @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]]] | |
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
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.