# Type of a return satement

I'm creating a experimental toy language for my own education purposes (an impure typed Lisp based on Clojure - https://github.com/mikera/kiss)

I think I understand the concept of each expression in the language having a return type.

However some expressions may contain flow control statements that mean that the expression will not return normally, e.g.

• An early function return
• A break within a loop
• A continue / recur within a loop
• A goto (the horror...)

I'm not sure how to represent these in my type system. Should such things alter the type of the expression? Or should I have a parallel mechanism that enumerates alternative ways the expression may be exited?

• Have you looked at a book on type systems, such as Pierce's Types and Programming Languages, or Harpers? – Dave Clarke May 10 '14 at 17:36
• Not yet - thanks for the recommendation though! – mikera May 10 '14 at 17:44
• I implemented a break statement for Rich Hickey's predecessor language DotLisp using just an internal type, but that's just for an interpreter. – Mark Hurd May 18 '14 at 7:51

There is hardly a good reason to give a return expression a type.

In Benjamin Pierce's book, Types and Programming Languages, he mentions a similar situation: the type of throw expressions. Like return, a throw expression will not produce a value and instead changes the flow of control.

Pierce's comment is that if such expressions is to be given a type at all, a logical choice is ⊥, the "bottom" type. The bottom type is a type, but one which is impossible to instantiate. There are no objects of type ⊥.

This makes perfect sense for expressions that redirect flow in a program. They don't produce a value at all. So to denote this, we say their type is this "uninhabited" ⊥ type. If they did return a value, this would violate the one and only property of ⊥: that there are no values. We would have done the impossible.

If you come from an object oriented background, you might like to think about ⊥ as the "dual" of the Object type. (We sometimes call Object by the name ⊤ in computer science). In a subtype hierarchy, every type is a subtype of ⊤. Dually, ⊥ is a subtype of every other type. This means if I had a value of type ⊥, I can up-cast it

The type system in most programming language only tracks the type of values. A type system assigns types to a program; if the desired output from the type system is to characterize values, then the type system must assign types to the language constructs that produce value, i.e. expressions.

For example, in such a type system, the basic rule for function application (with a single argument, no subtyping or other subtlety) is $$\dfrac{F : T_1 \rightarrow T_2 \qquad A : T_1} {F(A) : T_2}$$ meaning that if $F$ is an expression that returns a function that returns a value of type $T_2$ when passed an argument of type $T_1$, and $A$ is an expression that returns a value of type $T_1$, then $F(A)$ is an expression that returns a value of type $T_2$.

With such a type system, only things that have a value have a type. So an expression like x + 1 has a type, but a statement like return x + 1; or break; doesn't have a type. For an instruction sequence like { foo(); bar(); }, the type system only cares that each expression that makes up a simple statement is well-typed. All the return statements in a function must be applied to an expression whose type matches the function's return type, but it's the expression that gets assigned a type, not the return statement.

Type systems can track other aspects. For example, a type system can track flow control. This is not very in programming languages but common in static analysis systems. One limited but well-known example is Java: in Java, the type system keeps track of which exceptions a piece of code can raise. This needs to be tracked not only in expressions, but also in statements. For expressions, the type system tracks both the type of the value and the set of possible raised exceptions; for statements, the type system tracks the set of possible raised exceptions. The type of functions must track the set of exceptions that the function may raise. A simplified rule for function application looks like this: $$\dfrac{F : T_1 \rightarrow^{S_2} T_2 \uparrow S_0 \qquad A : T_1 \uparrow S_1} {F(A) : T_2 \uparrow S_0 \cup S_1 \cup S_2}$$ where $A : T \uparrow S$ means that $A$ is an expression that either returns a value of type $S$ or raises an exception in the set $S$, and $T_1 \rightarrow^{S_2} T_2$ is the type of a function that takes an argument of type $T_1$ and either returns an argument of type $T_2$ or raises an exception in the set $S_2$. In such a type system, statements have exception sets but no value types. Here are rules to type-check a simple statement and sequential composition: $$\dfrac{A : T \uparrow S} {A; \uparrow S} \qquad \dfrac{I_1 \uparrow S_1 \qquad I_2 \uparrow S_2} {I_1; I_2 \uparrow S_1 \cup S_2}$$

Tracking local flow control is rare for type systems provided with compilers. (Compilers do flow control analysis internally as part of optimization and machine code generation, of course, but programs are not rejected at that stage, so this is rarely modeled as a type system.) It is more common in systems for slow (if not non-terminating) static analysis that attempt to prove properties such as termination, bounds checking, etc.

A type system can track model local flow control by tracking the continuations for a statement, i.e. what happens next. Unless you're willing to stick to sufficiently restricted (non-Turing complete languages), or to have a non-decidable type system, the type system will have to over-approximate and thus track possible continuations, i.e. what cannot be ruled out to happen next. For example:

• If $A$ is an expression without side effects, its only possible continuation is local return (i.e. the expression is evaluated and its context gets to use the resulting value).
• If $A$ is guaranteed not to terminate, then local return is not a possible continuation.
• The possible continuations of foo; bar are:
• the continuations of foo other than local return
• the continuations of bar, if local return is a possible continuation of foo
• The possible continuations of if condition then foo else bar are the possible continuations of foo or bar.
• The continuation of a return statement is the context of the function call.
• The continuation of break is the context of the enclosing loop.
• The continuation of continue is the context at the loop body start.
• The continuation of a goto is the context of the target label.

This type system would have judgements of the form $A : T \rightsquigarrow C$ and $I \rightsquigarrow C$ where $A$ is an expression, $I$ is a statement and $C$ is a set of continuations.