18
$\begingroup$

I am new to programming language theory. I was watching some online lectures in which the instructor claimed that a function with polymorphic type forall t: Type, t->t be the identity, but did not explain why. Can someone explain to me why? Maybe a proof of the claim from first principles.

$\endgroup$
  • 3
    $\begingroup$ I thought this question must be a duplicate, but I can't find it. cs.stackexchange.com/questions/341/… is a kind of follow-up. The standard reference is Theorems for free! by Phil Wadler. $\endgroup$ – Gilles 'SO- stop being evil' Oct 17 '17 at 21:21
  • 1
    $\begingroup$ Try to construct a generic function with this type that does anything else. You'll find that there is none. $\endgroup$ – Bergi Oct 17 '17 at 22:36
  • $\begingroup$ @Bergi Yes I was unable to find any counter example, but still was not sure how to prove it. $\endgroup$ – abhishek Oct 18 '17 at 9:36
  • $\begingroup$ But what were your observations when you tried to find one? Why did any attempts you made not work? $\endgroup$ – Bergi Oct 18 '17 at 12:09
  • $\begingroup$ @Gilles Maybe you remember cs.stackexchange.com/q/19430/14663? $\endgroup$ – Bergi Oct 18 '17 at 12:13
32
$\begingroup$

The first thing to note is that this isn't necessarily true. For example, depending on the language a function with that type, besides being the identity function, could: 1) loop forever, 2) mutate some state, 3) return null, 4) throw an exception, 5) perform some I/O, 6) fork a thread to do something else, 7) do call/cc shenanigans, 8) use something like Java's Object.hashCode, 9) use reflection to determine if the type is an integer and increment it if so, 10) use reflection to analyze the call stack and do something based on the context within which it is called, 11) probably many other things and certainly arbitrary combinations of the above.

So the property that leads to this, parametricity, is a property of the language as a whole and there are stronger and weaker variations of it. For many of the formal calculi studied in type theory, none of the above behaviors can occur. For example, for System F/the pure polymorphic lambda calculus, where parametricity was first studied, none of the above behaviors above can occur. It simply doesn't have exceptions, mutable state, null, call/cc, I/O, reflection, and it's strongly normalizing so it can't loop forever. As Gilles mentioned in a comment, the paper Theorems for free! by Phil Wadler is a good introduction to this topic and its references will go further into the theory, specifically the technique of logical relations. That link also lists some other papers by Wadler on the topic of parametricity.

Since parametricity is a property of the language, to prove it requires first formally articulating the language and then a relatively complicated argument. The informal argument for this particular case assuming we're in the polymorphic lambda calculus is that since we know nothing about t we can't perform any operations on the input (e.g. we can't increment it because we don't know if it is a number) or create a value of that type (for all we know t=Void, a type with no values at all). The only way to produce a value of type t is to return the one that is given to us. No other behaviors are possible. One way to see that is to use strong normalization and show that there is only one normal form term of this type.

$\endgroup$
  • 1
    $\begingroup$ How did System F avoid infinite loops that the type system can't detect? That's classified as unsolvable in the general case. $\endgroup$ – Joshua Oct 18 '17 at 21:00
  • 2
    $\begingroup$ @Joshua - the standard impossibility proof for the halting problem starts with the assumption that there is an infinite loop in the first place. So invoking it to question why System F doesn't have infinite loops is circular reasoning. More broadly, System F isn't nearly Turing complete, so I doubt it satisfies any of the assumptions of that proof. It's easily weak enough for a computer to prove that all of its programs terminate (no recursion, no while loops, only very weak for loops, etc.). $\endgroup$ – Jonathan Cast Oct 19 '17 at 13:31
  • $\begingroup$ @Joshua: it's unsolvable in the general case, which does not preclude solving it in many special cases. In particular, every program that happens to be a well-typed system F term has been proven to halt: there is one uniform proof that works for all these programs. Obviously, this means there are other programs, which cannot be typed in system F... $\endgroup$ – cody Sep 17 '18 at 22:26
