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?

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

StackExchange Computer Science Q#24579, answer score: 4