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.
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:
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?