On Aug 23, 2012, at 10:32 PM, wren ng thornton wrote:
> Now, be careful of something here. The reason this fails is because we're compiling Haskell to System Fc, which is a Church-style lambda calculus (i.e., it explicitly incorporates types into the term language). It is this fact of being Church-style which forces us to instantiate ifn before we can do case analysis on it. If, instead, we were compiling Haskell down to a Curry-style lambda calculus (i.e., pure lambda terms, with types as mere external annotations) then everything would work fine. In the Curry-style world we wouldn't need to instantiate ifn at a specific type before doing case analysis, so we don't have the problem of magicking up a type. And, by parametricity, the function fn can't do anything particular based on the type of its argument, so we don't have the problem of instantiating too early[1].
Okay, I think that's what I was looking for, and that makes perfect sense. Thank you!
> Of course, (strictly) Curry-style lambda calculi are undecidable after rank-2 polymorphism, and the decidability at rank-2 is pretty wonky. Hence the reason for preferring to compile down to a Church-style lambda calculus. There may be some intermediate style which admits your code and also admits the annotations needed for inference/checking, but I don't know that anyone's explored such a thing. Curry-style calculi tend to be understudied since they go undecidable much more quickly.
Gotcha. So if I'm understanding correctly, it sounds like the answer to one of my earlier questions is (very) roughly, "Yes, the original version of bar would be typesafe at runtime if the typechecker were magically able to allow it, but GHC doesn't allow it because trying to do so would get us into undecidability nastiness and isn't worth it." Which is sort of what I expected, but I couldn't figure out why; now I know.
I think now I will go refresh myself on System F (it's been a while) and read up on System Fc (which I wasn't previously aware of). (-:
Cheers,
-Matt