Skip to content

Instantly share code, notes, and snippets.

@JSuder-xx
Created February 7, 2021 16:35
Show Gist options
  • Save JSuder-xx/6af27af0027393c3cf2ecc334f17e935 to your computer and use it in GitHub Desktop.
Save JSuder-xx/6af27af0027393c3cf2ecc334f17e935 to your computer and use it in GitHub Desktop.
Peano numbers and linked lists verified in the type system (dependent typing) in TypeScript.
/**
* **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>
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment