Presence polymorphism

September 26, 2026 - Tagged as: en, plt.

I’ve been blogging about row polymorphism since 2013 (a life wasted?) but I only learned about presence polymorphism, which is a very related concept, recently.

For types with labels like records and variants, row polymorphism allows adding more labels, presence polymorphism allows removing labels.

Similar to row type variables, presence type variables have their own kinds. In this post we’ll use p prefixed type variables for presence variables, r prefixed types variables for row variables.

There are only two concrete presence types: Present and Absent. As the names suggest, Present makes a label present in the value, and Absent makes it absent.

With presence polymorphism, type of a record literal like

rec1 = (x = 123, msg = "hi", y = 456)
rec1 : (x : Int, msg : String, y : Int)

gets generalized as

rec1 : ∀ p1 p2 p3 . ((x : Int)^p1, (msg : String)^p2, (y : Int)^p3)

Instantiations of this type then give us subsets of the original record’s labels:

rec1 @Present @Present @Present : (x : Int, msg : String, y : Int)
rec1 @Present @Present @Absent  : (x : Int, msg : String)
rec1 @Present @Absent  @Absent  : (x : Int)
...

This is useful for the same reason that variant literals having row polymorphic type is useful:

var1 = ~Option.Some(123)
var1 : ∀ r1 . [Option[Int], ..r1]

Similar to how a variant value with the label for the named type Option[Int] can be passed as a variant with type [Option[Int], String], a record with labels (x : Int, msg : String) can be used as a single-label record (a : Int) or (msg : String), or an empty record ().

In other words, a simple and limited version of subtyping of variants can be implemented using row polymorphism, and subtyping of records can be implemented using presence polymorphism.

In contravariant (i.e. function argument) positions, the polymorphisms used for variants and records get swapped: records become row polymorphic and variants become presence polymorphic:

f1 = \(r) -> r.x + r.y
f2 = \(v) -> match v with
               ~Option.Some(x) -> x
               ~Option.None    -> 0
               ~msg as String  -> panic("Unexpected argument: `msg`")

f1 : ∀ r1    . (x : Int, y : Int, ..r1)    -> Int
f2 : ∀ p1 p2 . [Option[Int]^p1, String^p2] -> Int

In practice though, presence polymorphism is a bit difficult to deal with, because of type parameters growing proportionally with the labels in the types.

So instead, we make variants in covariant position and records in contravariant position row polymorphic, and that often works well enough. Consider the types of functions, and the record and variant above, with just row polymorphism, just presence polymorphism, and both:

-- With just row polymorphism
var1 : ∀ r1 . [Option[Int], ..r1]
rec1 :        (x : Int, msg : String, y : Int)

f1 : ∀ r1 . (x : Int, y : Int, ..r1) -> Int
f2 :        [Option[Int], String]    -> Int

-- With just presence polymorphism
var1 :              [Option[Int]]
rec1 : ∀ p1 p2 p3 . ((x : Int)^p1, (msg : String)^p2, (y : Int)^p3)

f1 :           (x : Int, y : Int)          -> Int
f2 : ∀ p1 p2 . [Option[Int]^p1, String^p2] -> Int

-- With presence and row polymorphism
var1 : ∀ r1       . [Option[Int], ..r1]
rec1 : ∀ p1 p2 p3 . ((x : Int)^p1, (msg : String)^p2, (y : Int)^p3)

f1 : ∀ r1    . (x : Int, y : Int, ..r1)    -> Int
f2 : ∀ p1 p2 . [Option[Int]^p1, String^p2] -> Int

In all of these cases, f1 rec1 and f2 var1 are well typed, giving us a limited subtyping-like type checking where a larger record can be passed as a smaller one, and a smaller variant can be passed as a larger one. (aka. width subtyping)

A function having a row or presence polymorphic parameter and a value being row or presence polymorphic are not the same things: in the function, the polymorphic argument will have a rigid type¹, just with type variables, but the polymorphic value can be used as different concrete types. So there’s still value in making records in covariant position polymorphic.

However my guess is, because of how unwieldy the type parameters get with larger records, presence polymorphism didn’t get as much attention as row polymorphism, and I hadn’t heard of it until recently.

---

1. Unless we support higher-ranked types, which come with their own set of problems.↩︎