identity functions are type declarations

Good afternoon. My name is Timur and I am a programmer.

Recently I finished one feature related to chromium (I forwarded disk_cache to webextensions api, this gives direct access to both http cache and code cache and many others – the first step to antidetect browser), but before writing an article on this topic I decided to take a break and cool my brain a little. Usually in such situations I arrange an audit of my notes, argue with myself from the past, sometimes I defeat him sometimes he defeats me, below is one of such etudes, I suggest we discuss it.

Let's talk about identity functions. Yes, that's right, plural.

Here is a definition of a function that will be familiar to anyone who has even briefly touched on functional programming:

id a = a

Here everything is clear: what we received at the input is what we gave. This is a polymorphic identity function. OK. But what if we want to define an identity function only for arguments of a certain type? In languages ​​with a nominative type system, it might look something like this:

id :: examinedType -> examinedType;
id a = a

But let's not rush to introduce any additional syntax for describing types. Let's just follow the code and see where it leads us.

For example, we want to write an id function for natural numbers, let's call it nat. What might it look like?

nat O = O
nat (S .n) = S (nat .n)

No surprises yet. But what can we tell from looking at this feature?
First, we can infer the type of the input parameter: someInferedTypeName: O | (S someInferedTypeName)
Moreover, we can deduce this not only by eye, it can be done programmatically. Unlike the execution of a function call on an argument, where we would go from left to right along the function clauses, we will go from right to left and from the end. We see the basis of induction:

nat O = O

and we understand that O is a terminal case. Thus, on the right we see the end of the function and on the left – the input parameter that will lead to this. We remember the input parameter – O and by the same clause we understand that this is part of the nat type (this statement is always true for identity functions, this is their advantage – ease of analysis)

Next we look at the inductive step:

nat (S .n) = S (nat .n)

from which (on the right) we deduce the result type:

S (что то, что возвращает nat .n)

and on the left we see what can lead to this – S .n where .n is nat (and we already know that O is nat). From the same clause we understand that (S nat) is also nat. We have no other clauses and we are ready to deduce the argument type:

nat = O | (S nat)
// или в нотации Coq:
Inductive nat : Set :=
  | O : nat
  | S : nat -> nat.

What happened here?
It is obvious that we took an easy-to-analyze function and deduced the type of the argument (which is the same as the type of the result).

Yes, we can say that, but saying that doesn't get us very far in our thinking. Let's describe what happened differently. Let's say that we expressed the type by selecting an identity function for it (easy to analyze). It sounds almost the same, but we are saying completely different things.

We say that for some set of types we can select identity functions such that by looking at each of these functions we can deduce its type. What does this mean? It means that some set of types can be described by functions, namely identity functions. That is, a function can be a type description language.

We need to know how to describe a type to express it through a function. To make it clear what we are talking about, let's look at a couple of examples.

For example, the type of prime numbers – can we express it through the identity function? Yes, we can. We write code that checks the number for primality and if it is prime – we return its value. At the same time, there is simply no branch in the code that handles the situation if the number is not prime. That's it, such a function will be an identity function for the type of prime numbers. How easy it will be to analyze is a question we will return to later. How effective it will be in execution in this context is not important at all. That is, we do not know the formula for prime numbers (yes, we have the Matiyasevich polynomial, good luck with its application), but we can determine whether a number belongs to this set – that's it, we have an identity type.

Now let's imagine a type – Diophatian equations. Can we express it? Easy. Can we write an identity function for such a type? Yes, moreover – it will be easy enough to analyze. But as soon as we try to specify our type and, say, express the type of Diophatian equations solvable in rational integers – we encounter Gilbert's tenth problem. That is, we can describe in words what type we want, but we cannot always express it as a function. Why is this so – an interesting question in itself, but this is a separate article.

At this stage, it is important to understand that we can consider the identity of the function as a way of describing a type. If the type of the definition domain of a regular function may differ from the type of the value domain, then for the identity function they coincide, which makes them convenient for describing types.

The second interesting property of identity functions is that we can always select a code that will programmatically easily determine that it is an identity function. No matter how complex the check for the argument's type, the identity function code can always be reduced to code of this type:

Definition SomeIdentityFunc (n) :=
  match (some_check n) with
  | true => n
  end.

Regardless of the complexity of some_check logic, we can (including programmatically) understand that SomeIdentityFunc is an identity function for some data type. That is, it will return n if n belongs to some type and is not defined for other types.

It is important to understand here that we are not talking about the fact that we can analyze any identity function, but about the fact that for any type that we can describe, we can find a variant of the identity function that is easy to recognize.

To summarize the above – instead of the paradigm of defining the type of a function (or function arguments), we shift to the paradigm – a function is a description of a type.

Dependent&refined types are just the implementation of this paradigm at a minimum.

With this paradigm it becomes more interesting to look at the proof of Turing and the Curry–Howard correspondence. No blowing of the veil, revelations and so on, everything is good and in its place, just looking at these things with the understanding that it is not the type that determines the function but the function that determines the type makes some moments more understandable and some – simply obvious. But more on that next time.

That's actually all I wanted to say today.

And there is no more news for today. It was Timur with you, good mood to everyone!