[Haskell-cafe] Rigid skolem type variable escaping scope

[wren ng thornton]

On 8/22/12 5:23 PM, Matthew Steele wrote:
> So my next question is: why does unpacking the newtype via pattern matching suddenly limit it to a single monomorphic type?

Some Haskell code:

     foo :: (forall a. a -> Int) -> Bool
     foo fn = ...

     newtype IntFn a = IntFn (a -> Int)

     bar1 :: (forall a. IntFn a) -> Bool
     bar1 ifn = case ifn of IntFn fn -> foo fn

     bar2 :: (forall a. IntFn a) -> Bool
     bar2 ifn = foo (case ifn of IntFn fn -> fn)


Some (eta long) System Fc code it gets compiled down to:

     bar1 = \ (ifn :: forall a. IntFn a) ->
         let A = ??? in
         case ifn @A of
         IntFn (fn :: A -> Int) -> foo (/\B -> \(b::B) -> fn @B b)

     bar2 = \ (ifn :: forall a. IntFn a) ->
         foo (/\A -> \(a::A) ->
             case ifn @A of
             IntFn (fn :: A -> Int) -> fn a)

There are two problems with bar1. First, where do we magic up that type 
A from? We need some type A. We can't just pattern match on ifn--- 
because it's a function (from types to terms)! Second, if we instantiate 
ifn at A, then we have that fn is monomorphic at A. But that means fn 
isn't polymorphic, and so we can't pass it to foo.


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].

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.


[1] I think.

-- 
Live well,
~wren