#Mechanized #proof of the #commutativity of #zipWith in #LiquidHaskell (continued in replies)

First, we define a type alias with a value argument (it behaves like a macro for refinement types) to describe a proof of the commutativity of some binary function "A":
```
{-@ type Commutative a A = x:a -> y:a -> {A x y == A y x} @-}
```
This says: For some value, A, and for all values x and y, passing x then y to A gives the same result as passing them in the other order.

Is there anyone who knows about #CRDT (#CmRDT) and is bored enough to have a discussion about #Commutativity, #Concurrency and #Causality? Trying to get my head around whether causal ordering is really required if all operations on your commute.

I don't have too much faith, but if this works then truly, #MastodonRules!

#DistributedSystems