9.20 Exit

A function that does not return directly to its caller has Exit as its return type. The operation error is an example of one which does not return to its caller. Instead, it causes a return to top-level.

n := 0
\[\]
0

Type: NonNegativeInteger

The function gasp is given return type Exit since it is guaranteed never to return a value to its caller.

gasp(): Exit ==
    free n
    n := n + 1
    error "Oh no!"

Function declaration gasp : () -> Exit has been added to workspace.

Type: Void

The return type of half is determined by resolving the types of the two branches of the if.

half(k) ==
  if odd? k then gasp()
  else k quo 2

Because gasp has the return type Exit, the type of if in half is resolved to be Integer.

half 4
Compiling function gasp with type () -> Exit
Compiling function half with type PositiveInteger -> Integer
\[\]
2

Type: PositiveInteger

half 3
Error signalled from user code in function gasp:
   Oh no!
n
\[\]
1

Type: NonNegativeInteger

For functions which return no value at all, use Void. See ugUserPage in Section ugUserNumber and VoidXmpPage for more information.