Peano numbers and linked lists verified in the type system (dependent typing) in TypeScript.

typescript_peano_and_list.ts

/**
 * **Power of Infer**
 * Infer allows us to match a type for a structure and unpack the internal structure of that type 
 * into local type variables. This is essentially destructuring/deconstructing/elimination.
 * 
 * The are two fundamental computation operations
 * * Building up or constructing types - which can be done with Mapped Types (comprehension).
 * * Unpacking types - which can be done with the combination of Conditional Types and the use of infer.
 * 
 * The examples below are the poster-child for this idea of computation through construction/deconstruction
 * * Natural Numbers through Peano
 * * Linked Lists 
 */
type ReadMe = {}

/**
 * The code below intentionally does not always use the most ideal abstraction in order to avoid the 
 * compiler error 
 * * "type instantiation is excessively deep and possibly infinite". 
 * 
 * The error is due to TypeScript limiting the recursion depth and also  
 * the fact that the compiler does not perform tail call optimization (which can eliminate recursion in generated code). 
 * Unfortunately, this means that there are limits to the application of computed types in TypeScript 
 * even though the type system Turing complete. However, with every release the team keeps hammering away at this limitation.
 */
type Limitations = {}

module PeanoNumbers {
    // Define the Peano number types: https://en.wikipedia.org/wiki/Peano_axioms
    type Zero = { kind: "Zero" }
    type Add1<innerNumber extends PeanoNumber> = { kind: "Add1", innerNumber: innerNumber }
    type PeanoNumber = Zero | Add1<any>
    // Peano operations
    type Sum<left extends PeanoNumber, right extends PeanoNumber> =
        right extends Zero
        ? left
        : right extends Add1<infer innerRight>
        ? { kind: "Add1", innerNumber: Sum<left, innerRight> }
        : never;
    type Multiply<left extends PeanoNumber, right extends PeanoNumber> =
        right extends Zero
        ? { kind: "Zero" }
        : right extends One
        ? left
        : right extends Add1<infer innerRight>
        ? Sum<left, Multiply<left, innerRight>>
        : never;

    // Some aliases
    type One = Add1<Zero>
    type Two = Add1<One>
    type Three = Add1<Two>
    type Four = Add1<Three>
    type Five = Add1<Four>
    type Six = Add1<Five>
    type Seven = Add1<Six>

    // Examples: Hover over the types to see the structure
    type TwoPlusFive = Sum<Two, Five>
    type ThreeMultipliedByFour = Multiply<Three, Four>
    type SevenMultipledByTwelve = Multiply<Seven, ThreeMultipliedByFour>
}

module LinkedLists {
    // Check it!!! We can use the exact same pattern for Linked Lists!!!
      
    // Nil is the Zero of lists.
    type Nil = { kind: "Nil" }
    // Cons is the Add1 of lists. Cons is the FP operation for creating a LL node.
    type Cons<value, innerList extends List> = { kind: "Cons", innerList: innerList, value: value }
    type List = Nil | Cons<any, any>;
    // Concat is the Sum operation on lists.
    type Concat<left extends List, right extends List> =
        right extends Nil
        ? left
        : right extends Cons<infer value, infer innerList>
        ? { kind: "Cons", value: value, innerList: Concat<left, innerList> }
        : never

    type Colors = Cons<"Red", Cons<"Green", Cons<"Blue", Nil>>>
    type Shapes = Cons<"Circle", Cons<"Triangle", Cons<"Square", Nil>>>

    // Hover over the type. Try declaring a local variable of the type and use intellisense to drill in.
    type ShapesAndColors = Concat<Shapes, Colors>
}