Function Declarations in Juvix¶

In Juvix, a function declaration is composed of a type signature and the body of the function. The type signature specifies the types of the arguments and the return type of the function. Constants are considered as functions with no arguments. The body of a function can either be a single expression or a set of function clauses when pattern matching is employed.

Syntax of Function Declarations¶

The syntax for a function declaration has the following form:

<funName> : <argType> -> <returnType> := <body>;

Function declarations in Juvix can have variations related to named and implicit arguments.

Named Arguments¶

A named argument is an argument whose name is specified in the function type signature before the colon. This name is then available within the scope of the function's body.

<funName> (<argName> : <argType>) : <returnType> := <body>;

For example, consider the function multiplyByTwo which takes a Nat (natural number) and returns a Nat. The argument is named n and is used in the function's body to return 2 * n.

  import Stdlib.Data.Nat open using {Nat; *};

  multiplyByTwo (n : Nat) : Nat := 2 * n;

Pattern Matching in Function Declarations¶

A function may consist of one or more function clauses instead of a single expression. This is applicable when the function's argument is a data type and we want to pattern match on that argument.

The syntax for a function declaration using pattern matching is as follows:

<funName> : <argType> -> <returnType>
    | <pat1> := <body1>
    | ...
    | <patN> := <bodyN>;

Here <pat1> through <patN> are patterns that are matched against the argument of the function. The corresponding body is evaluated when the pattern matches.

For instance, consider the following function with two clauses:

  import Stdlib.Data.Bool open;

  neg : Bool -> Bool
    | true := false
    | false := true;

When neg is called with true, the first clause is used and the function returns false. Similarly, when neg is called with false, the second clause is used and the function returns true.

Note that one may pattern match multiple arguments at once. The syntax in case of two arguments is as follows and can be extended to more arguments.

<funName> : <argType1> -> <argType2> -> <returnType>
    | <pat-1-1> <pat-1-2> := <body1>
    | ...
    | <pat-n-1> <pat-n-2> := <bodyN>;

Note

Initial function arguments that match variables or wildcards in all clauses can be moved to the left of the colon in the function definition. For example,

  import Stdlib.Data.Nat open;

  add (n : Nat) : Nat -> Nat
    | zero := n
    | (suc m) := suc (add n m);

is equivalent to

  import Stdlib.Data.Nat open;

  add : Nat -> Nat -> Nat
    | n zero := n
    | n (suc m) := suc (add n m);

If there is only one clause without any patterns, the pipe | must be omitted as we see earlier.

  import Stdlib.Data.Nat open;

  multiplyByTwo (n : Nat) : Nat := n;

Mutually Recursive Functions¶

Functions in Juvix can depend on each other recursively. In the following example, a function checks if a number is even by calling another function that verifies if the number is odd.

  import Stdlib.Data.Nat open;
  import Stdlib.Data.Bool open;

  import Stdlib.Prelude open;

  odd : Nat -> Bool
    | zero := false
    | (suc n) := even n;

  even : Nat -> Bool
    | zero := true
    | (suc n) := odd n;

Identifiers don't need to be defined before they are used, allowing for mutually recursive functions/types without any special syntax. However, exceptions exist. A symbol f cannot be forward-referenced in a statement s if a local module, import statement, or open statement exists between s and the definition of f.

Anonymous Functions (Lambdas)¶

Anonymous functions or lambdas can be defined using the following syntax:

Syntax of `lambda` declarations¶

\{ | pat1 .. patN_1 := clause1
   | ..
   | pat1 .. patN_M := clauseM }

The initial pipe | is optional. You can use either \ or the Unicode alternative λ to denote an anonymous function.

An anonymous function lists all clauses of a function without naming it. Any function declaration can be converted to use anonymous functions:

  import Stdlib.Prelude open;

  odd : Nat -> Bool :=
    \ {
      | zero := false
      | (suc n) := even n
    };

  even : Nat -> Bool :=
    \ {
      | zero := true
      | (suc n) := odd n
    };