Created
February 7, 2021 16:35
-
-
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.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
/** | |
* **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