Higher-kinded type

A higher-kinded type variable ranges over type constructors rather than over types^[2][6]. In fmap :: Functor f => (a -> b) -> f a -> f b, the variable f stands for Maybe, [], Either e or any other constructor of one argument, so one definition of Functor or Monad serves every container. Kinds, the types of types, keep this well formed: Int has kind Type and Maybe has kind Type -> Type. The underlying calculus is Girard's System Fω^[3]; Jones made it practical for type inference with constructor classes in 1993^[2], and Haskell adopted them in 1996. Scala added type constructor polymorphism in 2007^[4]. OCaml has no higher-kinded type variables, and expresses the same programs with functors over modules or with the brand encoding of Yallop and White^[1].

class Functor f where            -- f :: Type -> Type
  fmap :: (a -> b) -> f a -> f b
 
instance Functor Maybe where
  fmap _ Nothing  = Nothing
  fmap g (Just x) = Just (g x)
 
instance Functor (Either e) where   -- partial application: Either e :: Type -> Type
  fmap _ (Left e)  = Left e
  fmap g (Right x) = Right (g x)

The class variable f is applied to types in the method signature, f a and f b, so it cannot itself be a type; it is a function from types to types.

Kinds classify types the way types classify values^[6]. Every type that has values, such as Int, Maybe Int or Int -> Bool, has kind Type, written $\ast$ in older texts. A type constructor that needs one argument has kind $\ast \to \ast$, and constructors can take constructors as arguments:

import Control.Monad.State (StateT)
import Data.Functor.Compose (Compose)
import Data.Kind (Type)
 
newtype Fix f = Fix (f (Fix f))

Int :: Type
Maybe :: Type -> Type
Either String :: Type -> Type
Either :: Type -> Type -> Type
(->) :: Type -> Type -> Type
Fix :: (Type -> Type) -> Type
StateT :: Type -> (Type -> Type) -> Type -> Type
Compose :: (k -> Type) -> (k1 -> k) -> k1 -> Type
Functor :: (Type -> Type) -> Constraint
Monad :: (Type -> Type) -> Constraint

A type is higher-kinded when its kind has an arrow, and higher-order when an arrow appears to the left of another, as in Fix and the monad transformer StateT. Classes have kinds too, ending in Constraint rather than Type (see constraint kinds). Compose is kind-polymorphic: its kind contains kind variables, which GHC has supported since 2012^[7].

Kind checking rejects ill-formed types the way type checking rejects ill-formed terms.

instance Functor Int where
  fmap = undefined

