Re: Rigid skolem type variable escaping scope
Matthew Steele <mdsteele <at> alum.mit.edu>
2012-08-24 09:39:37 GMT
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 ins
tantiating too early.
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).