In example 2.2, to distinguish between an element and a function a better example is to consider a constant such as 7 can be an element of R or a constant function. With type theory notation, 1:R versus \x:R.1, another important point is that you have to specify the arity of the function, so that 1:R, \(x:R).1, \(x:R,y:R).1, \(x:C,y:C).1 are four different types, the first a constant, the second a constant function of one real variable, and the last a function of arity two whose variable type is the C the complex field.

I'm reading page four, perhaps type theory can distinguish among pure function, lazy functions, side-effect functions and other types of functions that are implemented by a procedure which can be lazy or not. So pi:R,(\x:R.pi) and (\x:Haskell-Action()).pi in which the last is a non pure lazy program for computing all digits of pi, are two different types, that is they belong to different universes.