Matthew Steele | 22 Aug 13:25 2012
Picon

Rigid skolem type variable escaping scope

While working on a project I have come across a new-to-me corner case of the type system that I don't think I
understand, and I am hoping that someone here can enlighten me.

Here's a minimal setup.  Let's say I have some existing code like this:

    {-# LANGUAGE Rank2Types #-}

    class FooClass a where ...

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

Now I want to make a type alias for these (a -> Int) functions, and give myself a new way to call foo.  I could do this:

    type IntFn a = a -> Int

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

This compiles just fine, as I would expect.  But now let's say I want to change it to make IntFn a newtype:

    newtype IntFn a = IntFn (a -> Int)

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

I had expected this to compile too.  But instead, I get an error like this one (using GHC 7.4.1):

    Couldn't match type `a0' with `a'
      because type variable `a' would escape its scope
(Continue reading)

Simon Peyton-Jones | 22 Aug 16:01 2012
Picon

Re: Rigid skolem type variable escaping scope

| This compiles just fine, as I would expect.  But now let's say I want
| to change it to make IntFn a newtype:
| 
|     newtype IntFn a = IntFn (a -> Int)
| 
|     bar :: (forall a. (FooClass a) => IntFn a) -> Bool
|     bar (IntFn fn) = foo fn

The easiest way is to imagine transforming the function to System F. I'll ignore the (FooClass a) bit since
it's irrelevant.  We'd get

bar = \(x :: forall a. IntFn a).
      ...what?...

We can't do case-analysis on x; it has a for-all type, so we must instantiate it. But at what type?  Let's guess
some random type 'b':

bar = \(x : forall a. IntFn a).
      case (x b) of 
        IntFn (f :: b -> Int) -> foo f

But now we are in trouble.  'foo' itself needs an argument of type (forall a. a->Int).  So we need a big lambda

bar = \(x : forall a. IntFn a).
      case (x b) of 
        IntFn (f :: b -> Int) -> foo (/\a. f)

But this is obviously wrong because 'b' escapes the /\a.

I don't know if I can explain it better than that
(Continue reading)

Lauri Alanko | 22 Aug 21:02 2012
Picon
Picon

Re: Rigid skolem type variable escaping scope

Quoting "Matthew Steele" <mdsteele <at> 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.

Lauri
Matthew Steele | 22 Aug 22:13 2012
Picon

Re: Rigid skolem type variable escaping scope

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

> Quoting "Matthew Steele" <mdsteele <at> 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)
(Continue reading)

Erik Hesselink | 22 Aug 22:32 2012
Picon

Re: Rigid skolem type variable escaping scope

On Wed, Aug 22, 2012 at 10:13 PM, Matthew Steele <mdsteele <at> alum.mit.edu> wrote:
> On Aug 22, 2012, at 3:02 PM, Lauri Alanko wrote:
>
>> Quoting "Matthew Steele" <mdsteele <at> 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
(Continue reading)

Matthew Steele | 22 Aug 23:23 2012
Picon

Re: Rigid skolem type variable escaping scope

On Aug 22, 2012, at 4:32 PM, Erik Hesselink wrote:

> On Wed, Aug 22, 2012 at 10:13 PM, Matthew Steele <mdsteele <at> alum.mit.edu> wrote:
>> On Aug 22, 2012, at 3:02 PM, Lauri Alanko wrote:
>> 
>>> Quoting "Matthew Steele" <mdsteele <at> 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:
(Continue reading)

wren ng thornton | 24 Aug 04:32 2012

Re: Rigid skolem type variable escaping scope

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  <at> A of
         IntFn (fn :: A -> Int) -> foo (/\B -> \(b::B) -> fn  <at> B b)

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

There are two problems with bar1. First, where do we magic up that type 
(Continue reading)

Matthew Steele | 24 Aug 11:39 2012
Picon

Re: Rigid skolem type variable escaping scope

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[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,
(Continue reading)

Ryan Ingram | 24 Aug 23:26 2012
Picon

Re: Rigid skolem type variable escaping scope

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 =
  \ ( <at> 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 <at> () (GHC.Types.Eq# <at> * <at> () <at> () <at> ~ <()>)

The " <at> " 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 = \ ( <at> 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 <at> () (Eq# <at> * <at> () <at> () <at> ~ <()>)
-- 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 <mdsteele <at> alum.mit.edu> 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 <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Lauri Alanko | 22 Aug 22:50 2012
Picon
Picon

Re: Rigid skolem type variable escaping scope

Quoting "Matthew Steele" <mdsteele <at> alum.mit.edu>:
> 1) bar ifn = case ifn of IntFn fn -> foo fn
> 2) bar ifn = foo (case ifn of IntFn fn -> fn)

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

As SPJ suggested, translation to System F with explicit type  
applications makes the issue clearer:

1) bar = \(ifn :: forall a. IntFn a).
              case ifn _a of IntFn (fn :: _a -> Int) -> foo (/\a. ???)
2) bar = \(ifn :: forall a. IntFn a).
              foo (/\a. case ifn a of IntFn (fn :: a -> Int) -> fn)

Lauri
oleg | 23 Aug 13:27 2012

Rigid skolem type variable escaping scope


Matthew Steele asked why foo type-checks and bar doesn't:
>   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

This and further questions become much simpler if we get a bit more
explicit. Imagine we cannot write type signatures like those of foo
and bar (no higher-ranked type signatures). But we can define
higher-rank newtypes. Since we can't give foo the higher-rank
signature, we must re-write it, introducing the auxiliary
newtype FaI.

> {-# LANGUAGE Rank2Types #-}

> class FooClass a where m :: a
>
> instance FooClass Int where m = 10
>
> newtype FaI = FaI{unFaI :: forall a. (FooClass a) => a -> Int}

> foo :: FaI -> Bool
> foo fn = ((unFaI fn)::(Char->Int)) m > 0

We cannot apply fn to a value: we must first remove the wrapper FaI
(and instantiate the type using the explicit annotation -- otherwise
the type-checker has no information how to select the FooClass
instance).

Let's try writing bar in this style. The first attempt

> newtype IntFn a = IntFn (a -> Int)
> newtype FaIntFn = FaIntFn{unFaIntFn:: forall a. FooClass a => IntFn a}
>
> bar :: FaIntFn -> Bool
> bar (IntFn fn) = foo fn

does not work: 
    Couldn't match expected type `FaIntFn' with actual type `IntFn t0'
    In the pattern: IntFn fn

Indeed, the argument of bar has the type FaIntFn rather than IntFn, so
we cannot pattern-match on IntFn. We must first remove the IntFn
wrapper. For example:

> bar :: FaIntFn -> Bool
> bar x = case unFaIntFn x of
>          IntFn fn  -> foo fn

That doesn't work for another reason: 
    Couldn't match expected type `FaI' with actual type `a0 -> Int'
    In the first argument of `foo', namely `fn'
    In the expression: foo fn

foo requires the argument of the type FaI, but fn is of the type
a0->Int. To get the desired FaI, we have to apply the wrapper FaI:

> bar :: FaIntFn -> Bool
> bar x = case unFaIntFn x of
>          IntFn fn  -> foo (FaI fn)

And now we get the desired error message, which should become clear:

    Couldn't match type `a0' with `a'
      because type variable `a' would escape its scope
    This (rigid, skolem) type variable is bound by
      a type expected by the context: FooClass a => a -> Int
    The following variables have types that mention a0
      fn :: a0 -> Int (bound at /tmp/h.hs:16:16)
    In the first argument of `FaI', namely `fn'
    In the first argument of `foo', namely `(FaI fn)'

When we apply FaI to fn, the type-checker must ensure that fn is
really polymorphic. That is, free type variable in fn's type do not
occur elsewhere type environment: see the generalization rule in the
HM type system. When we removed the wrapper
unFaIntFn, we instantiated the quantified type variable a with some
specific (but not yet determined) type a0. The variable fn receives
the type fn:: a0 -> Int. To type-check FaI fn, the type checker should
apply this rule

	G |- fn :: FooClass a0 => a0 -> Int
        -----------------------------------
        G |- FaI fn :: FaI

provided a0 does not occur in G. But it does occur: G has the binding
for fn, with the type a0 -> Int, with the undesirable occurrence of
a0.

To solve the problem then, we somehow need to move this problematic binding fn
out of G. That binding is introduced by the pattern-match. So, we
should move the pattern-match under the application of FaI:

> bar x = foo (FaI (case unFaIntFn x of IntFn fn  -> fn))

giving us the solution already pointed out.

> So my next question is: why does unpacking the newtype via pattern
> matching suddenly limit it to a single monomorphic type?

Because that's what removing wrappers like FaI does. There is no way
around it. That monomorphic type can be later generalized again, if
the side-condition for the generalization rule permits it.

You might have already noticed that `FaI' is like big Lambda of System
F, and unFaI is like System F type application. That's exactly what
they are:
     http://okmij.org/ftp/Haskell/types.html#some-impredicativity

My explanation is a restatement of the Simon Peyton-Jones explanation,
in more concrete, Haskell terms.

Gmane