4 votes
Accepted

Is Linear Evaluation Parametric?

Here's an Agda formalization of the non-linear version of your argument, and my comment above: ...
Dan Doel's user avatar
  • 931
3 votes

Efficient algorithm/ implementation to compute Transitive Closure of a Rule with respect to a Relationship

I give here an answer for a very specific subcase. We let $x \in A_1 \times \dots \times A_k$ be written $(x^1,\dots,x^k)$. When the rule $\sigma$ acts on each $A_i$ independently, in the same way, ...
Yann Strozecki's user avatar
2 votes
Accepted

Why Reflexive Graphs for Parametricity?

In the months since I asked this question, I think I have found a sensible answer. Often, the type of relations considered do not compose. For instance, if your notion of a relation $R : D \to E$ ...
Max New's user avatar
  • 1,675
1 vote

What is the relation of parametricity and function extensionality?

Indeed there is a similarity in these two definitions. Function extensionality that you showed is just a condition that specifies when two functions are equal. If we talk about logical relations then ...
winitzki's user avatar
  • 304

Only top scored, non community-wiki answers of a minimum length are eligible