Customizing universal serialization or ordering via explicit View and Quotient types

[pchiusano]

Not sure what I think of this idea but just writing it up. The general idea is to have a couple special types that Unison knows about which allow the programmer to selectively override and/or control how universal functions like == or < work, on a per-value basis.

Data types often have auxiliary information which isn't really part of the identity of the value but which is kept around to make certain access patterns more efficient. For instance, a Relation a b is conceptually a Set (a,b) but might be represented as a pair of maps (a Map a [b] and a Map b [a]). If you're comparing two Relation values for equality you don't need to compare both maps, only one (the other contains the same info, just indexed differently).

What programmers usually do in this situation is manually write a custom Eq instance for the type that directs the equality check to the non-redundant portion of the value. An alternate approach: still do things automatically, but have the programmer annotate which portions of the value are redundant. We can do that with a simple data type which I'll call View. Using pseudo-Haskell syntax here:

unique type View a v = View a 'v (a -> v)

instance Eq a => Eq (View a v) where
  View a _ _ == View a2 _ _ = a == a2

view : a -> (a -> v) -> View a v
view a f = View a (lazy '(f a)) f

lazy : 'a -> 'a -- builtin which memoizes a pure thunk

unique type Relation a b = Relation (View (Map a [b]) (Map b [a]))

The idea is that Unison's universal == would compare View a v values in terms of the a, not the v. Likewise for < and so on: to serialize a View a v f, you serialize (a, f), and then when deserializing, regenerate v by calling f a.

That covers a number of situations, but what if you wanted a text type that did case insensitive comparisons? In this case, there's a derived view (the result of calling toLower on the underlying Text), and you want comparisons to happen based on that derived view, rather than in terms of the original value. We could have another type for this:

unique type Quotient a v = Quotient a 'v (a -> v)

quotient : a -> (a -> v) -> Quotient a v
quotient a f = Quotient a (lazy '(f a)) f

instance Eq v => Quotient a v where 
  Quotient _ v _ == Quotient _ v2 _ = !v == !v2

unique type CaseInsensitiveText = CaseInsensitiveText (Quotient Text Text)

caseInsensitive : Text -> CaseInsensitiveText
caseInsensitive txt = CaseInsensitive (quotient txt Text.toLower)

Again this Quotient type would be used by the universal functions like ==.

I think what this idea has going for it is it's easy to implement and doesn't require a more general mechanism like typeclasses. And even with typeclasses, View and Quotient types could be useful - they better declare the intent of the type and automate away some boilerplate you'd otherwise write in a manual Eq or Ord instance.

I could also imagine more types of this sort, supporting different kinds of customization (like perhaps just customizing serialization), though I admit it's rather ad hoc and might become painful to use, like if you want to override ordering and hashing but not serialization, or something.