CODEWITHSUNDEEP
haskellexistential-typerank-n-types
Scott
Scott

Reputation: 4110

Having it both ways with rank-n-types

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?

Upvotes: 1

Views: 97

Answers (1)

Scott
Scott

Reputation: 4110

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

Upvotes: 0

Related Questions