Propel

Type-check algebraic laws!

Track commutativity, associativity, idempotency, and other algebraic properties in types

Propel is a programming language developed in the Programming Group at the University of St. Gal­len. It allows developers to annotate functions with algebraic properties such as commutativity, associativity, and idempotency. Propel’s type system uses a specialized automated inductive theorem prover to reason about these properties.

Try Propel

We compiled Propel to JavaScript using Scala.js for you to try the latest version locally in your browser.

Definitions

  • (def <var> [<type>] <expr>)
    Introduces a definition that is bound to <var> in the rest of the program. Recursive definitions must designate their type. Non-recursive definitions leave out the type declaration.
  • (type <var> <type>)
    Introduce a recursive or non-recursive type alias <var> for <type> in the rest of the program.
  • (prop-for <var> ([forall <[var type]...>] (== <expr> <expr>)))
    Asserts a universally quantified equation to be proven for the definition referenced by its identifier <var>. The universally quantified variables are of the form (<var type>). The equality is of the form (== <expr> <expr>).

Expressions

  • (lambda [<[properties...]>] <[var type]...> <expr>)
    A lambda expression with zero or more <properties>, one or more arguments of the form (<var> <type>), and a body <expr>. The annotated properties are type-checked and will be part of the function’s type.
  • (let <pattern> <expr> <expr>)
    Introduces a definition for each free variable in a given pattern (that must be exhaustive) which matches the first expression in the second expression. Non-trivial patterns are useful when a type has only one constructor, for example Tuple.
  • (letrec <[var type expr]...> <expr>)
    Introduces a recursive definition for the first expression that has the designated type and is bound to <var> in the last expression.
  • (lettype <[var type]...> <expr>)
    Introduces a recursive or non-recursive type alias <var> for <type> in <expr>.
  • (cases <expr> <[pattern expr]...>)
    Pattern-matches on the result of the first expression. Cases are surrounded by square brackets and each case has one pattern and one expression to be executed if the case matches.
  • (if <expr> <expr> <expr>)
    Performs a conditional check. The first expression must reduce to either True or False.
  • (not <expr>)
    Negates the booleans True or False.
  • (and <expr> <expr>)
    Computes the conjunction of two booleans.
  • (or <expr> <expr>)
    Computes the disjunction of two booleans.
  • (implies <expr> <expr>)
    Computes the implication between two booleans where the first expression is the antecedent and the second expression is the consequent.
  • (<constructor> <expr...>)
    Applies a constructor to its arguments.
  • (<expr> <expr...>)
    Applies an expression to its arguments.
  • (<expr> <[expr...]>)
    Applies an expression to its type arguments.

Patterns

  • (<K> <pattern...>)
    A pattern that will only match expressions constructed with the constructor <K> and whose arguments match each subpattern.

Types

  • {<constructor...>}
    Defines a tagged union defined by at least one constructor. Additionally, if constructors take arguments, then the arguments’ types must follow after the constructor inside parenthesis.
  • (fun <type...> <type>)
    Defines a function type and with one or more arguments (of the form <type>) and a result <type>.
  • (rec <var> <type>)
    Defines a recursive type and <var> will be bound to the recursive type inside <type>.
  • (forall <var> <type>)
    Defines a polymorphic type and <var> that is bound in <type>.

Properties

  • comm
    Commutativity: f x y = f y x
  • assoc
    Associativity: f (f x y) z = f x (f y z)
  • idem
    Idempotency: f x x = x
  • sel
    Selectivity: f x y = x or f x y = y
  • refl
    Reflexivity: f x x = True
  • irefl
    Irreflexivity: f x x = False
  • sym
    Symmetry: If f x y = True then f y x = True
  • antisym
    Antisymmetry: If f x y = True and f y x = True then x = y
  • asym
    Assymetry: If f x y = True then f y x = False
  • conn
    Connectedness: f x y = True or f y x = True
  • trans
    Transitivity: If f x y = True and f y z = True then f x z = True 

                
            

            

                
Click Check to check your code

            

        

        


    






    
Example: Addition of Peano Numbers and Vectors

    
The following example defines the following functions with their algebraic properties to be proven:

    
    
The following two code snippets show the implementations of these functions using Propel’s language which you can use in the editor above, and using Propel’s Scala DSL.

    

        

            
Propel Language


(type nat {(S nat) Z})            ; natural numbers
(type list {(Cons nat list) Nil}) ; lists

(def add (fun nat nat nat)
  (lambda [comm assoc] (a nat) (b nat)
    (cases a
      [Z b]
      [(S a) (S (add a b))])))

(prop-for add (forall (b nat) (== (add Z b) b))) ; left identity

(prop-for add (forall (a nat) (== (add a Z) a))) ; right identity

(def zipWith (fun (fun nat nat nat) list list list)
  (lambda (f (fun nat nat nat))
    (lambda [comm assoc idem] (x list) (y list)
      (cases (Tuple x y)
        [(Tuple Nil y) Nil]
        [(Tuple x Nil) Nil]
        [(Tuple (Cons x xs) (Cons y ys))
         (Cons ([comm assoc idem] f x y) (zipWith f xs ys))]))))

