Solution to https://twitter.com/tomas_mikula/status/1299347086203330560

dependent_effects.hs

{-# LANGUAGE RankNTypes #-} 
    
import Control.Monad (join)    
    
sendBoth    
  :: (Monad m, Applicative n)    
  => (forall a. a -> m ())    
  -> (forall a. m a -> n a)    
  -> (forall a. n a -> m a)    
  -> m a    
  -> m b    
  -> (a -> c)    
  -> (a -> b -> d)    
  -> m ()    
sendBoth postToTwitter mn nm ma mb g h =    
  join . nm $    
    (\a b -> postToTwitter $ h a b)                                     
      <$> mn ((\a -> nm (mn (postToTwitter $ g a) *> pure a)) =<< ma)  
      <*> mn mb                                                 
                         

eval_time.hs

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TupleSections #-}

import Control.Monad (join)

sendBoth
  :: (Monad m, Applicative n)
  => (forall a. (() -> a) -> n a)
  -> (forall a. m a -> n a)
  -> (forall a. n a -> m a)
  -> m a
  -> m b
  -> (a -> c)
  -> (a -> b -> d)
  -> (b -> e)
  -> m (c, d, e)
sendBoth async mn nm ma mb g h i =
  join . nm $ (\(nc, a) (ne, b) -> nm $ (,,) <$> nc <*> async (\_ -> h a b) <*> ne)
    <$> ((\a -> (async (\_ -> g a), a)) <$> mn ma)
    <*> ((\b -> (async (\_ -> i b), b)) <$> mn mb)

launch_async.hs

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TupleSections #-}

import Control.Monad (join)

sendBoth
  :: forall m n a b c d e
  .  (Monad m, Applicative n)
  => (forall x. (() -> x) -> m (n x))
  -> (forall x. m x -> n x)
  -> (forall x. n x -> m x)
  -> m a
  -> m b
  -> (a -> c)
  -> (a -> b -> d)
  -> (b -> e)
  -> m (c, d, e)
sendBoth async mn nm ma mb g h i = do
  ((nc, a), (ne, b)) <- nm (
    (,) <$> mn ((\a -> (,a) <$> async (\_ -> g a)) =<< ma)
        <*> mn ((\b -> (,b) <$> async (\_ -> i b)) =<< mb)
     )
  nd <- async (\_ -> h a b)
  nm $ (,,) <$> nc <*> nd <*> ne

This demands special semantics for n () in that an interpreter for such a value treats n () *> n a such that a is made available to subsequent computations as soon as n a is performed, without "waiting to observe ()".

async is a model of just "send this evaluation to another core".

I'm really being made to work for this! In this third installment, n represents the ability to wait for the completion of the evaluation of an asynchronous computation.