mLite Guard Expressions

Guard expressions can be used to limit the set of arguments that will be accepted within a pattern. For example, the following function computes the square root of a number using Newton's algorithm:

fun sqrt (r, last) where (last = r) = r
       | (r, last) = sqrt ((r + x / r) / 2, r)

It uses the same pattern (a, b) two times, once with the guard where (last = r) and once without any guard. The guarded pattern is only selected if the constraint last = r is satisfied. Otherwise, the second case is used.

Function close over identifiers used in guard expressions, so higher-order functions may use free variables in guards:

fun filter pred =
  let fun filter2 ([], r)      = rev r
                | (x :: xs, r) where (pred x)
                               = filter2 (xs, x :: r)
                | (x :: xs, r) = filter2 (xs, r)
  in fn a = filter2 (a, [])
  end

Here filter2 closes over pred. So when the higher-order filter function is applied to a predicate, it creates a new function that uses the predicate in the guard pred x:

val extract_even = filter (fn x = x mod 2 = 0)

The above function extracts even numbers from a list of numbers:

extract_even [1,2,3,4,5,6,7]  ;; gives [2,4,6]

Implicit Guards

When a guard expression applies only to a single type, like in the above filter function, the guard expression can often be used in the place of the pattern. This is called in implicit guard. The mechanism is explained in detail in this paper (ps).

For instance, the signum function can be written in a very natural way using implicit guards:

fun sgn x < 0 = ~1
      | x > 0 =  1
      | _     =  0

In this function, the pattern x where x < 0 has been contracted to x < 0. Likewise, x where x > 0 became x > 0. The compiler separates the pattern from the implicit guard expression and rewrites it to a pattern and an (explicit) guard. The details are explained in the paper.

Even the above filter function can be rewritten using an implicit guard:

fun filter f =
  let fun filter2 ([], r)        = rev r
                | (f x :: xs, r) = filter2 (xs, x :: r)
                | (x :: xs, r)   = filter2 (xs, r)
  in fn a = filter2 (a, [])
  end

Because function application binds stronger than infix operators (:: in this case), the guard tests the first element x of the list x :: xs for the property f.

Limitations

Implicit guards cannot be used when a relation between different variables of the same pattern has to be expressed in a guard expression. This was the case, for example, in the initial sqrt example on this page. For these cases, mLite also offers explicit guard expressions introduced by where.