(def addVectors
  (lambda [comm assoc] (x list) (y list) (zipWith add x y)))

    


        

            
Propel in Scala


enum ℕ:
  case Z
  case S(p: ℕ)

def add =
  prop.rec[(Comm & Assoc) := (ℕ, ℕ) =>: ℕ]: add =>
    props(
      (b: ℕ) => add(Z, b) =:= b, // left identity
      (a: ℕ) => add(a, Z) =:= a  // right identity
    ):
      case (Z, b) => b
      case (S(a), b) => S(add(a, b))

def zipWith[P >: (Comm & Assoc & Idem), T] =
  prop.rec[(P := (T, T) =>: T) =>
           (P := (List[T], List[T]) =>: List[T])]:
    zipWith => f =>
      case (Nil, y) => Nil
      case (x, Nil) => Nil
      case (x :: xs, y :: ys) => f(x, y) :: zipWith(f)(xs, ys)

def addVectors =
  prop[(Comm & Assoc) := (List[ℕ], List[ℕ]) =>: List[ℕ])]:
    zipWith(add)

        

    


    
Use Case: Conflict-Free Replicated Datatypes (CRDTs)

    
    

    A state-based Conflict-Free Rep­li­cat­ed Da­ta Type (CRDT) is any datatype that defines a merge function that combines any two instances—any two replicas—into one without any conflict or manual conflict resolution.
    We expect the two following properties to hold:
    

    
    
        
  1. The order of merging any number of replicas should not change the result, and
    2. 
        
  2. merging a replica with itself must not introduce any change to that replica, i.e. the replica remains constant.
    3. 
    

    

    When applied to two replicas the first property entails that merge must be commutative.
    When applied to three or more replicas the first property entails that merge must be associative.
    And the second property entails that merge must be idempotent.
    


    
Example: GCounter

    
    
A conflict-free rep­li­cat­ed grow­ing count­er (GCounter) between three peers is implemented as a map between a peer’s identifier and a number.
    The counter not only tracks the number of increments but tracks the origin of each increment.
    For example in the following figure, at the beginning—on the first line—the purple peer incremented the counter 9 times, received 0 increments from the yellow peer and 3 increments from the green peer.
    On the other hand the yellow peer received 7 increments from the purple peer, incremented its counter 2 times, and received 4 increments from the green peer.
    After syncing the purple and the yellow peer—on the second line—both agree on the number of increments.
    They do so by taking the pair-wise maximum number of increments.
    Finally after all peers sync—on the last line—they all agree on the number of increments and they are all able to deduce that there were 9 + 2 + 5 = 16 increments in total among them.
    

    
The following two code snippets show how a GCounter can be implemented using Propel’s language which you can use in the editor above, and using Propel’s Scala DSL.

    

        

            
Propel Language


(type nat {Zero (Succ nat)})      ; natural numbers
(type list {Nil (Cons nat list)}) ; lists

(def max (fun nat nat nat)
  (lambda [comm assoc idem] (x nat) (y nat)
    (cases (Tuple x y)
      [(Tuple Zero y) y]
      [(Tuple x Zero) x]
      [(Tuple (Succ a) (Succ b)) (Succ (max a b))])))

(def mergeGCounter (fun list list list)
  (lambda [comm assoc idem] (x list) (y list)
    (cases (Tuple x y)
      [(Tuple Nil _) Nil]
      [(Tuple _ Nil) Nil]
      [(Tuple (Cons a xs) (Cons b ys))
       (Cons (max a b) (mergeGCounter xs ys))])))

    


        

            
Propel in Scala


enum Nat:
  case Zero
  case Succ(pred: Nat)

def max =
  prop.rec[(Comm & Assoc & Idem) := (Nat, Nat) =>: Nat]: max =>
    case (Zero, y) => y
    case (x, Zero) => x
    case (Succ(n), Succ(m)) => Succ(max(n, m))

def zipWith[P >: (Comm & Assoc & Idem), T] =
  prop.rec[(P := (T, T) =>: T) =>
           (P := (List[T], List[T]) =>: List[T])]:
    zipWith => f =>
      case (Nil, y) => y
      case (x, Nil) => x
      case (x :: xs, y :: ys) => f(x, y) :: zipWith(f)(xs, ys)

def mergeGCounter =
  prop[(Comm & Assoc & Idem) :=
       (List[Nat], List[Nat]) =>: List[Nat]]:
    zipWith(max)

        

    


    
How do we guarantee that implementations of merge satisfy these properties?

    

    The state of the art is to verify models of these CRDTs manually or automatically by instantiating some framework.
    Other works have developed code synthesizers that generate a merge function with the required properties given the desired semantics.
    Both approaches limit developers.
    Our solution is to develop a type-system that tracks these properties and a compiler that can prove these properties at compile-time.
    


    
Properties We Support

    
Binary Functions

    

    

        
Commutativity

        
        
