Merge pull request #356 from byorgey/patch-1

Replace "rights" with "writes"

Author: goldfirere

podcast/34/transcript.markdown

@@ -38,7 +38,7 @@ So there’s some tricks that you can play to make sure that a program is determ
 
 What I did during my PhD was kind of look at one classic approach to deterministic parallelism and then generalize it a little bit. That was what the work on LVarS was. We took this kind of classic work on what are called IVars, which are variables that can only be written to once, and that if you try to read from an IVar, your attempt to read will block until it’s been written to. So it’s a sort of synchronization variable where if I try to read from an IVar and it hasn’t been written to yet, my attempt to read will block until somebody else comes – some other thread perhaps comes along and writes to it, and then I can read from it. That’s an IVar.
 
-The monad-par library is an IVar library for Haskell. So it’s a library that’s available. It’s also actually discussed in Simon Marlow’s book on Parallel and Concurrent Programming in Haskell. And what we did for my PhD was generalize the notion of IVars to what we call LVars. And so an LVar is a generalization of IVar where you can write to it multiple times, but those rights have to be increasing in some sense. So, for instance, you could have a counter where you can only count up. I could increment the counter, but I could never decrement. And then we’ve made rights more expressive now. We can do multiple rights. So if we want to keep determinism, we have to do something to kind of simultaneously decrease the expressivity of reads. So now, instead of being able to arbitrarily read a value out of that counter, instead, I can only ask a question like, has the counter reached, let’s say, the value 5 yet? And so that’s a question which will know, either it will eventually become true given certain inputs or it won’t. But the program will deterministically produce an answer given the same inputs, regardless of scheduling. 
+The monad-par library is an IVar library for Haskell. So it’s a library that’s available. It’s also actually discussed in Simon Marlow’s book on Parallel and Concurrent Programming in Haskell. And what we did for my PhD was generalize the notion of IVars to what we call LVars. And so an LVar is a generalization of IVar where you can write to it multiple times, but those writes have to be increasing in some sense. So, for instance, you could have a counter where you can only count up. I could increment the counter, but I could never decrement. And then we’ve made writes more expressive now. We can do multiple writes. So if we want to keep determinism, we have to do something to kind of simultaneously decrease the expressivity of reads. So now, instead of being able to arbitrarily read a value out of that counter, instead, I can only ask a question like, has the counter reached, let’s say, the value 5 yet? And so that’s a question which we know, either it will eventually become true given certain inputs or it won’t. But the program will deterministically produce an answer given the same inputs, regardless of scheduling. 
 
 And so that’s what LVars are. They generalize IVars a little bit to let you do this multiple increasing or what we call inflationary reads, or sorry, writes. And then reads have to be what you call threshold reads, which means you can only ask this limited set of questions. And you can put those together to get – what it turns out is a data structure that’s useful for deterministic parallel programming. 
 
@@ -58,7 +58,7 @@ The concern there is not so much having this sort of fine-grained control over t
 
 *LK (0:14:13)*: So I would say distributed programming is just hard no matter what, and I don’t think Haskell is any kind of silver bullet here. However, I think that if you’re using a programming language that lets you rule out certain classes of bugs, right, which Haskell does, then that perhaps frees you up to have the bandwidth to think about a different kind of bug, which maybe the language doesn’t rule out for you. But if you want to be concerned with dealing with correctness of a distributed system, then it’s nice to not have to worry about the kinds of bugs that Haskell does let you avoid. 
 
-So I think the point that you’re raising is interesting. When I was working on my PhD, one of the things that we wanted to be able to implement LVars—and then this is also true for CRDTs—is within LVar, you’re getting these rights. Your data structure, you’re getting rights. They’re coming in from different threads. For CRDT, it would be similar except you’re receiving updates from different processes, perhaps over a network. And you want to ensure that updates are inflationary. That is, that you’re only – the contents of your data structure will only ever grow over time. And moreover, the different states that that data structure can take on, they have to be elements of a certain algebraic structure that’s called a join-semilattice, right? So there wasn’t really anything, any way to express in the Haskell type system that that was true. And I really wished that there was some way that I could say, using Haskell types, that these updates are inflationary or that the state this data structure can take on are elements of a lattice, and so on. And so I was frustrated that I couldn’t do that. Liquid Haskell was just beginning to come on the scene at the time when I was doing my PhD, and it’s a really promising technology to be able to express those kinds of properties. But Liquid Haskell was kind of – as I was doing my PhD, Liquid Haskell was kind of just more getting off the ground. And so this was like 2013, 2014. It was an exciting idea, but it wasn’t really ready for us to use yet. 
+So I think the point that you’re raising is interesting. When I was working on my PhD, one of the things that we wanted to be able to implement LVars—and then this is also true for CRDTs—is within LVar, you’re getting these writes. Your data structure, you’re getting writes. They’re coming in from different threads. For CRDT, it would be similar except you’re receiving updates from different processes, perhaps over a network. And you want to ensure that updates are inflationary. That is, that you’re only – the contents of your data structure will only ever grow over time. And moreover, the different states that that data structure can take on, they have to be elements of a certain algebraic structure that’s called a join-semilattice, right? So there wasn’t really anything, any way to express in the Haskell type system that that was true. And I really wished that there was some way that I could say, using Haskell types, that these updates are inflationary or that the state this data structure can take on are elements of a lattice, and so on. And so I was frustrated that I couldn’t do that. Liquid Haskell was just beginning to come on the scene at the time when I was doing my PhD, and it’s a really promising technology to be able to express those kinds of properties. But Liquid Haskell was kind of – as I was doing my PhD, Liquid Haskell was kind of just more getting off the ground. And so this was like 2013, 2014. It was an exciting idea, but it wasn’t really ready for us to use yet. 
 
 And then I stepped away from distributed programming for a while in the time after my PhD and while I was working at Intel. And so it was really exciting to me when I came back to thinking about this stuff and began getting more serious about distributed systems, especially with an eye toward verification to come back to this stuff after I started my faculty position in 2018 and returned to looking at Liquid Haskell, realizing that Liquid Haskell had made a lot of progress in the intervening years and realized that it actually was a viable tool for being able to express and prove the kinds of properties that I had always wanted to be able to state and prove using Haskell type.