The Ling Language

modular and precise resource management

Nicolas Pouillard

2015-12-28, 32nd Chaos Communication Congress

Introduction

Optimizations

improving
safe
automatic
predictable

        +-----+               +-----+
  input |     | intermediate  |     | output
 ------>|  F  |-------------->|  G  |------->
  data  |     |    data       |     |  data
        +-----+               +-----+

        +----------+
  input |          | output
 ------>|    FG    |------->
  data  |          |  data
        +----------+

In case of emergency, you can:

make F a better producer
make G a better consumer
decide to allocate

Where does Ling go?

Numerical computation
Embedded systems
Drivers and Kernels
Security and cryptography

What does Ling feature?

Terms are used for meta-programming and as data.
Processes are used to describe behavior.
Types enforce a safe use of data by terms.
Sessions enforce a safe behavior of processes.
Dependent types and sessions enable formal verification.
Duality sessions enables fusion.

Where does Ling come from?

Purely Functional Programming (λ-calculus, Haskell)
Dependent Types (Martin-Löf Type Theory, CoC)
Formal verification (Coq, Agda, Idris)
Communicating processes (π-calculus, Erlang)
Session Types and Linear Logic:
- A lot of existing research papers
- Dependent protocols for communication together with Daniel Gustafsson and Nicolas Guenot at the IT-University of Copenhagen
- Limestone by Jean-Philippe Bernardy and Víctor López Juan at the University of Chalmers

Matrix Multiplication

\[(A·B)_{ij} = \sum_{k=0}^{m-1} A_{ik} × B_{kj}\]

Bₘₓₚ

Aₙₓₘ

(A·B)ₙₓₚ

\(zipP(u,v)_k\)	\(= u_k × v_k\)
\(sumD(w)\)	\(= \sum_{k=0}^{m-1} w_{k}\)
\(dotP(u,v)\)	\(= sumD(zipP(u,v))\)

Outline

Your first Ling program
Types as an approximation
Duality
Allocation & Fusion
Back to matrix multiplication

Your first Ling program

Notations

? : What I am going to read?

! : Here is what I write!

double =
  proc{a: ?Int, b: !Int}
    let x <- a.
    b <- x + x

proc{b: !Int}
  new (a: Int).
  a <- 21.
  @double{a, b}

Replacing @double by its definition:

proc{b: !Int}
  new (a: Int).
  a <- 21.
  let x <- a.
  b <- x + x

Fusing away the allocation:

proc{b: !Int}
  let x = 21.
  b <- x + x

Expanding local definitions:

proc{b: !Int}
  b <- 42

How I Learned to Stop Worrying and Love the Types

If you believe that...

Type systems are just here to reject programs
Java, C#, C++ have a good type system
Unit testing can replace a type system

Think again...

Actually, good type systems can:

Explain why/where your program can fail
Empower the compiler for optimizations
Automate parts of your program

A type is an approximation
which enables abstraction

Approximate at will

    +--------+
 a  |        | d = a / b
--->|        |----------->
    | divmod |
--->|        |----------->
 b  |        | m = a % b
    +--------+

Processes can be composed in parallel and sequentially.
Sessions enable a precise control of the process interface.
Linearity ensures that reads and writes happen exactly once.

Approximate at will

proc{   a: ?Int, b: ?Int ,  d: !Int, m: !Int   } -- Any order
proc[:  a: ?Int, b: ?Int ,  d: !Int, m: !Int  :] -- In order
proc[   a: ?Int, b: ?Int ,  d: !Int, m: !Int   ] -- All in parallel
proc[: [a: ?Int, b: ?Int], [d: !Int, m: !Int] :] -- ∥ read; ∥ write
proc[: {a: ?Int, b: ?Int}, [d: !Int, m: !Int] :] -- Any read; ∥ write
  let x <- a.
  let y <- b.
  d <- x / y.
  m <- x % y
  ( let x <- a
  | let y <- b).
  ( d <- x / y
  | m <- x % y)
  let y <- b.
  let x <- a.
  m <- x % y.
  d <- x / y

  let x <- a.
  let y <- b.
  ( d <- x / y
  | m <- x % y)
  let y <- b.
  let x <- a.
  ( d <- x / y
  | m <- x % y)
  ( let x <- a
  | let y <- b).
  d <- x / y.
  m <- x % y

Duality

S	`~S`
`!A`	`?A`
`{S₀, ..., Sₙ}`	`[~S₀, ..., ~Sₙ]`
`[:S₀, ..., Sₙ:]`	`[:~S₀, ..., ~Sₙ:]`

Example

~{ !Int, [: ?Double, ?Int:]}
= [~!Int,~[: ?Double, ?Int:]]
= [ ?Int,~[: ?Double, ?Int:]]
= [ ?Int, [:~?Double,~?Int:]]
= [ ?Int, [: !Double, !Int:]]

Allocation & Fusion

Allocation with Fusion

S a session (!Int, {!Int,?Double})
F a process following S
G a process following the dual of S

new [ c : S, d : ~S ].
( @F{c}
| @G{d} )

new [: c : S, d : ~S :].
@F{c}.
@G{d}

Mandatory Allocation

F = proc(u: {!Int^100}) ...
G = proc(u: {?Int^100}) ...

FG = proc()
  new/alloc [: u: {!Int^100}, v: {?Int^100} :]
  @F{u}.
  @G{v}

Or:

F = proc(u: [!Int^100]) ...

G = proc(u: [?Int^100]) ...

Back to Matrix Multiplication

ZipWith and pointwise product

zipP = zipWith Double Double Double _*D_

zipWith =
  \(A B C: Type)
   (f: (a: A)(b: B)-> C)
   (n: Int)->
  proc{[: a: ?A^n :], [: b: ?B^n :], [: c: !C^n :]}

    slice (a,b,c)^n (cc <- f (<- a) (<- b))

Fold-left and summation

sumD = foldl Double Double _+D_ 0.0

foldl = \(A B: Type)
         (f: (acc: B)(a: A)-> B)
         (init: B)
         (n: Int)->
  proc[: [: ai: ?A^n :], cr: !B :]

    new (tmp: B).
    tmp <- init.
    slice (ai)^n
      (tmp <- f (<- tmp) (<- a)).
    fwd(?B)(tmp,cr)

Dot product

dotP = \(n : Int)->
  proc{u: [: ?Double^n :],
       v: [: ?Double^n :],
       o: !Double}

    new [: w: [: !Double^n :], w' :]
    @(zipP n){u, v, w}.
    @(sumD n)[:w', o:]

Fused dot product

fused_dotP = \(n : Int)->
  proc{[: ai: ?Double^n :],
       [: bi: ?Double^n :],
       o : !Double}

  new (tmp : Double).
  tmp <- 0.0.
  (slice (ai, bi)^n
    let a <- ai.
    let b <- bi.
    let c <- tmp.
    tmp <- (c +D (a *D b))).
  let x <- tmp.
  o <- x

Precision	+ Modularity
	=

Cost Free Abstraction!

Fusion:

predictable + safe + automatic

https://github.com/np/ling