A commutative function is one whose arguments can be given in any order without changing the result

        
E.g. Average of two numbers

        
    

    

        
Idempotency

        
        
If an idempotent function is called with the same argument it must return it

        
E.g. Set union

        
    

    

        
Associativity

        
        
An associative function is one that can be folded in any direction on arguments without changing the result

        
E.g. List concatenation

        
    

    

        
Selectivity

        
        
A selective function must always return one of its arguments

        
E.g. Maximum of two numbers

        
    

    



    
Binary Relations

    

        

            
Reflexivity

            
            
A reflexive relation is one where every element is related to itself

            
E.g. Equality

            
        

        

            
Symmetric

            
            
A symmetric relation is one where an element is related to another if and only if the other is related to it

            
E.g. Inequality

            
        

        

            
Transitivity

            
            
In a transitive relation if an element a is related to b and b is related to c then a must be related to c

            
E.g. Ancestry

            
        

        

            
Connectivity

            
            
A connected relation is one where between any two distinct elements some relation exists

            
E.g. Total order

            
        

        

            
Antisymmetry

            
            
An antisymmetric relation is one where between any two distinct elements at most one relation exists

            
E.g. Divisibility

            
        

    


    
Getting Started



Building and Loading the Propel Docker image




We provide you with propel.tar.xz on Zenodo (doi: 10.5281/zenodo.7817421), which is a pre-built container image that contains all necessary programs.
To load, run the following command:



$ docker load < propel.tar.xz




Further, we also provide the option to build the contain anew. To build, run the
following command which takes between 10 and 20 minutes:



$ docker build -t propel .




Rebuilding the image may not work on Apple M1 machines because of incomplete emulation of system calls (specifically the inotify kernel subsystem).
Hence, we recommend rebuilding the image on a platform fully supported by Docker, like x86-64 systems.




Compiling Propel



The provided container already contains a binary executable of Propel.





To compile Propel to Java bytecode yourself, run the following command:



$ docker run -it --rm propel bash -c 'cd /propel; sbt clean compile'




To compile Propel to a native binary yourself, run the following command:



$ docker run -it --rm propel bash -c 'cd /propel; sbt clean nativeLink'




Compiling Propel, to bytecode or to a native executable, may not work inside the Docker container on Apple M1 machines for the reasons mentioned earlier.





The resulting binary is at /propel/​.native/​target/​scala-3.2.2/​propel.
The propel executable in the $PATH is already symlinked to that binary file.
Hence, by default, you can just run propel.




From the Propel Docker image



Propel is also provided as a DSL in Scala.
To experiment with the DSL, we invite you take a look into the following files in the Propel Docker image:
/propel/​src/​test/​scala/​propel/​ScalaExamplesNat.scala,
/propel/​src/​test/​scala/​propel/​ScalaExamplesNum.scala and
/propel/​src/​test/​scala/​propel/​ScalaExamplesList.scala inside the container.





As an example, you can execute the following commands to run a shell, explore the files and recompile the project:



$ docker run -it --rm propel bash                               # open a shell
$ nano /propel/src/test/scala/propel/ScalaExamplesList.scala    # open the file

# edit and save the file
$ cd /propel && sbt Test/compile                                # recompile




Compiling the examples may not work inside the Docker container on Apple M1 machines for the reasons mentioned earlier.





You may define your own function using the following syntax:



def myFunction = prop[(FunctionProperties) := (T1, T1) =>: T2] { (x, y) => body }
// or
def myRecursiveFunction = prop.rec[(FunctionProperties) := (T1, T1) =>: T2] { myRecursiveFunction => (x, y) => body }



Here, myFunction is the name of the function, FunctionProperties is a list of function properties the function has (separated by &), T1 is the type of the arguments of the binary function, T2 is the return type of the function, x and y are the names of the function arguments, and body is the function body.





The function properties are chosen from the following list: Comm, Assoc, Idem, Sel, Refl, Antisym, Trans, Conn, and Sym.





If Propel is able to prove the properties that the function is annotated with, then compilation succeeds.
If the properties cannot be proven, then a compilation error indicates which property could not be proven.





For example, you can add the following GCounter CRDT example to one of the files in /propel/​src/​test/​scala/​propel:



def mergeGCounter = prop[(Comm & Assoc & Idem) := (List[Num], List[Num]) =>: List[Num]] { zipWith(maxNum) }



    
Publications

    
    
        
  1. George Zakhour, Pascal Weisenburger, and Guido Salvaneschi. 2024.  Automated Verification of Fundamental Algebraic Laws.
            Proceedings of the ACM on Programming Languages 8, PLDI, Article 178, June 24–28, 2024, Copenhagen, Denmark. https://​doi.org/​10.1145/3656408 [author version]
    2. 
        
  2. George Zakhour, Pascal Weisenburger, and Guido Salvaneschi. 2023. Type-Checking CRDT Convergence.
            Proceedings of the ACM on Programming Languages 7, PLDI, Article 162, June 17–21, 2023, Orlando, Florida, United States. https://​doi.org/​10.1145/3591276 [author version]
    3.