What is the difference between the semantic and syntactic views of function types?

Question

Edit: My original question referred to nonconstructive and constructive definitions of function types. I changed the terminology in the question and the title to semantic and syntactic, which the answer indicates is the correct terminology for this distinction.

I can recall two ways of defining functions in set theory and programming languages with set-theoretic foundations. The function type $\tau \to \sigma$ can be defined semantically as the set of all maps from $\tau$ to $\sigma \cup \{\bot\}$, i.e., all objects $f$ such that if $x \in \tau$ then $f(x) \in \sigma \cup \{\bot\}$. Alternatively, the function type $\tau \to \sigma$ can be defined syntactically as the set of all terms in a given language whose type is $\tau \to \sigma$ (possibly modulo some equivalence relationship). As a programmer, I work with the latter definition, but I often pretend that I'm working with the former definition.

What are the differences between the inhabitants of $\tau \to \sigma$ according to the two definitions above? For instance, are uncomputable functions included in the first but not the second definition?

To be precise, I'm interested in the situation where terms are strongly typed, functions are side effect free and may be nonterminating, and functions are equal iff, for all inputs, they both diverge or both return the same value.

Answer 1

These are not called constructive and nonconstructive! The one you call "nonconstructive" works just as well in constructive mathematics (you have to be a bit careful about how you define the $\bot$ value, but that is a technical detail).

Rather, you are asking about semantic and syntactic distinctions. We imagine that the expressions we write in a program correspond to abstract mathematical objects. For example, the syntactic expression (fun n => 2 + n) 2 denotes the number $4$. (Under this view "evaluating a program" is about finding out which abstract mathematical object it denotes.)

We can then ask what mathematical objects corresponding to expressions of type a -> b. Presumably they are actual mathematical functions (although that is not so clear in the presence of computational effects). But they are not all functions, because those functions that can be expressed in a programming language have special properties, such as:

1. they are Turing computable (because programming langauges can be interprted by Turing machiens).

2. they are continuous (because in finite time we can only get finite information about input, and continuity essentially says that only finite amount of input is required to produce a finite amount of output).

So, it may make sense to restrict to special kinds of mathematical functions (only computable ones, only continuous ones). This way our mathematical objects will correspond more closely to our programs, and so presumably we will have a better setup. (In fact, as soon as we have a language with recursion, we cannot think of expressions of type a -> b as just ordinary functions, but rather somehting like the continuous ones--but let me not go there just now.)

As you say, most programers take a syntactic view, in which functions are syntactic expressions. This is certainly a possibility that can go a long way. But the semantic view in which we think of programs as denoting mathematical objects has its benefits too. Mathematicians know an awful lot about computability and continuity, and you can bring the knowledge in when you take the semantic view.

A trivial application of the semantic method is this: suppose we want to implement comparison of functions eq : (nat -> nat) -> (nat -> nat) -> bool which tells us whether two functions f, g : nat -> nat are equal. How do we do it? The answer is that we cannot implement it because that would give us a discontinuous function. But proving this fact using only syntactic methods is much harder. In fact, I do not know how to do it without using some computability theory, which again is a semantic method. You may think it is obvious that eq cannot be implemented, in which case you should wonder why eq : (nat -> bool) -> (nat -> bool) -> bool can be implemented (and the implementation was first found using semantic methods).

Another area where the semantic view is needed is numerical computation. It is absurd to claim that a program (syntactic entity) for solving a differential equation has nothing to do with differential equations (semantic entity).

Let me also say what the constructive-nonconstructive distinction is. This is about the logic you use to do math. If we use nonconstructive logic, which is the traditional way to do it, then we will be able to prove that there exist non-computable functions. Consequently, there will be functions we cannot implement. But if we use constructive logic, then it is impossible to prove existence of a non-computable function. (In fact, we may add an axiom to constructive logic which says "all maps are computable", although I would advise against this: how do you know that all external input that is coming into your computer from the universe is computable?) This is not the traditional way, but it is one that programers can sympathize with.

Lastly, I want to nitpick about something your write in your title. Definitions are not constructive or non-constructive. They just are. Constructivity is important when we prove and construct things. Function types in a programming language are defined a la type theory in terms of:

• a type constructor, such as ->
• rules for forming terms, such as $\lambda$-abstraction
• rules for using terms, such as application
• equations which are supposed to hold, such as $\beta$-reduction.

This works equally well in constructive and non-constructive logic, because it is just syntax. There are meta-theorems which say that for finite discrete objects (syntax, natural numbers, finite graphs, lists, ...) there is no difference between constructive and non-constructive logic (I am skipping over a lot of details). But when you ask for the semantics of your type, i.e., what mathematical object it corresponds to, then it makes a difference.