Skip to content

Instantly share code, notes, and snippets.

@joaomilho
Created Nov 3, 2020
Embed
What would you like to do?
Fully typed arithmetics with TypeScript 😨
type Nat = ["S", Nat] | ["Z"];
type Succ<N extends Nat> = ["S", N]
type S<N extends Nat> = Succ<N>
type Prev<N extends Nat> = N[1]
type Z = ["Z"]
type Zero = Z
type One = S<Z>
type Two = S<S<Z>>
type Three = S<S<S<Z>>>
type Four = S<S<S<S<Z>>>>
type Five = S<S<S<S<S<Z>>>>>
type Six = S<S<S<S<S<S<Z>>>>>>
type Seven = S<S<S<S<S<S<S<Z>>>>>>>
type Eight = S<S<S<S<S<S<S<S<Z>>>>>>>>
type Nine = S<S<S<S<S<S<S<S<S<Z>>>>>>>>>
type Ten = S<S<S<S<S<S<S<S<S<S<Z>>>>>>>>>>
type IsZero<N extends Nat> =
N extends Zero ? true : false
type Concat<X extends Nat, Y extends Nat> =
X extends Zero ? Y :
["S", Concat<X[1], Y>];
type Prod<X extends Nat, Y extends Nat> =
X extends Zero ? Zero :
Concat<Y, Prod<X[1], Y>>;
type Power<Base extends Nat, Exp extends Nat> =
Exp extends Zero ? One :
Prod<Base, Power<Base, Exp[1]>>;
type ToS<N extends Nat> =
N extends Zero ? 'Z' :
`S${ToS<N[1]>}`;
type ToDots<N extends Nat> =
N extends Zero ? '' :
`.${ToDots<N[1]>}`;
type LTE<X extends Nat, Y extends Nat> =
X extends Zero ? true :
Y extends Zero ? false :
LTE<X[1], Y[1]>
type LT<X extends Nat, Y extends Nat> = LTE<["S", X], Y>
type GTE<X extends Nat, Y extends Nat> = LTE<Y, X>
type GT<X extends Nat, Y extends Nat> = LT<Y, X>
type Eq<X extends Nat, Y extends Nat> =
X extends Zero ? IsZero<Y> :
Y extends Zero ? false :
Eq<X[1], Y[1]>
type Fib<X extends Nat> =
X extends Zero ? Zero :
X extends One ? One :
Concat<Fib<X[1]>, Fib<X[1][1]>>
type Fac<X extends Nat> =
X extends Zero ? One :
Prod<X, Fac<X[1]>>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment