Functional Programming

Jean-Baptiste Tristan & K. Rustan M. Leino

Overview

Dafny is a statically and strongly typed programming language
A functional program is essentially made of three kinds of definitions
- Functions
- Constants
- Datatypes
- Type synonyms

Function declaration

Here is an example function definition

  function FunctionName(x: X, y: Y): R {
    expression
  }

Declared with the keyword function
Has a name: FunctionName
Has typed parameters: x and y, respectively of types X and Y
Has a return type: R
Has a body: expression

Function body

The body of a function is an expression
An expression has a type
An expression can be evaluated and produces a value of that type
Evaluating an expression has no side effect

Calling a function

  function F(n: int, m: int): int {
    n + m
  }

  function G(n: int): int {
    F(n + n, n * n)
  }

To call a function, the type of the arguments must match that of the parameters
Arguments are evaluated before the function is called
The arguments are then substituted in the body of the function
The type of the expression must match the return type

Constants

The arity of a function is the number of parameters
A constant is a function with arity 0, written without the parentheses
Declared with the keyword const

  const constantName: Type := expression

Predicates

A function whose return type is bool is also called a predicate
Declared with keyword predicate
Return type is implicit

  predicate predicateName(x: X, y: Y) {
    booleanExpression
  }

Expressions

We will now introduce the language of expressions
We call this set of expressions “functional expressions”
- There will be others
Dafny has 5 primitive scalar types:
- Booleans (bool)
- Integers (int)
- Reals (real)
- Characters (char)
- Bit vectors (bv0, bv1, bv2, …, bv32, …)

Type test

Every expression has a type
There is an expression to test if an expression is of a certain type
It uses the keyword is
It evaluates to a Boolean value
We will use that expression and predicates to introduce the syntax and types of expressions in Dafny
That way, you learn Dafny by reading Dafny

  predicate IntPlus3IsInt(n: int) { (n + 3) is int }

Booleans

  predicate False() { false is bool }

  predicate True() { true is bool }

  predicate Conjunction(a: bool, b: bool) { (a && b) is bool }

  predicate Disjunction(a: bool, b: bool) { (a || b) is bool }

  predicate Implication(a: bool, b: bool) { (a ==> b) is bool }

  predicate Explication(a: bool, b: bool) { (a <== b) is bool }

  predicate Equivalence(a: bool, b: bool) { (a <==> b) is bool }

  predicate Negation(a: bool) { !a is bool }

Integers

  predicate DecimalLiteral() { 38 is int }
  predicate HexadecimalLiteral() { 0xBadDecaf is int }
  predicate ReadableLiteral() { 4_345_765 is int }
  predicate Negation(n: int) { -n is int }
  predicate Addition(n: int, m: int) { (n + m) is int }
  predicate Substraction(n: int, m: int) { (n - m) is int }
  predicate Multiplication(n: int, m: int) { (n * m) is int }
  predicate Division(n: int, m: int) { (n / m) is int }
  predicate Modulus(n: int, m: int) { (n % m) is int }
  predicate Equality(n: int, m: int) { (n == m) is bool }
  predicate Disequality(n: int, m: int) { (n != m) is bool }
  predicate SmallerOrEqual(n: int, m: int) { (n <= m) is bool }
  predicate Smaller(n: int, m: int) { (n < m) is bool }
  predicate GreaterOrEqual(n: int, m: int) { (n >= m) is bool }
  predicate Greater(n: int, m: int) { (n > m) is bool }

Reals

  predicate DecimalLiteral() { 38.98 is real }
  predicate ReadableLiteral() { 4_345_765.999_987 is real }
  predicate Negation(n: real) { -n is real }
  predicate Addition(n: real, m: real) { (n + m) is real }
  predicate Substraction(n: real, m: real) { (n - m) is real }
  predicate Multiplication(n: real, m: real) { (n * m) is real }
  predicate Division(n: real, m: real) { (n / m) is real }
  predicate Equality(n: real, m: real) { (n == m) is bool }
  predicate Disequality(n: real, m: real) { (n != m) is bool }
  predicate SmallerOrEqual(n: real, m: real) { (n <= m) is bool }
  predicate Smaller(n: real, m: real) { (n < m) is bool }
  predicate GreaterOrEqual(n: real, m: real) { (n >= m) is bool }
  predicate Greater(n: real, m: real) { (n > m) is bool }
  predicate IntegerToReal(k: int) { (k as real) is real }
  predicate Floor(n: real) { (n.Floor) is int }

Characters

Characters are Unicode

  predicate ASCII() { 'a' is char }
  predicate SingleQuote() { '\'' is char }
  predicate DoubleQuote() { '\"' is char }
  predicate BackSlash() { '\\' is char }
  predicate NullCharacter() { '\0' is char }
  predicate LineFeed() { '\n' is char }
  predicate CarriageReturn() { '\r' is char }
  predicate Tab() { '\t' is char }
  predicate Unicode() { '\U{1F71D}' is char }
  predicate Addition(a: char, b: char) { (a + b) is char }
  predicate Substraction(a: char, b: char) { (a - b) is char }
  predicate Less(a: char, b: char) { (a < b) is bool }
  predicate LessEqual(a: char, b: char) { (a <= b) is bool }
  predicate Greater(a: char, b: char) { (a > b) is bool }
  predicate GreaterEqual(a: char, b: char) { (a >= b) is bool }

Other expressions

  predicate ConditionalExpression<T>(bexpr: bool, expr1: T, expr2: T)  { 
    (if bexpr then expr1 else expr2) is T
  }

  predicate LetBinding<U, V>(expr1: U, expr2: V) { (var x := expr1; expr2) is V }

  predicate Tuple<T, U, V>(t: T, u: U, v: V) { (t, u, v) is (T, U, V) }

  predicate TupleAccess0<T, U, V>(tup: (T, U, V)) { tup.0 is T }

  predicate TupleAccess1<T, U, V>(tup: (T, U, V)) { tup.1 is U }

  predicate TupleAccess2<T, U, V>(tup: (T, U, V)) { tup.2 is V }

Despite what the name suggests, x is not a mutable variable
x cannot be updated, it is just a name for the value of expr1
You can replace x with expr1 in expr2 without changing the value of the expression

Functions are first-class citizens

A function can be passed as an argument to a function
Type of a function
- If parameters have types X, Y, Z
- If return type is U
- The type of the function is (X, Y, Z) -> U

Functions as in-parameters

  function Apply(f: int -> int, n: int): int {
    f(n)
  }

Functions as out-parameters

  function ApplyPartial(f: int -> int -> int, n: int): int -> int {
    f(n)
  }

Recursive functions

A function definition can be recursive

  function Factorial(n: int): int {
    if n == 0 then 1 else n * Factorial(n - 1)
  }

New expression: anonymous functions and application

  predicate LambdaAbstraction<U, V>(expr: V) { ((x: U) => expr) is U -> V }

  predicate Application<U, V>(fun: U -> V, arg: U) { fun(arg) is V }

Algebraic datatypes

Algebraic datatypes are a staple of functional programming
As a first approximation, they are like an enumeration of possible values
Here, the datatype defines two values, Small and Large

  datatype Size =
    | Small
    | Large

Type and constructors

A datatype definition defines multiple things
- A type whose name is that of the datatype definition
- The possible values
- Constructors for such values (in this simple case, the constructor and the value cannot be distinguished)

  predicate Constructor() { Small is Size }

Equality

Simple datatypes support equality

  predicate Equality(a: Size, b: Size) { (a == b) is bool }

  predicate Disequality(a: Size, b: Size) { (a != b) is bool }

Pattern matching

Pattern matching allows you to consider the possible values of a datatype

  function SizeToOunces(s: Size): int {
    match s
    case Small => 4
    case Large => 8
  }

New expression: pattern matching

  predicate MatchExpression(s: Size) {
    (match s case Small => 4 case Large => 8) is int
  }

Parameterized constructors

Constructors can have parameters
Example
- Coffee is a constructor: it takes a value of type Size and produces a value of type Drink
- Coffee(Small) is a value

  datatype Drink =
    | Coffee(Size)
    | Tea(Size)
    | Water(Size)

Applying constructors

  predicate Constructor() { (Tea(Small)) is Drink }

Are constructors functions?
- No
- Coffee and Tea cannot be used without being fully applied

Matching constructors with parameters

  function GetCaffeine(d: Drink): int {
    match d
    case Coffee(s) => 5 * SizeToOunces(s)
    case Tea(s) => 7 * SizeToOunces(s)
    case Water(s) => 0
  }

Wild identifiers on arguments

When you don't need to use a value and don't want to name it

  function GetCaffeine(d: Drink): int {
    match d
    case Coffee(s) => 5 * SizeToOunces(s)
    case Tea(s) => 7 * SizeToOunces(s)
    case Water(_) => 0
  }