kinderr.hs:1:18: error:
    * Expected kind `* -> *', but `Int' has kind `*'
    * In the first argument of `Functor', namely `Int'
      In the instance declaration for `Functor Int'
  |
1 | instance Functor Int where
  |                  ^^^

With a variable of kind $\ast \to \ast$, a function can be written once for every container that supports the operations it needs.

import qualified Data.Map as Map
import Data.Foldable (toList)
 
data Tree a = Leaf | Node (Tree a) a (Tree a)
 
instance Functor Tree where
  fmap _ Leaf = Leaf
  fmap g (Node l x r) = Node (fmap g l) (g x) (fmap g r)
 
instance Foldable Tree where
  foldr _ z Leaf = z
  foldr g z (Node l x r) = foldr g (g x (foldr g z r)) l
 
-- One definition, for every container t of kind Type -> Type.
summary :: (Foldable t, Functor t) => t Int -> (Int, [Int])
summary xs = (sum xs, toList (fmap (* 10) xs))
 
main :: IO ()
main = do
  print (summary [1, 2, 3])
  print (summary (Just 4))
  print (summary (Map.fromList [("a", 5), ("b", 6)]))
  print (summary (Node (Node Leaf 7 Leaf) 8 (Node Leaf 9 Leaf)))
  print (summary (Right 3 :: Either String Int))

(6,[10,20,30])
(4,[40])
(11,[50,60])
(24,[70,80,90])
(3,[30])

The same idea underlies Traversable, Foldable, the monad transformer library and the lens library, whose types quantify over functors. Without higher-kinded variables each of these would need a separate definition, or a separate class, for each container.

Higher-kinded data

A record can be parameterized by a type constructor that wraps each field. With Maybe it describes a partially filled form, with Identity a complete one, and with lists a set of candidates, all from one declaration.

{-# LANGUAGE StandaloneDeriving, FlexibleContexts, UndecidableInstances #-}
import Data.Functor.Identity (Identity (..))
 
-- A record parameterized by a type constructor: each field is wrapped in f.
data Person f = Person { name :: f String, age :: f Int }
 
deriving instance (Show (f String), Show (f Int)) => Show (Person f)
 
-- A form being filled in has optional fields; a finished one has plain ones.
validate :: Person Maybe -> Maybe (Person Identity)
validate (Person n a) = Person <$> fmap Identity n <*> fmap Identity a
 
main :: IO ()
main = do
  print (validate (Person (Just "Ada") (Just 36)))
  print (validate (Person (Just "Ada") Nothing))
  let defaults = Person ["anonymous"] [0, 18]  -- Person [] : several candidates
  print defaults

Just (Person {name = Identity "Ada", age = Identity 36})
Nothing
Person {name = ["anonymous"], age = [0,18]}

Type inference must solve equations like $fa=\mathtt{Maybe}\mathtt{Int}$. In general this is higher-order unification, which is undecidable^[8]: with type-level lambdas, $f$ could be $\lambda t.\mathtt{Maybe}\mathtt{Int}$ as well as Maybe. Jones's constructor classes avoid the problem by allowing only type constructors and their partial applications as values of higher-kinded variables, never lambdas^[2]. Constructors are injective and generative, so $fa=gb$ holds exactly when $f=g$ and $a=b$, and ordinary first-order unification suffices.

The cost is that only the last argument of a constructor can be abstracted: Either e is a functor in its right component, and the pair type (a, a) is not f a for any constructor f. Type synonyms cannot be partially applied, so a newtype must name the shape instead.

-- There are no type-level lambdas: to map over both halves of (a, a),
-- the shape needs a name of kind Type -> Type.
newtype Pair a = Pair (a, a) deriving Show
 
instance Functor Pair where
  fmap g (Pair (x, y)) = Pair (g x, g y)
 
-- Either e is a partial application in the last argument only; mapping
-- over the Left side also needs a newtype that flips the arguments.
newtype Flip p b a = Flip (p a b) deriving Show
 
instance Functor (Flip Either b) where
  fmap g (Flip (Left x)) = Flip (Left (g x))
  fmap _ (Flip (Right y)) = Flip (Right y)
 
main :: IO ()
main = do
  print (fmap (+ 1) (Pair (1, 2)))
  print (fmap (+ 1) (1, 2))
  print (fmap length (Flip (Left "error") :: Flip Either Int String))

Pair (2,3)
(1,3)
Flip (Left 5)

The built-in instance for pairs maps only the second component, which is why the second line differs from the first.

Scala supports higher-kinded type parameters, written F[_]^[4], and libraries such as Cats build the same class hierarchy on them. Java, C# and Go generics range over types only, so a Functor interface cannot mention the container type applied to a different element. Rust's generic associated types, stable since 2022, cover some of the same uses.

OCaml has higher-kinded types in its module language: a module signature can contain an abstract 'a t, and a functor over that signature is generic in the container.

(* OCaml type variables range over types only, so a function generic in
   the container is written as a functor over a module that supplies it. *)
module type FUNCTOR = sig
  type 'a t
  val map : ('a -> 'b) -> 'a t -> 'b t
  val to_list : 'a t -> 'a list
end
 
module Summary (F : FUNCTOR) = struct
  let summary (xs : int F.t) = (List.fold_left ( + ) 0 (F.to_list xs), F.to_list (F.map (( * ) 10) xs))
end
 
module L = Summary (struct type 'a t = 'a list let map = List.map let to_list l = l end)
module O = Summary (struct type 'a t = 'a option let map = Option.map let to_list = Option.to_list end)

(6, [10; 20; 30])
(4, [40])

This works, but every instantiation is an explicit module application. Yallop and White showed how to recover higher-kinded polymorphism in the core language by defunctionalization^[1]: an abstract brand type stands for each constructor, and ('a, 'f) app represents 'f applied to 'a. The version below uses an extensible variant, so that the projections are checked rather than unsafe casts.

(* Lightweight higher-kinded polymorphism: ('a, 'f) app stands for "'f
   applied to 'a", where 'f is an abstract brand naming a type constructor.
   Each constructor gets a brand and an injection and projection. *)
type ('a, 'f) app = ..
 
type list_br
type ('a, 'f) app += List : 'a list -> ('a, list_br) app
let prj_list : ('a, list_br) app -> 'a list = function List l -> l | _ -> assert false
 
type option_br
type ('a, 'f) app += Opt : 'a option -> ('a, option_br) app
let prj_opt : ('a, option_br) app -> 'a option = function Opt o -> o | _ -> assert false
 
(* A functor dictionary for any brand 'f: an ordinary value, with 'f an
   ordinary type variable. *)
type 'f functor_ = { map : 'a 'b. ('a -> 'b) -> ('a, 'f) app -> ('b, 'f) app }
 
let list_functor = { map = (fun g x -> List (List.map g (prj_list x))) }
let option_functor = { map = (fun g x -> Opt (Option.map g (prj_opt x))) }
 
(* Generic in the container: 'f is a type variable of "kind" * -> *. *)
let times_ten (f : 'f functor_) (xs : (int, 'f) app) = f.map (fun x -> x * 10) xs

[10; 20; 30]  Some 40

Girard's System Fω of 1972 quantifies over type operators of any kind, and is the calculus in which higher-kinded polymorphism is usually studied^[3][6]. Jones introduced constructor classes in 1993, with a restriction that keeps type inference decidable^[2]; Haskell 1.3 adopted them in 1996, making Functor and Monad classes over constructors, and Haskell 98 kept them^[5]. Scala added type constructor polymorphism in version 2.5 in 2007, described by Moors, Piessens and Odersky^[4]. GHC added kind polymorphism and promoted datatypes in 2012^[7]. Yallop and White's encoding for OCaml appeared in 2014^[1].

• FunctorIn functional programming, a functor is a type constructor f with an operation fmap : (a -> b) -> f a -> f b that applies a function inside the structure without changing its shape, preserving identity and composition. Lists, options, trees and functions out of a fixed type are functors. The notion comes from category theory. In OCaml the word also names parametrised modules such as Map.Make.
• MonadIn functional programming, a monad is a type constructor m with two operations, return : a -> m a and bind : m a -> (a -> m b) -> m b, satisfying three laws. It lets code with some extra behaviour, such as failure, several results, configuration, state or I/O, be written as a sequence of ordinary steps, with the behaviour defined once in bind. The notion comes from category theory.
• Constraint kindsConstraintKinds is the GHC extension that gives constraints their own kind, Constraint, so that the thing to the left of => becomes a first-class type-level entity that can be named with a synonym, passed as a parameter, returned by a type family, and stored in a data type. It lets a class leave to each instance what that instance needs of its element types, as when a container class requires Ord for sets and nothing for lists, and it lets dictionaries be packaged as ordinary values with Dict.
• LensA lens is a first-class pair of a getter and a setter for one part of a structure, with laws that make them agree: you get back what you set, setting what you got changes nothing, and a second set overwrites the first. Lenses compose, so a path through nested immutable records is one value that can read or update the part at its end. They originated in work on the view-update problem, and in Haskell are usually encoded as functions polymorphic in a functor, which makes composition ordinary function composition.
• TraversableTraversable is the abstraction of a container that can be rebuilt while an applicative effect is performed on each element in order: traverse : (a -> f b) -> t a -> f (t b). Validating every element, parsing each string, numbering the nodes of a tree and taking cartesian products are all traversals with different applicative functors. traverse subsumes both map (with the identity functor) and foldMap (with a constant functor into a monoid), and it satisfies laws saying it visits every element exactly once.
• Dictionary passingDictionary passing is the standard way to implement type classes. Each class becomes a record type whose fields are its methods, each instance becomes a value of that record type, and each function with a class constraint receives the record, the dictionary, as an extra argument, which the compiler supplies at every call site after resolving which instance applies. An instance that itself has a context, such as equality on lists given equality on elements, becomes a function from dictionaries to a dictionary, and a superclass becomes a field. The same technique written by hand is the usual way to get type-class-like overloading in OCaml, with records, first-class modules or functors.
• Dependent typeA dependent type is a type that may mention values, so that a vector's length can appear in its type and a function's result type can be computed from its arguments. Function types generalize to dependent products Π(x : A). B(x), and pairs to dependent sums Σ(x : A). B(x). Because types can express propositions and programs can be proofs, languages with dependent types, such as Agda, Coq (Rocq), Lean and Idris, double as proof assistants. The price is that type checking involves evaluating programs, so these languages require functions to terminate, and type equality is decided up to computation.
• Orphan instanceAn orphan instance is a type class instance declared in a module that defines neither the class nor the type. Because instance resolution is global but imports are not, two orphans for the same class and type can coexist in one program, and code compiled against different ones can disagree: a Set built under one ordering and searched under another silently loses elements. GHC warns about orphans, and Rust forbids them outright with its orphan rule. The usual fix is a newtype, which gives the instance a type of its own.
• Yoneda lemmaFor a functor F and an object a, natural transformations from Hom(a, -) to F correspond one to one with elements of F a. In Haskell, forall b. (a -> b) -> f b is isomorphic to f a, and the left-hand form turns a chain of fmaps into one composed function and a single fmap.

• Functional Programming in C++Sum types, monadic optional and expected, lazy range pipelines, folds, composition, and persistent structures, in C++23.
• Lenses and Prisms in OCamlAn optics library whose kinds are a phantom polymorphic variant, and a ppx that derives lenses from records, prisms from variants, and both from field paths and patterns.

1. [1]J. Yallop, L. White, “Lightweight higher-kinded polymorphism”, FLOPS (2014).
2. [2]M. P. Jones, “A system of constructor classes: overloading and implicit higher-order polymorphism”, FPCA (1993).
3. [3]J.-Y. Girard, Interprétation fonctionnelle et élimination des coupures de l’arithmétique d’ordre supérieur, thèse d’État, Université Paris 7 (1972).
4. [4]A. Moors, F. Piessens, M. Odersky, “Generics of a higher kind”, OOPSLA (2008).
5. [5]S. Peyton Jones (ed.), Haskell 98 Language and Libraries: The Revised Report, Cambridge University Press (2003).
6. [6]B. C. Pierce, Types and Programming Languages, ch. 29–30, MIT Press (2002).
7. [7]B. A. Yorgey, S. Weirich, J. Cretin, S. Peyton Jones, D. Vytiniotis, J. P. Magalhães, “Giving Haskell a promotion”, TLDI (2012).
8. [8]G. Huet, “The undecidability of unification in third order logic”, Information and Control 22 (1973).

last updated 29 September 2026