Show HN: Checking the Collatz conjecture using only TypeScript's type system

Show HN: Checking the Collatz conjecture using only TypeScript's type system(ostro.ws)

4 points by robbieo 6 years ago | 4 comments

SilasX 6 years ago |

Interesting! Two questions:

1) Could you maybe simplify the computational effort by defining "divide by 2" instead of general division, since you only ever divide by 2 for Collatz?

2) The author concludes by explicitly checking each integer. Given the power of types, isn't there a single statement you can make that would prompt it to check all integers, i.e. seeing if it can prove that all integers type-check?

robbieo 6 years ago | |

1) sure, but I figured I might as well implement all 4 operations for posterity. The `divideBy2` type would be not-that-dissimilar from the Even type. 2) Ha, if only! If that were true then we could prove all sorts of number-theoretic things by rewriting them in "types." Part of the point of this post is there is no magical power of types; they're just another programming language.

SilasX 6 years ago | | |

Thanks for replying!

2) I didn't mean it would guarantee a proof, I just meant it would attempt a proof up to the limit of its type checker's ability to prove type validity.