type system

Type-level Collatz Sequence

The Collatz conjecture is an unsolved problem in mathematics. It states that for any positive integer n, the sequence of numbers generated by the following algorithm will eventually reach 1. These are also called the hailstone numbers. function collatz(n: number): number { return n % 2 === 0 ? n / 2 : 3 * n + 1; } The sequence generated by a given $n$ is the sequence of numbers n, collatz(n), collatz(collatz(n)), collatz(collatz(collatz(n))), and so on.

Typesafe Function Composition

Do ya wanna know how to type function composition in Typescript? Read on! 1. Background 1.1. Type-theoretic Pseudocode 2. Typescript 2.1. IsComposablePair 2.1.1. Type-based Pattern Matching using infer 2.1.2. IsComposablePair 2.2. Every 2.3. Pair 3. Component Synthesis 4. Function Integration 5. Future Work: Constructive Approach 1. Background Function composition is an operation that takes two functions, $f$ and $g$, and produces a new function $h$ such that $h(x) = g(f(x))$.

Towards a well-typed plugin architecture

declare abstract class EnginePlugin<I = unknown, D = unknown> { createInterface?(ø: Record<string, unknown>): I getDependencies?(): D } type Defined<T> = T extends undefined ? never : T type ExtractPlugins<T> = T extends Engine<infer PX> ? PX : never type UnionToIntersection<U> = ( U extends unknown ? (k: U) => void : never ) extends (k: infer I) => void ? I : never type MergeInterfaces< E extends Engine, K extends keyof EnginePlugin, > = UnionToIntersection<ReturnType<Defined<ExtractPlugins<E>[number][K]>>> type Assume<T, U> = T extends U ?

A non-recursive type-level inclusion operator

type E1<X> = <T>() => T extends X ? 0 : 1 type E2<X> = <T>() => T extends X ? 0 : 1 type IsEqual<X, Y> = E1<X> extends E2<Y> ? true : false /** * Whether or not T includes U as an element. */ type Includes<T extends readonly unknown[], U> = true extends { [key in keyof T]: IsEqual<T[key], U> }[number] ? true : false A non-recursive type-level Includes operator in Typescript Introduction Includes is a type-level operator that determines whether a given type T includes a given type U as an element.

Point-free Programming via HKTs

In Typescript, point-free programming has been traditionally limited due to the difficulty the type system has representing the abstracted types associated with point-free (also called ’tacit’) programming. 1. What is Tacit Programming? 2. Type-Level Programming 2.1. The Hard (Naive) Way 2.2. Tacit Logic via HKTs 3. Addendum: Library 3.1. Basic HKT Abstractions 3.2. HKT Composition 3.3. Narrow Type Inference 3.4. Value-level Apply 3.5. Auto-applyable HKTs 3.

Variadic HKT Composition

In a previous article, Higher Kinded Types in Typescript, we explored how to encode HKTs, as well as some of their applications. For example, we could define a value and type-level operation like the following: // "hello! hello!" const result = map(double, map(append("! "), "hello")); On both the type and value levels, the given string goes through a complex operation. In the end though, the type system can still capture and encode the operations being performed.

Higher Kinded Types in Typescript

HKTs are a powerful abstraction. Just as there are different types of higher-order functions, so are there so-called ‘higher-kinded types’. Taxonomy This blog post concerns one particular type of HKT - to define the taxonomy, first we will cover a few types, and a way they can be categorized. We can classify types in terms of ‘order’, a rough level of abstraction. Here are a few zero-order types that exist:

Type Guard Composition

Type guards are a powerful tool for type system design. They are used to express that a type is only valid if it satisfies a certain condition. For example, we can express that a type is only valid if it is a number or a string. 1. Union Type Guards 1.1. Naive Union Implementation 1.2. 2-adic Union Composition 1.3. N-adic Union Composition 1.3.1. GuardReturnType 1.3.2. Variadic Is-Union 1.

Unchained Tuple Types

The asserts syntax introduced with TS 3.7 allows us to interleave mutative runtime code with type annotations to express type mutations in a powerful way. This allows us to do away with the chaining syntax as described in my earlier article, Chained Tuple Types, and express our Set mutations in a much more familiar iterative way: const set: Set = new Set(); set.insert(2); set.insert(4); set.insert(8); set.remove(4); const hasResult1 = set.

Chained Tuple Types

With Typescript 4.1, it’s now possible to use variadic tuple types to construct large types with what appears to be runtime code. The general idea is that we will utilize a chaining pattern, where each operation on the chain returns an expanded version of the chain’s type. To motivate the example, let us consider a Set class. Our Set is a chaining class, where you may insert, remove, and check for the existence of numbers.