Haskell's flaw with ContT, callCC when

Ongoing quest to make sense of ContT and friends. Please consider the (absurd but illustrative) code below:

v :: IO (Either String [String]) v = return $ Left "Error message" doit :: IO (Either String ()) doit = (flip runContT return) $ callCC $ \k -> do x <- liftIO $ v x2 <- either (k . Left) return x when True $ k (Left "Error message 2") -- k (Left "Error message 3") return $ Right () -- success 

This code does not compile. However, if you replace when k-call comment below, it compiles. What's happening?

Alternatively, if I comment out the x2 line, it also compiles. ???

Obviously, this is a distilled version of the source code, and therefore all elements serve the purpose. Appreciate the explanatory help about what is happening and how to fix it. Thanks.

+4
source share
1 answer

The problem here is with the when and either types, and not something special for ContT:

 when :: forall (m :: * -> *). (Monad m) => Bool -> m () -> m () either :: forall ac b. (a -> c) -> (b -> c) -> Either ab -> c 

The second argument must be of type m () for some monad m . Thus, the when line of your code can be changed as follows:

 when True $ k (Left "Error message 2") >> return () 

to compile the code. This is probably not what you want to do, but it gives us a hint about what might be wrong: the type k was declared unacceptable for when .

Now for the signature either : note that the two arguments either must be functions that produce results of the same type. The return type here is determined by the type x , which, in turn, is fixed by an explicit signature on v . Thus, the bit (k . Left) must be of the same type; this in turn captures the type k at (defined by the GHC)

 k :: Either String () -> ContT (Either String ()) IO [String] 

This is incompatible with when .

However, when you comment out the line x2 , its influence on the type of code code check is deleted, so k no longer forced into an inconvenient type and can freely take the type

 k :: Either [Char] () -> ContT (Either [Char] ()) IO () 

which is good in the when book. Thus, the code is compiled.

As a final note, I used the GHCi breakpoints tool to get exact types of k according to two scenarios - I'm not so expert as to write them out manually and be sure of their correctness :-) Use :break ModuleName line-number column-number to try.

+6
source

Source: https://habr.com/ru/post/1300701/


All Articles