1 Feb
2010
1 Feb
'10
2:39 p.m.
And I'm pretty sure that there's no way to convince Agda that F = R, or something similar, because, despite the fact that Agda has injective type constructors like GHC (R x = R y => x = y), it doesn't let you make the inference R Unit = F Unit => R = F. Of course, in Agda, one could arguably say that it's true, because Agda has no type case, so there's (I'm pretty sure) no way to write an F such that R T = F T, but R U /= F U, for some U /= T.
It's easy to construct an F that is different from R but agrees with R for the case of Unit: F = λ _ -> R Unit So there's a good reason why Agda doesn't let F and R unify: it would really be completely wrong. Stefan