Wild identifiers on constructors

  function GetCaffeine(d: Drink): int {
    match d
    case Coffee(s) => 5 * SizeToOunces(s)
    case Tea(s) => 7 * SizeToOunces(s)
    case _ => 0
  }

Named parameters

Constructor parameters can be named

  datatype Drink =
    | Coffee(sz: Size)
    | Tea(sz: Size)
    | Water(sz: Size)

Discriminators and destructors

Discriminator: test if a value correspond to a specific constructor
Destructor: extract value for some constructor

  predicate Discriminator(d: Drink) { d.Coffee? is bool }

  predicate Destructor(d: Drink) { d.sz is Size }

Example with discriminators and destructors

  function GetCaffeine(d: Drink): int {
    if d.Coffee? then
      5 * SizeToOunces(d.sz)
    else if d.Tea? then
      7 * SizeToOunces(d.sz)
    else
      0
  }

Member declarations

Functions can be defined along with datatype
- That is, including constants and predicates
In this context, the datatype value can be referred to as this

  datatype Size =
    | Small
    | Large
  {

    predicate This() { this is Size }

  }

Example with member function

  datatype Size =
    | Small
    | Large
  {

    function ToOunces(): int {
      match this
      case Small => 4
      case Large => 8
    }

  }

Functional dot notation

You have functional programming with dot notation!
For OO experts: no late binding, no dynamic dispatch, it's just syntactic convenience

  predicate DotExpression(s: Size) { s.ToOunces is () -> int }

Records

Algebraic datatypes with a single constructor are also called records
The single constructor usually has the same name as the datatype, but you can also choose a different name

  datatype Complex = Complex(r: real, i: real)

Type operators

Datatypes can be parameterized with a type
That way, you can define collections that are oblivious to what they contain
List is a type operator: it takes a type as an argument and creates a new type

  datatype List<T> =
    | Nil
    | Cons(head: T, tail: List)

Polymorphism

Functions can also be parameterized
That way, you can not only define collections oblivious to what they contain
But also functions on them that are also oblivious
The parameters of a function can be typed with type parameters
Type parameters always appear before parameters (prenex polymorphism)
A parameterized type needs to be applied to a type argument

  function Len<T>(l: List<T>): nat {
    match l
    case Nil => 0
    case Cons(_, tail) => 1 + Len(tail)
  }

Type parameter inference

In most cases, Dafny can infer that the type should be

  function Len<T>(l: List): nat {
    match l
    case Nil => 0
    case Cons(_, tail) => 1 + Len(tail)
  }

Type characteristics

Sometimes, you want to constrain a type parameter
It is done with type characteristics (of which there are 4 in Dafny)
For example, you can demand that the type support equality

  function TestEquality<T(==)>(a: T, b: T): bool {
    a == b
  }

Collections

Dafny has 4 built-in immutable collections for programming
- Sequences (seq<T>)
- Sets (set<T> and iset<T>)
- Multisets (multiset<T>)
- Maps (map<K, V> and imap<K, V>)
Sets and maps come in two flavors: finite and possibly infinite
Sequences and multisets are always finite
The built-in type string is a type synonym for seq<char>
The contents of these collections may be mutable, but the collections themselves are not

Sequences

  predicate Empty<T>() { [] is seq<T> }
  predicate SequenceDisplay<T>(x: T, y: T, z: T) { [x, y, z] is seq<T> }
  predicate Equality<T(==)>(a: seq, b: seq) { (a == b) is bool }
  predicate Disequality<T(==)>(a: seq, b: seq) { (a != b) is bool }
  predicate ProperPrefix<T(==)>(a: seq, b: seq) { (a < b) is bool }
  predicate Prefix<T(==)>(a: seq, b: seq) { (a <= b) is bool }
  predicate Concatenation<T>(a: seq, b: seq) { (a + b) is seq<T> }
  predicate Membership<T(==)>(a: seq, e: T) { (e in a) is bool }
  predicate Absence<T(==)>(a: seq, e: T) { (e !in a) is bool }
  predicate Size<T>(a: seq) { |a| is int }
  predicate Indexing<T>(a: seq, k: int) { a[k] is T }
  predicate Update<T>(a: seq, k: int, e: T) { a[k := e] is seq<T> }
  predicate Slice<T>(a: seq, k: int, l: int) { a[k..l] is seq<T> }
  predicate Drop<T>(a: seq, k: int) { a[k..] is seq<T> }
  predicate Take<T>(a: seq, l: int) { a[..l] is seq<T> }

Strings

Strings are sequences of characters

  predicate Type(s: string) { s is seq<char> }

  predicate Display() { "Hello" is string }

