Is unsafeInterleaveIO idempotent?

Learn
#1

I am writing a LazyIO applicative (hobby experiment, not serious) and I want to make sure everything is as lazy as can be without introducing weird semantic issues stemming from ignorance.

newtype LazyIO a = LazyIO { unLazyIO :: IO a } 

instance Functor LazyIO where
  fmap f io = LazyIO $ fmap f (unsafeInterleaveIO $ unLazyIO io) 

instance Applicative LazyIO where
  pure = LazyIO . pure 
  f <*> g = LazyIO $ do
    f' <- unsafeInterleaveIO $ unLazyIO f 
    g' <- unsafeInterleaveIO $ unLazyIO g 
    pure $ f' g'  
  

liftLIO :: IO a -> LazyIO a 
liftLIO = LazyIO 

runLazyIO :: LazyIO a -> IO a 
runLazyIO = unsafeInterleaveIO . unLazyIO
#2

If you can rely on the IO’s you are accessing are idempotent then this will work, but IO can by definition do anything and is not

#3

I want to make sure everything is as lazy as can be without introducing weird semantic issues stemming from ignorance.

…alright, but remember - you did want “to make sure”.

Now to answer the question:

Is unsafeInterleaveIO idempotent?

or:

unsafeInterleaveIO (unsafeInterleaveIO m) ≟ unsafeInterleaveIO m

(note the small question mark over the equals symbol).

Now for some equational reasoning:

(original expression on left)
unsafeInterleaveIO (unsafeInterleaveIO m)

(from the definition of unsafeInterleaveIO)
= unsafeDupableInterleaveIO (noDuplicate >> (unsafeDupableInterleaveIO (noDuplicate >> m)))

…question: what is noDuplicate :: IO ()?

Ensures that the suspensions under evaluation by the current thread are unique; that is, the current thread is not evaluating anything that is also under evaluation by another thread that has also executed noDuplicate.

This operation is used in the definition of unsafePerformIO to
prevent the IO action from being executed multiple times, which is
usually undesirable.

…so in this situation calling noDuplicate more than once is redundant, as m is part of the larger I/O action noDuplicate >> (unsafeDupableInterleaveIO (noDuplicate >> m))

Back to the equational reasoning:

(inner noDuplicate call redundant)
= unsafeDupableInterleaveIO (noDuplicate >> (unsafeDupableInterleaveIO m))

(assumption: only one I/O thread in use)
= unsafeDupableInterleaveIO (unsafeDupableInterleaveIO m)

Two points:

  • use assumptions wisely;

  • the next step would be to use the definition of unsafeDupableInterleaveIO:

    unsafeDupableInterleaveIO (IO m)
  = IO ( \ s -> let
                   r = case m s of (# _, res #) -> res
                in
                (# s, r #))

    to replace its calls. For larger definitions, sometimes using an auxiliary definition can be helpful:

    unsafeDupableInterleaveIO (IO m)
  = IO (\ s -> unsafeDupableInterleaveIO# m s)

unsafeDupableInterleaveIO# m s =
  = let
       r = case m s of (# _, res #) -> res
    in
    (# s, r #)

    Now all the actual work is done by unsafeDupableInterleaveIO#.

More equational reasoning:

(change of name: m → act)
= unsafeDupableInterleaveIO (unsafeDupableInterleaveIO act)

(from that modified definition of unsafeDupableInterleaveIO, and act = IO m)
= case act of IO m -> unsafeDupableInterleaveIO (IO (\ s -> unsafeDupableInterleaveIO# m s))

(…again, but taking care to avoid name clashes)
= case act of IO m -> IO (\ s0 -> unsafeDupableInterleaveIO# (\s -> unsafeDupableInterleaveIO# m s)) s0)

(since unsafeDupableInterleaveIO# is a function)
= case act of IO m -> IO (\ s0 -> unsafeDupableInterleaveIO# (unsafeDupableInterleaveIO# m) s0

(…and again)
= case act of IO m -> IO (unsafeDupableInterleaveIO# (unsafeDupableInterleaveIO# m))

From all of that, your original question now reduces to:

unsafeDupableInterleaveIO# (unsafeDupableInterleaveIO# w) ≟ unsafeDupableInterleaveIO# w

  • again, note that small question mark,
  • and the new name w, to avoid confusion with the original m (and subsequently act)

Now to start a second equational-reasoning session:

unsafeDupableInterleaveIO# (unsafeDupableInterleaveIO# w) =

  • (since unsafeDupableInterleaveIO# is a function of two parameters)

    unsafeDupableInterleaveIO# (\s -> unsafeDupableInterleaveIO# w s)

  • (from the definition of unsafeDupableInterleaveIO#)

    unsafeDupableInterleaveIO# 
   (\ s -> let
              r = case w s of (# _, res #) -> res
           in
           (# s, r #))

  • (again, since unsafeDupableInterleaveIO# is a function of two parameters)

    \ s0 -> unsafeDupableInterleaveIO# 
   (\s -> let
             r = case w s of (# _, res #) -> res
          in
          (# s, r #))
   s0

  • (using the definition of unsafeDupableInterleaveIO# again)

    \ s0 -> let
           r = case (\s -> let
                              r = case w s of (# _, res #) -> res
                           in
                           (# s, r #))
                    s0
                of (# _, res #) -> res
        in
        (# s0, r #)

  • (renaming the “outer” r and res to avoid confusion later)

    \ s0 -> let
           r1 = case (\s -> let
                               r = case w s of (# _, res #) -> res
                            in
                            (# s, r #))
                     s0
                 of (# _, res0 #) -> res0
        in
        (# s0, r1 #)

From here, it’s just a matter of:

  • applying that “inner lambda” (\ s -> let ... in (# s, r #)) to its argument s0,

  • simplifying those case expressions and changing names as needed,

  • then carefully observing the final expression, looking for (sub)expressions which can be replaced by a combination of calls to existing functions.

If you’re wondering why I’m leaving these last few steps to you:

…so please don’t “copy & paste” what you did to answer your original question:

Is unsafeInterleaveIO idempotent?

A simple “yes” or “no” will suffice :-D

2 Likes