theorems for free, polymorphic equality
Can someone walk me through the first paragraph of the section on polymorphic equality?
The programming language Miranda provides a polymorphic equality function, with type:
(=): ∀ X, X → X → Bool
Applying parametricity to the type of (=) yields, for all a : A → A'
for all x, y ∈ A, (x =A y) = (a x =A' a y).This is obviously false
Then they also say "This is not a contradiction to the parametricity theorem".
Smells like bullshit. If the statement they've got is the result of applying parametricity, then it is a contradiction to the theorem. But also I have my doubts about how they have applied the theorem. Everywhere else there is no "=" between "(x =A y)" and what follows; only a "if...then".
The programming language Miranda provides a polymorphic equality function, with type:
(=): ∀ X, X → X → Bool
Applying parametricity to the type of (=) yields, for all a : A → A'
for all x, y ∈ A, (x =A y) = (a x =A' a y).This is obviously false
Then they also say "This is not a contradiction to the parametricity theorem".
Smells like bullshit. If the statement they've got is the result of applying parametricity, then it is a contradiction to the theorem. But also I have my doubts about how they have applied the theorem. Everywhere else there is no "=" between "(x =A y)" and what follows; only a "if...then".