Sets

  predicate EmptySet<T(==)>() { {} is set<T> }
  predicate SetDisplay<T(==)>(x: T, y: T, z: T) { {x, y, z} is set<T> }
  predicate Union<T(==)>(A: set<T>, B: set<T>) { (A + B) is set<T> }
  predicate Intersection<T(==)>(A: set<T>, B: set<T>) { (A * B) is set<T> }
  predicate AsymmetricDifference<T(==)>(A: set<T>, B: set<T>) { (A - B) is set<T> }
  predicate Equality<T(==)>(A: set<T>, B: set<T>) { (A == B) is bool }
  predicate Disequality<T(==)>(A: set<T>, B: set<T>) { (A != B) is bool }
  predicate Subset<T(==)>(A: set<T>, B: set<T>) { (A <= B) is bool }
  predicate StrictSubset<T(==)>(A: set<T>, B: set<T>) { (A < B) is bool }
  predicate Superset<T(==)>(A: set<T>, B: set<T>) { (A >= B) is bool }
  predicate StrictSuperset<T(==)>(A: set<T>, B: set<T>) { (A > B) is bool }
  predicate Disjoint<T(==)>(A: set<T>, B: set<T>) { (A !! B) is bool }
  predicate Membership<T(==)>(e: T, A: set<T>) { (e in A) is bool }
  predicate Absence<T(==)>(e: T, A: set<T>) { (e !in A) is bool }
  predicate Cardinality<T(==)>(A: set<T>) { |A| is int }

Multisets

  predicate EmptyMultiset<T(==)>() { multiset{} is multiset<T> }
  predicate MultisetDisplay<T(==)>(x: T, y: T, z: T) { multiset{x, y, z} is multiset<T> }
  predicate Union<T(==)>(A: multiset<T>, B: multiset<T>) { (A + B) is multiset<T> }
  predicate Intersection<T(==)>(A: multiset<T>, B: multiset<T>) { (A * B) is multiset<T> }
  predicate Difference<T(==)>(A: multiset<T>, B: multiset<T>) { (A - B) is multiset<T> }
  predicate Equality<T(==)>(A: multiset<T>, B: multiset<T>) { (A == B) is bool }
  predicate Disequality<T(==)>(A: multiset<T>, B: multiset<T>) { (A != B) is bool }
  predicate Submultiset<T(==)>(A: multiset<T>, B: multiset<T>) { (A <= B) is bool }
  predicate StrictSubmultiset<T(==)>(A: multiset<T>, B: multiset<T>) { (A < B) is bool }
  predicate Supermultiset<T(==)>(A: multiset<T>, B: multiset<T>) { (A >= B) is bool }
  predicate StrictSupermultiset<T(==)>(A: multiset<T>, B: multiset<T>) { (A > B) is bool }
  predicate Disjoint<T(==)>(A: multiset<T>, B: multiset<T>) { (A !! B) is bool }
  predicate Membership<T(==)>(e: T, A: multiset<T>) { (e in A) is bool }
  predicate Absence<T(==)>(e: T, A: multiset<T>) { (e !in A) is bool }
  predicate Cardinality<T(==)>(A: multiset<T>) { |A| is int }
  predicate Multiplicity<T(==)>(e: T, A: multiset<T>) { A[e] is int }
  predicate MultiplicityUpdate<T(==)>(e: T, A: multiset<T>, k: int) { A[e := k] is multiset<T> }

Maps

  predicate Empty<U(==), V>() { map[] is map<U, V> }
  predicate Display() { map[20 := true, 3 := false, 20 := false] is map<int,bool>}
  predicate KeyMembership<U(==), V>(m: map, k: U) { (k in m) is bool }
  predicate KeyAbsence<U(==), V>(m: map, k: U) { (k !in m) is bool }
  predicate Cardinality<U(==), V>(m: map) { |m| is int }
  predicate Indexing<U(==), V>(m: map, k: U) { m[k] is V}
  predicate Update<U(==), V>(m: map, k: U, v: V) { m[k := v] is map}
  predicate Keys<U(==), V>(m: map) { m.Keys is set<U> }
  predicate Values<U(==), V(==)>(m: map) { m.Values is set<V> }
  predicate Items<U(==), V(==)>(m: map) { m.Items is set<(U, V)> }
  predicate Merge<U(==), V>(m1: map, m2: map) { (m1 + m2) is map }
  predicate MapDomainSubtraction<U(==), V>(m: map, s: set) { (m - s) is map }

Type synonyms

  type Complex = (real, real)