Lightweight higher-kinded polymorphism

Jeremy Yallop and Leo White, University of Cambridge. FLOPS 2014 — 12th International Symposium on Functional and Logic Programming, Kanazawa, Japan, 4–6 June 2014; LNCS 8475, Springer, pp. 119–135 (doi 10.1007/978-3-319-07151-0_8). 17 pages. Read from the authors’ PDF; the text below is extracted from the paper itself.

T1 — peer-reviewed primary research, and the corpus’s second scholarly source after cpp-hopl. It is also the first source here written to define a mechanism rather than to describe or sell a language.

The problem

The abstract states it. Higher-kinded polymorphism, meaning “abstraction over type constructors”, is “an essential component of many functional programming techniques such as monads, folds, and embedded DSLs.” haskell has it in the core language. ML-family languages, ocaml included, give every type variable kind *, so abstracting a type constructor means reaching for the module system and a functor. The paper’s complaint is ergonomic and specific: “the separation between the core language and the module language leads to awkwardness as functors proliferate.”

The worked example is when b m = if b then m else return (), which in Haskell has type ∀ (m :: * → *). Monad m ⇒ Bool → m () → m (), and in OCaml has to become a functor before it can be written at all.

The technique

Two pieces, both ordinary types:

• An abstract type app representing type application, so 'a list can be written as ('a, List.t) app.
• An opaque, uninhabited brand (List.t above), standing for the constructor list as something a type variable can range over.

Each brand ships inj and prj to move between the concrete type and its encoded form. Type constructors become “uninhabited members of the base kind *”, which is what lets a *-only type system talk about them. The general name for the move is type defunctionalization: a higher-order construct is replaced by a first-order tag plus an apply operation.

The cost the authors state themselves

Worth quoting because library documentation that adopts the technique tends not to: “The obvious disadvantage to the lack of a kind system is that the type checker is no help in preventing the formation of ill-kinded expressions, such as (List.t, List.t) app.” They immediately bound it — this “cannot lead to runtime errors”, since no ill-typed value can be formed by it — while elsewhere noting failures in prj as a real case.

So the encoding buys expressiveness and gives up kind checking. Nothing checks that a brand is used where a brand belongs, and the mistakes surface as type errors phrased in terms of the encoding rather than the program.

Why a 2014 OCaml paper sits in this wiki

Because it is the mechanism under fp-ts, which names this paper as its basis, and therefore under most attempts at Haskell-style abstraction in typescript. Two languages a decade apart, with unrelated designs and unrelated communities, hit the same wall (no abstraction over type constructors) and reached for the same workaround. That is a stronger claim about the wall than either library could make on its own.

It also gives the spoke something it has been short of: an account of a language limitation written by people with no product to sell, stating what their fix does not do.

Related

fp-ts · ocaml · haskell · typescript · type-system · functional-programming · effect · synthesis