3.1. Defining Functions

Felix supports three syntactic forms for definining functions. The simplest form is illustrated by:

  fun f[t] (x:t, y:int): int * t => y,x;

You will note this function is polymorphic with one type argument t, it accepts a single argument of tuple type t * int, and returns a tuple of type int * t. The return type can be omitted in this case because it can be deduced:

  fun f[t] (x:t, y:int)=> y,x;

In this form, the function body is just an expression whose elaboration yields the value returned by the function.

The second form allows procedural code in a function, provided its side effects are limited to the scope of the function, so that the function itself has no side effects:

  fun f[t] (x:t, y:int): int * t =
  {
    var z = y;
    z++;
    return z,x;
  }

In this form, the returned value is the argument of the first return statement elaborated by the flow of control. Again, the return type can be omitted if the function type can be deduced. This is the most general form, the first form is just synactic sugar for

  fun f[t] (x:t, y:int): int * t =
  {
    return y,x;
  }

saving a few keystrokes, but greatly simplifying code layout, and improving the ability of the programmer to reason that the function has no side effects.

This form supports an extension to curry form:

  fun f[t] (x:t) (y:int): int * t =
  {
    return y,x;
  }

which is short hand for

  fun f[t] (x:t): int -> int * t =
  {
    fun g(y:int): int * t =
    {
      return y,x;
    }
    return g;
  }

Similarly, the first form also supports this extension.

The final form is

  fun f: u -> int  =
    | Empty => 0
    | Cons (_,?tail) => 1 + f tail
  ;

which is short hand for:

  fun f(x:u):int =
    match x with
    | Empty => 0
    | Cons (_,?tail) => 1 + f tail
    endmatch
  ;

All these forms can be used anonymously wherever a function closure is required, by simply enclosing them in parentheses and omitting the function name:

  print$ (fun f[t] (x:t, y:int)=> y,x) (1,2);

This is called the lambda form of the function, such lambda forms are first class expressions.

Two special cases of the lambda forms can be used for functions:

  { x }

is a function with unit argument, returning value x, and is short hand for:

  (fun()=>x)

and

  { var y = x; ++x; return x; }

is short hand for

  (fun () = { var y = x; ++x; return x; })

You should note very carefully the following are NOT equivalent:

  fun f()=>x;
  val f = { x };

The first line defines a function f, but does not form a closure. The second line stores a closure of an anonymous function into value f. Although any application of either f is equivalent, the lookup rules for variable and function names are distinct. Function names can be overloaded, and lookup choses the right function to use in an application based on the function argument.

Variable names, even if used applicatively, do not participate in overload resolution.

Felix also allows functions to provide pre-conditions and post-conditions. Here is an example:

  fun f(x: int, y:int when x+y>0): int expect result > 0 =
  {
    return x + y;
  }

The special identifier result is used to denote the value returned by the function. Pre and post conditions are part of the intuitive function type, but they are not part of the formal type. Instead, pre and post conditions are checked prior to and after function application, respectively, and abort the program if the conditions are not met.

3.1.1. Lazy value Types

A lazy value type is a function type with the domain 0 or void. A value of such a type can be constructed and used with syntax like:

   var y = 1.0;
   fun x = sin y;
   print x; endl;
   var y = 0.5;
   print x; endl;

The function x is semantically equivalent to a function taking unit argument, however each reference to x is automatically applied to the unit value () wherever it is written. In effect, such a function looks like a value whose body is substituted for each reference to it. This is also how it is implemented. In particular in the example, the output will be the value sin 1.0 and sin 0.5.