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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
