On Aug 22, 2012, at 4:32 PM, Erik Hesselink wrote:
> On Wed, Aug 22, 2012 at 10:13 PM, Matthew Steele <mdste...@alum.mit.edu>
> wrote:
>> On Aug 22, 2012, at 3:02 PM, Lauri Alanko wrote:
>>
>>> Quoting "Matthew Steele" <mdste...@alum.mit.edu>:
>>>
>>>> {-# 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.
Okay, that does make sense, and I can see now why (2) works while (1) doesn't.
So my next question is: why does unpacking the newtype via pattern matching
suddenly limit it to a single monomorphic type? As you said, ifn has the type
"something that can be an (IntFn a) for any a you choose". Since an (IntFn a)
is just a newtype around an (a -> Int), why, when you unpack ifn into (IntFn
fn), is the type of fn not "something that can be an (a -> Int) for any a you
choose"? Is it possible to add a local type annotation to force fn to remain
polymorphic?
Cheers,
-Matt
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
