Efficient Linear Algebra with Plover

January 3, 2016

Finding your position with GPS satellites takes complicated math. It’s a challenging problem in the best case, and becomes even harder on resource constrainted computers such as thosed used by Swift Navigation to create affordable, accurate GPS chips.

Swift Navigation must use efficient C code on the chip to work within memory constraints. They discovered that writing numerical algorithms in a low level language is error prone, so Scott Kovach and Kyle Miller decided to create a lienar algebra domain specific language which compiles into efficient idiomatic C.

In this video Scott discusses language design and how he implemented the DSL in Haskell.


  • What is a computer language?
    • First and foremost it’s made of the people who use and develop it
    • Second, its syntax for expressing ideas
    • Third, perhaps the distinguishing part is that it can be turned into machine code and executed
    • Fourth, the body of work that has been created within it
    • These are each different forces defining and acting on a language
  • Scott works at Swift Navigation creating high precision low cost GPS units
    • The devices have constrained resources
    • “Doing” GPS requires lots of matrix math
  • Their goal is to prototype and test algorithms then compile them into C code to run on the chips
    • Historically they’ve had trouble with this
    • It was difficult to verify that the embedded implementation matches the modeling of the algorithm
    • So they built a language to make it easier
  • Design goals
    • The syntax should allow easy implementations of certain textbook numerical algorithms
    • Support low-level details along with matrix arithmetic
    • No additional memory used by the abstraction
    • Static verification of the math
    • Human-readable C code output (a problem with existing code generation programs)
  • Why not code directly in C?
    • We want to be able to express arithmetic the way we would do in math
    • Multiplying scalars by scalars, vectors, or matrices
    • C requires lots of for-loop and/or function calls and it gets tedious and error prone
  • An overview of the linguistic properties of plover
  • Linear algebra refresher
    • Two ways to think of a matrix: a representation of a linear function
    • Since we’re computing we care only about fininite dimensional vector spaces
    • Matrix multiplication is function composition
    • Plover checks for improper multiplication (that multiplicand columns and rows are appropriate)
    • An visual example of multiplying two matrices
  • Comparison of a Plover “hello world” program and the C it generates
  • Plover detects opportunities for optimization, such as when the programmer explicitly creates a diagonl matrix
  • Details of the problems of type checking
  • “Real World Plover” - check out the docs
  • A final example