![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
theorems for free, polymorphic equality
Aug. 7th, 2016 04:15 pmCan someone walk me through the first paragraph of the section on polymorphic equality?
The programming language Miranda provides a polymorphic equality function, with type:
Applying parametricity to the type of (=) yields, for all a : A → A'
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".
(=): ∀ 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).
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".
