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
.
multiplyByTwo (n : Nat) : Nat := 2 * n;
Default Values¶
We can assign default values to function arguments. This feature allows a function to operate without explicit argument values by using the provided defaults.
To specify a default value for an argument, use the :=
operator followed by
the desired value. In the following example, x
and y
are given default
values of 0
and 1
, respectively:
f {x : Nat := 0} {y : Nat := 1} : Nat := x + y;
When calling this function without providing values for x
and y
, such as
f
, the function will use the default values and return 1
.
Note
Here are some key points to remember about using default argument values in Juvix:

No Referencing Previous Arguments: Default values cannot refer to previous arguments. Therefore, the following code would result in a scope error:
f {n : Nat := 0} {m : Nat := n + 1} ....

FunctionSpecific Feature: Only functions can have default values. Other constructs or types do not support this feature.

LeftHand Side Limitation: Only arguments on the lefthand side (LHS) of the
:
can have default values. The following syntax is invalid:f : {n : Nat := 0} := ...
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:
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>
 <pat11> <pat12> := <body1>
 ...
 <patn1> <patn2> := <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,
add (n : Nat) : Nat > Nat
 zero := n
 (suc m) := suc (add n m);
is equivalent to
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.
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
.
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 forwardreferenced 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:
odd : Nat > Bool :=
\ {
 zero := false
 (suc n) := even n
};
even : Nat > Bool :=
\ {
 zero := true
 (suc n) := odd n
};