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.
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?
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.has(8); // :: true const hasResult2 = set.
The string deduplication problem is a canonical one within computer science, serving a similar purpose as fizz-buzz in terms of being an example of a simple problem that a reasonably knowledgable practitioner should be able to solve with minimal effort.
The problem appears in a few variants, but briefly one such variant is to remove duplicate letters in a given string, such that the string then has only one instance of any given letter.
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.
Some “easy to state” problems in Typescript can require somewhat sophisticated type constructs.
Let’s say you want to enforce that every function in a particular map takes in as its first parameter, either a number or a string:
type PermissibleInput = number | string; const myFunctionMap = { foobar(x: number): void; barfoo(y: string): void; } If you do this in the naive way, as e.g. Record<string, (number | string) => any>, you will discover that this type actually encodes the requirements that every function must support both input types - which is a problem, as myFunctionMap is not actually composed of such functions.