Either -> rank2 type correspondence

1
2
3
4
5
6
7
8
9
10
11
12
13
14
{-# LANGUAGE RankNTypes #-}
data Test a b = Test {runTest :: (forall r. (a -> r) -> (b -> r) -> r)}
              
test :: Test Int String
test = Test (\f g -> f 4)
       
test2 :: Test Bool [Int]
test2 = Test (\f g -> g [3,4,5])
    
a = runTest test Left Right -- Left 4
a2 = runTest test2 Left Right -- Right [3,4,5]
    
b = runTest test Just (const Nothing) -- Just 4
b2 = runTest test2 Just (const Nothing) -- Nothing

Either -> rank2 type correspondence (annotation)

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
data EitherCPS a b = CPS { case_ :: forall r. (a -> r) -> (b -> r) -> r }

leftCPS :: a -> EitherCPS a b
leftCPS a = CPS (\ka kb -> ka a)

rightCPS :: b -> EitherCPS a b
rightCPS b = CPS (\ka kb -> kb b)

proj1 :: Either a b -> EitherCPS a b
proj1 (Left a) = leftCPS a
proj1 (Right b) = rightCPS b

proj2 :: EitherCPS a b -> Either a b
proj2 sum =
  case_ sum
        ( \ a -> Left a )
        ( \ b -> Right b )