15
$\begingroup$

The proof of the claim is quite complex, but if that's what you really want, you can check out Reynolds' original paper on the topic.

The key idea is that it holds for parametrically polymorphic functions, where the body of a polymorphic function is the same for all monomorphic instantiations of the function. In such a system, no assumptions can be made about the type of a parameter of polymorphic type, and if the only value in scope has a generic type, there's nothing to do with it but return it, or pass it to other functions you've defined, that can in turn do nothing but return it or pass it.. .etc. So in the end, all you can do is some chain of identity functions before returning the parameter.

$\endgroup$
8
$\begingroup$

With all the caveats that Derek mentions, and ignoring paradoxes that result from using set theory, let me sketch a proof in the spirit of Reynolds/Wadler.

A function of the type:

f :: forall t . t -> t

is a family of functions $f_t$ indexed by type $t$.

The idea is that, to formally define polymorphic functions, we should not treat types as sets of values, but rather as relations. Basic types, like Int induce equality relations--e.g., two Int values are related if they are equal. Functions are related if they map related values to related values. The interesting case is polymorphic functions. They map related types to related values.

In our case, we want to establish a relation between two polymorphic functions $f$ and $g$ of the type:

forall t . t -> t

Suppose that type $s$ is related to type $t$. The first function $f$ maps type $s$ to a value--here, the value itself is a function $f_s$ of the type $s \to s$. The second function maps type $t$ to another value $g_t$ of the type $t \to t$. We say that $f$ is related to $g$ if the values $f_s$ and $g_t$ are related. Since these values are themselves functions, they are related if they map related values to related values.

The crucial step is to use the Reynolds' parametricity theorem, which says that any term is in a relation with itself. In our case, the function f is related to itself. In other words, if s is related to t, $f_s$ is also related to $f_t$.

We can now pick any relation between any two types and apply this theorem. Let's pick the first type as the unit type (), which has only one value, also called (). We'll keep the second type t arbitrary but non-empty. Let's pick a relation between () and t to be simply one pair ((), c), where c is some value of the type t (a relation is just a subset of the cartesian product of sets). Parametricity theorem tells us that $f_{(\,)}$ must be related to $f_t$. They must map related values to related values. The first function $f_{(\,)}$ doesn't have much choice, it must map the only value () back to (). Therefore the second function $f_t$ must map c to c (the only values related to ()). Since c is completely arbitrary, we conclude that $f_t$ is $id_t$ and, since t is completely arbitrary, f is id.

You can find more details in my blog.

$\endgroup$
-2
$\begingroup$

EDIT: A comment above has provided the missing piece. Some people are deliberately playing with less-than-turing-complete languages. I explicitly don't care about such languages. A really usuable not-turing-complete language is a crazy hard thing to design. The whole rest of this expands on what happens trying to apply these theorems to a full language.

False!

function f(a): forall t: Type, t->t
    function g(a): forall t: Type, t->t
       return (a is g) ? f : a
    return a is f ? g : a

where the is operator compares two variables for reference identity. That is, they contain the same value. Not an equivalent value, same value. Functions f and g are equivalent by some definition but they aren't the same.

If this function is passed itself it returns something else; otherwise it returns its input. The something else has the same type as itself therefore it can be substituted. In other words, f is not the identity, because f(f) returns g, whereas the identity would return f.

For the theorem to hold it has to assume the ridiculous ability to reduce

function cantor(n, <z, a>) : forall t: t: Type int, <int, t> -> <int, t>
    return n > 1 ? cantor((n % 2 > 0) ? (n + 1) : n / 2, <z + 1, a>) : <z, a>
return cantor(1000, <0, a>)[1]¹

If you're willing to assume that you can assume the much easier type inference can be handled.

