Presence polymorphism

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 :…