2
$\begingroup$

I am reading Theorems for free! by Philip Wadler which is a paper about how to derive theorems from the type signature of a function.

Parametricity is just a reformulation of Reynolds’ abstraction theorem: terms evaluated in related environments yield related values.

What is an environment in this case ? More generally, how do I interpret the statement in bold ?

I think I understand the parametricity thing correctly but somehow I cannot map this sentence to something more intuitive.

$\endgroup$
  • $\begingroup$ I believe it's the same as contexts in typing judgements $\endgroup$ – xuq01 Jun 24 '18 at 11:24
  • $\begingroup$ Could you clarify your question? In a comment you mentioned you already know what an environment is, so I'm confused about what you are asking. $\endgroup$ – D.W. Jun 24 '18 at 17:56
  • 1
    $\begingroup$ @D.W. I think that environment refers to a context in typing judgement notation. But I was after the meaning of the sentence in bold. What I found so far: the Uniqueness property states that for any given context and expression there exist at most one type derived from the type judgement. So we know that in the same environment the same expression yields the same type. Now on the case of distinct terms evaluated in the same context: by manually testing on paper I couldn't create two expression of distinct types without altering the context; which might lead to the beginning of an answer. $\endgroup$ – user88487 Jun 24 '18 at 18:05
3
$\begingroup$

The environments are related not identical. The context of this statement is logical relations, as described e.g. here. A logical relation is a type-indexed family of relations which follows the structure of the types (in a way I won't elaborate on). If for each type $\tau$, we assign a (binary) relation $R[\tau]$, then given $f:\tau_1\to\tau_2,x:\tau_1\vdash f\, x : \tau_2$ when $R[\tau_1\to\tau_2](f,f')$ and $R[\tau_1](x,x')$ we can ask if it is the case that $R[\tau_2](f\, x,f'\, x')$. This is what it is referring to in "terms evaluated in related environments yield related result".

$\endgroup$

Your Answer

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