If we try to restrict the domain until the theorem holds we end up having to restrict it awfully far.

  • Pure Functional (no mutable state, no IO). OK I can live with that. A lot of time we want to run proofs over functions.
  • Empty standard library. meh.
  • No raise and no exit. Now we're starting to get constrained.
  • There is no bottom type.
  • The language has a rule that allows the compiler to collapse infinite recursion by assuming it must terminate. The compiler is allowed to reject trivial infinite recursion.
  • The compiler is allowed to fail if presented with something that can't be proved either way.² Now the standard library can't take functions as arguments. Boo.
  • There is no nil. This is starting to get problematic. We've ran out of ways to deal with 1/0.³
  • The language can't do branch type inferences and does not have an override for when the programmer can prove a type inference the language cant. This is pretty bad.

The existence of both of the last two constraints has crippled the language. While it is still Turing complete the only way to get general purpose work out of it is to simulate an inner platform that interprets a language with looser requirements.

¹ If you think the compiler can deduce that one, try this one

function fermat(z) : int -> int
    function pow(x, p)
        return p = 0 ? 1 : x * pow(x, p - 1)
    function f2(x, y, z) : int, int, int -> <int, int>
        left = pow(x, 5) + pow(y, 5)
        right = pow(z, 5)
        return left = right
            ? <x, y>
            : pow(x, 5) < right
                ? f2(x + 1, y, z)
                : pow(y, 5) < right
                    ? f2(2, y + 1, z)
                    : f2(2, 2, z + 1)
    return f2(2, 2, z)
function cantor(n, <z, a>) : forall t: t: Type int, <int, t> -> <int, t>
    return n > 1 ? cantor((n % 2 > 0) ? (n + 1) : n / 2, <z + 1, a>) : <z, a>
return cantor(fermat(3)[0], <0, a>)[1]

² The proof that the compiler can't do this depends on blinding. We can use multiple libraries to ensure the compiler can't see the loop at once. Also, we can always construct something where the program would work but could not be compiled because the compiler can't perform the induction in available memory.

³ Somebody thinks you can have this return nil without arbitrary generic types returning nil. This pays a nasty penalty for which I have seen no effective language that can pay it.

function f(a, b, c): t: Type: t[],int,int->t
    return a[b/c]

must not compile. The fundamental problem is runtime array indexing doesn't work anymore.

$\endgroup$
  • $\begingroup$ @Bergi: I constructed a counterexample. $\endgroup$ – Joshua Oct 18 '17 at 21:08
  • 1
    $\begingroup$ Please take a moment to reflect on the difference between your answer and the other two. Derek's opening sentence is “The first thing to note is that this isn't necessarily true”. And then he explains what properties of a language make it true. jmite also explains what makes it true. In contrast, your answer gives an example in an unspecified (and uncommon language) with zero explanation. (What is the foil quantifier anyway?) This is not helpful at all. $\endgroup$ – Gilles 'SO- stop being evil' Oct 18 '17 at 21:40
  • 1
    $\begingroup$ @D.W: if a is f then the type of a is the type of f which is also type of g and therefore the typecheck should pass. If a real compiler kicked it out I would use the runtime cast that real languages always have for the static type system getting it wrong and it would never fail at runtime. $\endgroup$ – Joshua Oct 18 '17 at 23:02
  • 2
    $\begingroup$ That's not how a static typechecker works. It doesn't check that the types match for a single specific input. There are specific type rules, which are intended to ensure that the function will typecheck on all possible inputs. If you require use of a typecast then this solution is much less interesting. Of course if you bypass the type system then the type of a function guarantees nothing -- no surprise there! $\endgroup$ – D.W. Oct 19 '17 at 5:25
  • 1
    $\begingroup$ @D.W.: You miss the point. There is enough information for the static type checker to prove the code is type safe if it had the wit to find it. $\endgroup$ – Joshua Oct 19 '17 at 17:13

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.