F# and LVars

Read Time: 8 minutes

Today I want to spend some time with join-semilattices, specifically my F# implementation, LVar. It is a conceptually interesting data structure and approach to managing information, as well as improving program correctness.

What is a join-semilattice? For purposes of this conversation, you can think of it as a structure that has specific properties regarding data and increasing information. It is worth expanding on two prominent properties. One, it is a partially ordered set. Two, it is associative, communicative, and idempotent when combined with other join-semilattices. Why does this matter? Because these properties provide interesting capabilities that can be used to manage a variable’s information in a unique way. A join-semilattice can provide guarentees as a developer encodes not just datatype, but intent of a variable. From a practical sense it means we can build variables that only “grow” their information in a predefined manner. Using these types of variables can ensure a higher level of correct intention for an application.

At this point some examples are useful. Think of a variable that only ever increases (hit count, game high score, etc), from an intuitive approach the value always goes up, but typically languages don’t limit interactions with a variable to that constraint type. In contrast, a hit counter or high score tracker using an LVar only increases, by definition. When the LVar’s value is set, it will only accept a new value that is greater than or equal to its existing value. As another example, consider a data structure that tracks team members voting on a ballot. Once a person votes, they will always maintain a vote, it shouldn’t randomly disappear in the future due to a coding or data synchronization error. Using an LVar set or hashmap only permits the internal values to improve in information through inserts and updates (remove is forbidden). When merging the set or hashmap, keys are not lost, and the values only improve.

The original inspiration for this post and package came from Lindsey Kuper’s LVar work. If you want more technical explanations, the papers I most used for reference material are worth a read. The first being LVars: Lattice-based Data Structures for Deterministic Parallelism. The second is the Bloom Lattice variables paper, Logic and Lattices for Distributed Programming. These aren’t the only places lattice variables discussed, but these drove most of my journey. It is also worth mentioning at this point, my goal is not to implement their definitions verbatim; my LVars package is more of an inspired-by, focusing on the factors that are important to my current needs.

LVars provide interesting characteristics, but as is often the case, these benefits come some restrictions and tradeoffs. Only some types of data can be properly represented with lattices. For instance, lists and arrays do not meet the requirements of being able to support associative, communicative, and idempotent operations. This can mean architecting solutions using structures like sets and hashmaps, sometimes in creative ways. This is just one of the trade-offs to considered. Since I’m talking about datatypes, what does the LVar package currently support?

  • Min - Values only decrease.
  • Max - Values only increase.
  • Boolean - Starts as false, once changed to true, it can never be false again.
  • Set - Once a value is added, it cannot be removed.
  • PSet - Same as a set, but values are positive numeric values only.
  • Bag - Similar to a set, but there can be multiple instances of a value. Multiplicity of values is tracked, but values can only be added, not removed.
  • Map - Keys can only be added. Values are LVars.
  • Intervals - Intervals are ranges defined by min and max values. They increase in information by getting tighter, or more precise.

Beyond datatype support, what does the LVar interface look like? All LVars have common functions (see below). They also have their own type-appropriate supported functions (e.g. AND for LBool, Union for LSet, etc) while excluding non-conformating functions (e.g. remove).

  • init - Create an LVar.
  • set - Set/Update the value of the LVar within its defined constraints.
  • merge - Combine two LVars into a single LVar.
  • reveal - Unwrap the LVar into its F#-primative value.

I often turn to examples to help solidify concepts in my head. This is especially helpful when dealing with mathematical structures. It really helps to form a pattern and shape of these variables. The first example I will use is an LBool (LVar Boolean).

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
// Initializing an LBool
let bobVoted = LBool.init false

// Setting an LBool (to true)
let bobVoted = LBool.set true bobVoted

// Setting an LBool (to false)
// NOTE: The resulting value is still true (once Bob votes, he can't unvote)
let bobVoted = LBool.set false bobVoted

// Unwrap an LBool as a bool
bobVoted |> LBool.reveal |> printfn "Bob voted: %b"

// Merge two LBools (merging data from two different processes)
// NOTE: If one of these in true, the result is true
let bobVoted = LBool.merge bobVotedServer1 bobVotedServer2

Looking at another example, LMax only increases. This means set is the greater of the provided LMax, and the newly provided numeric value. Of course this is the kind of business logic is easy enough to write, but it can be nice this intent is encoded in the variable so you don’t have to worry about it. This ties back to the earlier idea of including intent in the type definitions used. This level of self-documentation goes a long way to code comprehension as well.

1
2
3
4
5
6
7
8
9
10
11
// Initializing an LMax
let highScore = LMax.init 0

// Setting an LMax (value increases to 525)
let highScore = LMax.set 525 highScore 

// Setting an LMax (value doesn't change (310 < 525))
let highScore = LMax.set 310 highScore 

// Merges two LMaxs (taking the higher value)
let highScore = LMax.merge highScoreServer1 highScoreServer2

For the last example I’ll use a more complex type, LInterval. The goal of LInterval is to maintain a range of values, where increasing information tightens the range. If this sounds familar, its because I’ve worked with this concept before in my Propagator package. Below I have some examples of creating, updating, and merging interval ranges. 

1
2
3
4
5
6
7
8
9
// Set a temp based on the knowledge that the temperature is at least 17 degrees
let tempStation1 = LInterval(Interval(Some 17, None))

// Set a temp based on the knowledge that the temperature is 20 +- 5 degrees 
let tempStation2 = LInterval(Interval(Some 15, Some 25))

// Aggregate temperature data from multiple stations (resulting range is 17-25 degrees)
let temp = LInterval.merge tempStation1 tempStation2 
printfn "Temperature Estimate: %A" (Interval.toTuple(temp.reveal))

This is a light view of what join-semilattices and LVars can bring to the table. I hope you’ve found the concepts and possibilities interesting. The package itself is still a work in progress, but I wanted to share current progress. My hope is this inspires to see code and data differently, and perhaps even experiment with new ways to code. That’s one of the many things I enjoy pulling from programming language research. Even if the specific implementation doesn’t make sense for me currently, the additional perspective inevitably improves my future code and designs in some way. Until next time.

References:

Related Posts: