LogoThe Eiffel Compiler / Interpreter (tecomp)


Ghost functions and higher order functions

Ghost functions

Boolean expressions of the form

  all(x:X) p(a,x)  -- x is a bound variable, a is free within the expression
  some(x:X) p(a,x)

are not computable in general, even if the boolean valued function "p" is computable. I.e. the following constructs are illegal in executable code.

  -- Illegal if expression!!!
  if all(x:X) p(a,x) 
  then exp1 
  else exp2 
  -- Illegal function definition!!!
  f_illegal(a:A): BOOLEAN
      Result = all(x:X) p(a,x)

The compiler cannot accept these constructs because it is unable to generate code to calculate the expression/function.

But a function like "f_illegal" could be very useful in assertions. Since there is no need to have runtime code for assertions, the fact that "f_illegal" is not computable does not disturb as long as it is a mathematically meaningful function.

In order to make this possible, Modern Eiffel has ghost types.

  T              -- a normal type
  ghost T        -- a ghost type

Objects of ghost type are called ghost objects. Ghost objects cannot flow into real computations. But it is possible to inject ghost objects into assertions.

A function which returns ghost objects is a ghost function. Ghost functions can only be used in assertions.

With this we can define a legal version of "f_illegal".

  f_legal(a:A): ghost BOOLEAN
      Result = all(x:X) p(a,x)

Ghost functions can be combined arbitrarly. I.e. "f_legal" is a valid definition, regardless whether "p" is a computable function or not.

Ghost functions are a powerful means to structure complicated assertions.

Functions as objects

Functions are objects and can be passed around arbitrarily. I.e. functions can be attached to local variables, passed as arguments and returned as results.

Function objects have a type. A function receiving as argument an object of type A and returning an object of type R has the type A->R.

  A->R           -- function taking one argument
  [A,B,...]->R   -- function taking many arguments
  []->R          -- function with no argument, i.e. constant function
  ghost(A->R)    -- a ghost function type
  A -> ghost R   -- the same ghost function type
  f:A->R         -- variable representing a function
  f[a]           -- function "f" evaluated with the argument "a"
  g:[A,B]->R     -- variable representing a function with two arguments
  g[a,b]         -- function "g" evalutated with the arguments "a" and "b"
  h:[A,B]->[R,T] -- variable representing a function with two argumens
                 -- returning two values

The function "g" is a function that maps a tuple of type [A,B] to R. But as described in the last post "Tuples and functions", sequences of expressions and tuples with matching types can be used interchangeably.

Therefore the function "g" can be called with "g[a,b]" as if it were a function with two arguments instead of "g[ [a,b] ]" which were necessary if Modern Eiffel would not have this conversion between sequences of expressions and tuple expressions.

The module "function"

The class FUNCTION

The type A->R inherits from the type FUNCTION[A,R]. The declaration of FUNCIONT[A,R] is contained within a module "function" and looks like

  -- file: function.e
  deferred class

The fact that the class FUNCTION has only two formal generics, one for the argument and one for the return type, is no restriction. A and R can be arbitrary tuples. Therefore any multiargument-multireturn function [A,B]->[R,T] can be represented as FUNCTION[ [A,B], [R,T] ].

Basic functions of the module "function"

The module "function" has the following basic functions

    is_defined(f:CURRENT, a:A): ghost BOOLEAN
        -- Is the function `f' defined at argument `a'?
      deferred end
    is_total(f:CURRENT): ghost BOOLEAN
        -- Is the function `f' defined for all arguments?
        Result = all(a:A) f.is_defined(a)
    [] (f:CURRENT, a:A): B
        -- Value of function `f' at argument `a'.

All functions in Modern Eiffel are potentially partial functions. The function "is_defined" represents the precondition of the function "f" and returns whether the function is defined at a certain argument.

The function "is_total" tells whether the function is defined for all possible arguments.

The function "[]" returns the value of the function at a certain argument.

Only the function "[]" can be called in computations. The functions "is_defined" and "is_total" are ghost functions and can be used only in assertions.

The operator "[]" stands for function application. The value of the function "f" at argument "a" is returned by "f[a]".

Note: We abandon the syntax of ISE Eiffel that all functions must have names and can have an optional operator alias. In the following we treat operators as first class feature names. I.e. the operator symbols "=", "<=", "/", "and", "not", "or", ... are valid feature names for functions with one argument (prefix operator) or two arguments (binary operator). The bracket operator "[]" can have an arbitrary number of arguments. This convention is essentially the same as the one used in the programming language Scala.

Equality of functions

Mathematically functions are sets of key-value pairs. Therefore we say the two functions "f" and "g" are equal if their sets of key-value pairs are equal.

Two sets "a" and "b" are equal if "a" is a subset of "b" and "b" is a subset of "a".

The following feature block in the module "function" codes these definitions into Modern Eiffel.

  feature  -- equality
    is_contained(f,g:CURRENT): ghost BOOLEAN
        Result = all(a:A) check
                   f.is_defined(a) => g.is_defined(a)
                   f.is_defined(a) => (f[a] = g[a])
    = (f,g:CURRENT): ghost BOOLEAN
        Result = (f.is_contained(g) and g.is_contained(a))
    is_strictly_contained(f,g:CURRENT): ghost BOOLEAN
        Result = (f.is_contained(g) and f/=g)

Properties of containment and equality

We expect containment to be reflexive, antisymmetric and transitive and equality to be reflexive, symmetric and transitive. I.e. we expect the following assertions to be true.

    all(f,g,h:CURRENT) check
      reflexive:     f.is_contained(f)
      antisymmetric: f.is_contained(g) => g.is_contained(f) => (f=g)
      transitive:    f.is_contained(g) 
                     => g.is_contained(h)
                     => f.is_contained(h)
      reflexive:     f=f
      symmetric:     (f=g) => (g=f)
      transitive:    (f=g) => (g=h) => (f=h)

The proof engine of Modern Eiffel is able to proof these properties automatically. The reader is encouraged to prove these assertions in order to see that the proofs are straighforward.

Parent class of FUNCTION

The above properties of "is_contained" and "=" satisfy the needed properties for the type "PARTIALLY_ORDERED". And indeed we can define the class FUNCTION in the following manner.

  deferred class
        is_less_equal as is_contained
        is_less       as is_strictly_contained

Note that the parent type PARTIALLY_COMPARABLE must be inherited as a ghost type because in the parent all functions are defined as computable functions. Inheriting as ghost converts all functions inherited from the parent to ghost functions.

This declaration of the class FUNCTION is highly recommendable because with PARTIALLY_ORDERED as parent the module "function" inherits all proved assertions of the parent class.

Creation of function objects

Convert functions into function objects

Any function can be converted to a function object. Having the function "func"


the following expressions are equivalent

  func(a,b)             -- call "func" directly
    f:[A,B]->R := func  -- create a function object and assign it to "f"
    f[a,b]              -- call the function object

Note: While named functions like "func" are called in the usual manner with parenthesized arguments, anonymous functions (i.e. function objects) are called with the arguments provided in brackets.

The possibility gets interesting if we start to pass around function objects.

  -- assume `gfunc' has the definition
  gfunc(f:[A,B]->R, x:X): T
  -- then the following expression is valid

Create function objects from expressions

Any expression can be used to create a function object. Suppose we have an expression "e" then "x->e" is a function which maps any argument to the value of "e" with "x" replaced by the argument, i.e. "(x->e)[y]=e[x:=y]".

  -- general rule
  x->e              (x->e)[y] = e[x:=y]
  -- some examples
  i->i+1            (i->i+1)[5] = 6
                    (i->i+1)[n+m] = (n+m)+1
  i->(i+j)/k        (i->(i+j)/k)[10] = (10+j)/k

In the expression "x->e" the variable "x" is a bound variable. It can be renamed arbitrarly (but consistently on the left and the right hand side of the arrow).

  (x->e)  =  (y->e[x:=y]) 
  (x->e)  =  (z->e[x:=z])

Some more possibilities to create function objects from expressions.

  x:X->e            -- explicitly typed argument
  [x,y,..]->e       -- multiargument function
  [x:X,y:Y,...]->e  -- multiargument function with explicitly typed arguments 
  -- call of the function
  [x,y]->e           ([x,y]->e)[a,b] = e[x,y:=a,b]

Preconditions of function objects

All functions are potentially partial, i.e. they can have preconditions. The preconditions are handed over to the function "is_defined" of the function object.

In the above example the function "func(a:A,b:B):R" has the precondition "pre(a,b)". Therefore in the corresponding function object "f" the expression "f.is_defined(a,b)" has the same value as "pre(a,b)".

The same applies to function objects created from expressions. Any expression "e" can have a set of preconditions "p1", "p2", ...

  e          -- an expression
  p1,p2,...  -- the precondition expressions of e
  (x->e).is_defined(y) = check (x->p1)[y], (x->p2)[y], ... end


  a/b        -- e.g. division of natural numbers
  b/=0       -- precondition of "a/b"
  b->a/b     -- function where the divisor is taken as the argument
  (b->a/b).is_defined(i) = (i/=0)

Emacs suffix

 Local Variables: 
 mode: outline
 coding: iso-latin-1
 outline-regexp: "=\\(=\\)*"
Table of contents

- Ghost functions

- Functions as objects

- The module "function"

- The class FUNCTION

- Basic functions of the module "function"

- Equality of functions

- Properties of containment and equality

- Parent class of FUNCTION

- Creation of function objects

- Convert functions into function objects

- Create function objects from expressions

- Preconditions of function objects

- Emacs suffix