Rank-2-Types and the Scope

Help
#1

Hi!

i’m trying to understand rank-2-types and what a scope is. so i have started to play around with this type

data Foo u v = Foo u (u -> v)

Now for example this fails with “Type Variable u has escaped its scope”:

foo :: forall a. a -> (forall u. Foo u a) -> a
foo a q@(Foo u f) = foo (f u) q

In my naive world this should work because it is not necessary to know for the type-checker what u is inside the scope of foo - it is only used in the context of f.

anyway this can be done by moving some parts around and helping the type-checker understand that u really has nothing to do with foo

foo :: forall a. a -> (forall u. Foo u a) -> a
foo a q = foo (g q) q
  where
  g :: forall u. Foo u a -> a
  g (Foo u f) = f u

but this gets quite ugly when having something like Array (forall u. Foo u a)) or Maybe etc. In this case using map will not work:

foo :: forall a. Array a -> (Array (forall u. Foo u a)) -> Array a
foo as qs = foo (g <$> qs) qs
  where
  g :: forall u. Foo u a -> a
  g (Foo u f) = f u

where redefining map with bind is ok

foo :: forall a. Array a -> (Array (forall u. Foo u a)) -> Array a
foo as qs = foo (qs >>= (pure <<< g)) qs
  where
  g :: forall u. Foo u a -> a
  g (Foo u f) = f u

Somewhat this does not feel right.

Soooo, What is a scope? And what defines a scope? Especially the last example with the array seems odd - How to probably handle this case?

#2

The issue with your first example pertains to where the u in forall u. Foo u a is being instantiated. The general intuition for forall is that you can think of it like a term-level lambda abstraction that takes a type as an argument. So in the case of forall u. Foo u a, this is intuitively a function from type u to Foo u a. Applying a type argument like this is called instantiation. In order to pattern match on Foo u a we must first instantiate it (apply a type argument), just like if you had String -> Maybe Int you would have to apply a String before you could pattern match on the Maybe. The q binder is binding to the instantiated Foo, and not the generalized Foo. Once it’s instantiated, it won’t typecheck as forall u. Foo u a just like Maybe Int won’t typecheck as String -> Maybe Int. When you pull it out into an intermediate g, the outer q is not being instantiated, so it will continue to typecheck. The confusion arises because these instantiations are implicit.

The issue with Array (forall ...) is that this is an impredicative type, which is an open research problem. There’s a whole host of literature on this, and even some new stuff. GHC is potentially getting something called “guarded” impredicativity which might help with cases like this.

Basically the compiler does not really attempt to deal with impredicativity. When and where to instantiate is kind of ambiguous. The workaround is to define a newtype, which gives the compiler clear boundaries for instantiation.

newtype GFoo a = GFoo (forall u. Foo u a)

-- No longer any impredicative types in this signature since
-- it's hidden under a constructor,
foo :: forall a. Array a -> Array (GFoo a) -> Array a
4 Likes
#3

The first example can be made clear by looking at what it desugars to:

foo :: forall a. a -> (forall u. Foo u a) -> a
foo a tmp = case tmp {- `u` is instantiated here -} of
  q@(Foo u f) -> foo (f u) q

So, you are binding q to the result of instantiating tmp with a fresh unknown. You can also manually write it as:

foo :: forall a. a -> (forall u. Foo u a) -> a
foo a q = case q of
  Foo u f -> foo (f u) q

Which works.