Enforce lists to be monotonic at compile time

type-level-monotonic.ts

// Adapted from http://blog.braulio.me/posts/2017-08-10-enforce-monotonic.html

//
// booleans
//

type Bool = 'T' | 'F'

type If<B extends Bool, Then, Else> = {
  T: Then
  F: Else
}[B]

//
// naturals
//

interface Zero {
  isZero: 'T'
  prev: never
}

interface Succ<N extends Nat> {
  isZero: 'F'
  prev: N
}

type Nat = Zero | Succ<any>

type One = Succ<Zero>
type Two = Succ<One>

type IsZero<N extends Nat> = N['isZero']

type Prev<N extends Nat> = N['prev']

//
// type-level functions
//

type Sum<N1 extends Nat, N2 extends Nat> = {
  T: N2
  F: Succ<Sum<Prev<N1>, N2>>
}[IsZero<N1>]

type Lte<N1 extends Nat, N2 extends Nat> = {
  T: 'T'
  F: If<IsZero<N2>, 'F', Lte<Prev<N1>, Prev<N2>>>
}[IsZero<N1>]

//
// hlists
//

interface HNil {
  isHNil: 'T'
  head: never
  tail: never
}

interface HCons<H, T extends HList> {
  isHNil: 'F'
  head: H
  tail: T
}

type HList = HNil | HCons<any, any>

type IsHNil<L extends HList> = L['isHNil']

type Head<L extends HList> = L['head']

type Tail<L extends HList> = L['tail']

//
// Increasing: given a type-level list of type-level nats
// evaluates to the type 'T' if the nats are monotonically increasing
//

type And<B1 extends Bool, B2 extends Bool> = If<B1, B2, 'F'>

type Increasing<L extends HList> = {
  T: 'T'
  F: If<IsHNil<Tail<L>>, 'T', And<Lte<Head<L>, Head<Tail<L>>>, Increasing<Tail<L>>>>
}[IsHNil<L>]

// [0, 1, 2] is ok
const success: Increasing<HCons<Zero, HCons<One, HCons<Two, HNil>>>> = 'T'

// [0, 1, 0] is not
const failure: Increasing<HCons<Zero, HCons<One, HCons<Zero, HNil>>>> = 'F'