Intersection of row types

records
rows
row-typing
type-system

#1

Hi all,

For a library I’m working on, I’m trying to create two operators on records. Given two records, r1 .|. r2 should return a record with the union of all fields, and r1 .&. r2 should return a record with the intersection of them (left biased). For example:

r1 :: {age :: Int}
r1 = {age: 30}

r2 :: {name :: String}
r2 = {name: "John"}

r3 :: {name :: String, town :: String}
r3 = {name: "Peter", town: "Amsterdam"}

r4 = r1 .|. r2 -- ==> {name: "John", age 30} :: {name :: String, age :: Int}
r5 = r2 .|. r3 -- ==> Type error! Both r2 and r3 contain the field (name :: String).

r6 = r1 .&. r2 -- ==> {} :: {}
r7 = r2 .&. r3 -- ==> {name: "John"} :: {name :: String}

Using disjointUnion from the record library, creating <&> is doable. However, I’m struggling with the intersection. Does anybody know if such a thing is even possible?

Below the code I have till now:

module Rows where

import Prelude

import Prim.Row (class Nub, class Union)
import Record (disjointUnion)


-- Union --

class (Union a b c, Nub c c) <= DisjointUnion a b c
instance disjointUnion  :: (Union a b c, Nub c c) => DisjointUnion a b c

infixl 5 or as .|.
or :: forall a b c. DisjointUnion a b c => Record a -> Record b -> Record c
or r1 r2 = disjointUnion r1 r2


-- Intersection --

class Intersection (a :: # Type) (b :: # Type) (c :: # Type)
-- ?how_to_make_an_instance

infixl 4 and as .&.
and :: forall a b c. Intersection a b c => Record a -> Record b -> Record c
and r1 r2 = ?how_to_do_this

#2

I think the trick is to go via RowList. You might want to take a look at @justinw’s record-diff, which includes a RowListIntersection class:


#3

Thanks Harry, I’ll take a look!

How difficult would it be to build an Intersection class into the compiler, as with Union and Nub?


#4

It’s probably not too hard to implement, but I’d prefer not to. I think we ought to start getting more conservative about adding new compiler-solved classes, especially if what they achieve is already possible in userland. I think all the same reasons for not having Prelude built in to the language apply: in particular, after a new compiler-solved class has been added, we can’t change it without it being a breaking change to the language.


#5

Yeah, you’re totally right. I hope PureScript will be so polished that most of these things can be done in userland.

I’m going to play around with the row list code, hope it will work out!


#6

Wonderful! The way through RowLists works like a charm!

About compiler solved classes and sliming those down: couldn’t Prim.Union and friends be implemented by using RowList in the same way instead of supplying Prim.Row.Union?


#7

The ones that are built in right now exhibit much better inference and performance. RowList is a compile-time performance drain, while Union and friends are implemented in Haskell. It’s essentially the difference of the type-checker interpreting a program vs it being native code.


#8

Yes, I know. The question is however: where to draw the line between

  • built in type classes with better inference and performance; and
  • define type classes in user space because PureScript is powerful enough.

#9

The answer is to implement it in PureScript if it’s possible, and if after using it for a while – and there’s demand – propose a new compiler solved class. For example, we originally implemented Lacks in terms of several Union constraints, and it was pretty terrible in practice. Lacks is frequently needed and the original implementation led to enough confusion that we added compiler support.


#10

Sounds awfully reasonable :slight_smile: