Having it both ways with rank-n-types

Question

I'm playing with a ConduitT style monad that uses existential quantification, and I'm playing whack-a-mole trying to get the types to unify. There's two versions of this scenario:

Here, Await i has an existentially quantified a, which allows the await method to pass it whatever type of i -> Await i -> a that it wants.

{-# LANGUAGE RankNTypes #-}

newtype Piped r a = Piped { unPiped :: forall b. r -> (r -> a -> b) -> b }

instance Functor (Piped r) where                              
  fmap f (Piped c) = Piped $ \r rest -> c r (\r -> rest r . f)

runPiped :: Piped r a -> r -> a      
runPiped (Piped p) r = p r $ \_ -> id

newtype Await i = Await { unAwait :: forall a. Yield i a -> a }           
newtype Yield i a = Yield { unYield :: i -> Await i -> a }                

runAwait :: Await i -> (i -> Await i -> a) -> a                           
runAwait (Await await) = await . Yield                                    

runYield :: Yield i a -> i -> (Yield i a -> a) -> a                       
runYield (Yield yield) i = yield i . Await
                     -- broke        ^^^^^
                     -- because Await swallows the type of `a`                                

await :: forall i a y. Piped (Await i, y) i                               
await = Piped $                                                           
  \(a, y) f -> runAwait a $ \i a' -> f (a', y) i

Fails with:

• Couldn't match type ‘Yield i a -> a’
                 with ‘forall a1. Yield i a1 -> a1’
  Expected type: (Yield i a -> a) -> Await i
    Actual type: (forall a. Yield i a -> a) -> Await i
• In the second argument of ‘(.)’, namely ‘Await’

The runYield method is broken because it can't unify the existentially qualified type parameter in Await i with a.

Second scenario:

In order to fix runYield, Await now specifies a, which unifies Await i a with Yield i a. However, now that a is specified, yield can't pass it an Yield i b with any value of b that it pleases:

newtype Piped r a = Piped { unPiped :: forall b. r -> (r -> a -> b) -> b }
newtype Await i a = Await { unAwait :: Yield i a -> a }                   
newtype Yield i a = Yield { unYield :: i -> Await i a -> a }              

runAwait :: Await i a -> (i -> Await i a -> a) -> a                       
runAwait (Await await) = await . Yield                                    

runYield :: Yield i a -> i -> (Yield i a -> a) -> a                       
runYield (Yield yield) i = yield i . Await                                

await :: Piped (Await i a, y) i                                           
await = Piped $                                                           
  \(a, y) f -> runAwait a $ \i a' -> f (a', y) i                          
-- ^^^^^^

Fails with:

• Couldn't match type ‘b’ with ‘a’
  ‘b’ is a rigid type variable bound by
    a type expected by the context:
      forall b. (Await i a, y) -> ((Await i a, y) -> i -> b) -> b
  Expected type: (Await i a, y)
    Actual type: (Await i b, y)

So I appear to need it both ways, existentially quantified sometimes and concrete other times. I've tried creating wrappers to hide the extra type parameter, switching newtype for data, and it also occurred to me that if i could define a function Await i a -> Await i b that might also solve the issue but I'm a bit out of my depth here. Any ideas?

FYI, switching between newtype and data has no hope of helping you solve any type errors, unless the type declaration itself produces an error. — dfeuer
Are you sure you don't want runYield :: Yield i a -> i -> (forall a2 . Yield i a2 -> a2) -> a ? With your signature it looks incorrect to me -- you need the rank-2 type. — chi
This seems to produce the same error as in the first scenario. — Scott
Am I being dense? I don't see any existential variables. data Await i = Await i (Await i) and newtype Yield i a = Yield (Await i -> a) if you remove all the CPS, no? It's rank-1 universal quantification all the way through? — HTNW
I retract my answer; @chi's comment is the way to go, I think. You might need to rewrite runYield in pointful form to make it work. — user11228628

Scott Scott · Accepted Answer · 2019-04-20T21:09:47

I ran into the same problem once I tried to define the yield function; i had to remove the extra type variable from yield and it wouldn't typecheck.

The solution turned out to be to redefine the types as such:

newtype Await i = Await { unAwait :: forall b. Yield' i b -> b }     
newtype Yield i = Yield { unYield :: forall b. i -> Await' i b -> b }

type Await' i a = Yield i -> a                                       
type Yield' i a = i -> Await i -> a

This way, there's no additional constructor to swallow type variables in await:

await :: Piped (Await i, y) i                  
await = Piped $                                
  \(Await a, y) f -> a $ \i a' -> f (a', y) i

Having it both ways with rank-n-types

1 Answers