The hkt-toolbelt now provides a way to ‘reify’ a higher-order type into a concrete function type. This is useful for representation of point-free code.
to reify: make (something abstract) more concrete or real.
Basics of Higher-Order Types For the purposes of hkt-toolbelt, a higher-order type is merely a representation of a type mapping, i.e. an ‘applicable’ type that maps from an input type to an output type.
Higher-order types are useful because they can take in higher order types, or return higher order types.
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.
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))$.
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 ?
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.
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.6. HKT-Level Flow 3.7. HKT-level Split 3.
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.
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 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.3.3. References for this Section 2.
There are a few interesting questions about the nature of programs, and specifically about sets of programs, as represented by lambda calculus expressions.
1. How many programs have N terms? 2. How fast does the set of programs of length N grow? 3. How many programs of length N converge? 4. What is the longest-running convergent program of length N? 5. How fast does BB(N) grow? 6. What percentage of programs converge?