On Wed, Aug 22, 2012 at 10:13 PM, Matthew Steele wrote:

On Aug 22, 2012, at 3:02 PM, Lauri Alanko wrote:

...

Quoting "Matthew Steele" :

...

{-# LANGUAGE Rank2Types #-}

class FooClass a where ...

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

...

newtype IntFn a = IntFn (a -> Int)

bar :: (forall a. (FooClass a) => IntFn a) -> Bool bar (IntFn fn) = foo fn

In case you hadn't yet discovered it, the solution here is to unpack the IntFn a bit later in a context where the required type argument is known:

bar ifn = foo (case ifn of IntFn fn -> fn)

Hope this helps.

Ah ha, thank you! Yes, this solves my problem.

However, I confess that I am still struggling to understand why unpacking earlier, as I originally tried, is invalid here. The two implementations are:

1) bar ifn = case ifn of IntFn fn -> foo fn 2) bar ifn = foo (case ifn of IntFn fn -> fn)

Why is (1) invalid while (2) is valid? Is is possible to make (1) valid by e.g. adding a type signature somewhere, or is there something fundamentally wrong with it? (I tried a few things that I thought might work, but had no luck.)

I can't help feeling like maybe I am missing some small but important piece from my mental model of how rank-2 types work. (-: Maybe there's some paper somewhere I need to read?

Look at it this way: the argument ifn has a type that says that *for any type a you choose* it is an IntFn. But when you have unpacked it by pattern matching, it only contains a function (a -> Int) for *one specific type a*. At that point, you've chosen your a. The function foo wants an argument that works for *any* type a. So passing it the function from IntFn isn't enough, since that only works for *one specific a*. So you pass it a case expression that produces a function for *any a*, by unpacking the IntFn only inside. I hope that makes sense (and is correct...) Erik

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

System Fc has another name: "GHC Core". You can read it by running 'ghc -ddump-ds' (or, if you want to see the much later results after optimization, -ddump-simpl): For example: NonGADT.hs: {-# LANGUAGE TypeFamilies, ExistentialQuantification, GADTs #-} module NonGADT where data T a = (a ~ ()) => T f :: T a -> a f T = () x :: T () x = T C:\haskell>ghc -ddump-ds NonGADT.hs [1 of 1] Compiling NonGADT ( NonGADT.hs, NonGADT.o ) ==================== Desugar (after optimization) ==================== Result size = 17 NonGADT.f :: forall a_a9N. NonGADT.T a_a9N -> a_a9N [LclIdX] NonGADT.f = \ (@ a_acv) (ds_dcC :: NonGADT.T a_acv) -> case ds_dcC of _ { NonGADT.T rb_dcE -> GHC.Tuple.() `cast` (Sym rb_dcE :: () ~# a_acv) } NonGADT.x :: NonGADT.T () [LclIdX] NonGADT.x = NonGADT.$WT @ () (GHC.Types.Eq# @ * @ () @ () @~ <()>) The "@" is type application; "cast" is a system Fc feature that that allows type equality to be witnessed by terms; Removing the module names and renaming things to be a bit more readable, we get: f :: forall a. T a -> a f = \ (@ a) (x :: T a) -> case x of { T c -> () `cast` (Sym c :: () ~# a) } -- Here ~# is an unboxed type equality witness; it gets erased during compilation. -- We need Sym c because c :: a ~# () and cast wants to go from () to a, so the -- compiler uses Sym to swap the order. x :: T () x = T @() (Eq# @* @() @() @~ <()>) -- Eq# seems to be the constructor for ~#; I'm not sure what the <()> syntax is. -- Notice the kind polymorphism; Eq# takes a kind argument as its first -- argument, then two type arguments of that kind. -- ryan On Fri, Aug 24, 2012 at 2:39 AM, Matthew Steele wrote:

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

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe