Effect idea: Lifetime tracking with effects

[qrpnxz]

Building on the ideas from #93's STE, turns out we can use Effects to track object lifetimes:

data Life s :: Effect
type instance DispatchOf (Life s) = Static NoSideEffects
data instance StaticRep (Life s) = Life

newtype Tagged s a = Tagged a

with :: (forall s. Tagged s r -> Eff (Life s : es) a) -> r -> Eff es a
with k = evalStaticRep Life . k . Tagged

withFile :: IOE :> es => FilePath -> IOMode -> (forall s. Tagged s Handle -> Eff (Life s : es) a) -> Eff es a
withFile path mode k = bracket (openFile path mode) hClose (with k)

hFileSize :: (IOE :> es, Life s :> es) => Tagged s Handle -> Eff es Integer
hFileSize (Tagged handle) = liftIO $ hFileSize handle

hTell :: (IOE :> es, Life s :> es) => Tagged s Handle -> Eff es Integer
hTell (Tagged handle) = liftIO $ hTell handle

Example:

main = runEff $
  withFile "/usr/bin/bash" ReadMode $ \bashHandle ->
    withFile "/usr/bin/grep" ReadMode $ \grepHandle -> do
      (liftIO . print) =<< hFileSize grepHandle
      (liftIO . print) =<< raise (hFileSize bashHandle)

(raise to avoid overlapping instances. Perhaps the plug-in helps here, but I haven't been able to use it.)

---

This is utterly inescapable as far as I can tell. You can try to sneak the value out with a GADT, but you can't do anything with it because the effect is gone.

[arybczak]

This is utterly inescapable as far as I can tell

What about escape = pure . unTagged? Then you no longer need to care about s.

[qrpnxz]

I perhaps should have mentioned that not everything would be exported. You would not allow unwrapping Tagged normally. Nor allow running the effect except with with (can be named something else). And unwrapped versions of resource-using operations (e.g. hTell :: Handle -> _ Integer) would ideally not exist, or be part of an unsafe interface.

[qrpnxz]

I came up with Tagged because things like Handle are not already tagged. But a library could have a tag in it's custom object type already, then wrapping would not be necessary, but they would need Life internals to run the effect.

[qrpnxz]

Another use of this lifetime mechanic is safe, unchecked-bounds indexing of arrays. You can tag index values so that they are guaranteed to be in-bounds. I will try to post an example of that later today.

[qrpnxz]

And unwrapped versions of resource-using operations (e.g. hTell :: Handle -> _ Integer) would ideally not exist, or be part of an unsafe interface.

Actually, even these should be fine as long as you can never get a Handle willy nilly. And it should be simple to write like _ :: (Life s :> es) => (Handle -> _ a) -> (Tagged s Handle -> Eff es a).

[qrpnxz]

Specializing the technique to a particular effect may be preferred for some things:

data File s :: Effect
type instance DispatchOf (File s) = Static WithSideEffects
data instance StaticRep (File s) = File IO.Handle

type Handle = Proxy

withFile :: (IOE :> es) => FilePath -> IOMode -> (forall s. Handle s -> Eff (File s : es) a) -> Eff es a
withFile path mode action = bracket (openFile path mode) hClose $ \h ->
  evalStaticRep (File h) (action Proxy)

fileSize :: forall s es. File s :> es => Handle s -> Eff es Integer
fileSize _ = do -- ^ ScopedTypeVariables v
  (File h) <- getStaticRep :: Eff es (StaticRep (File s))
  unsafeEff_ $ hFileSize h

Example:

main = runEff $
  withFile "/usr/bin/bash" ReadMode $ \h1 ->
    withFile "/usr/bin/grep" ReadMode $ \h2 -> do
      (liftIO . print) =<< fileSize h2
      (liftIO . print) =<< raise (fileSize h1)

I think Handle s actually being the handle is preferable (at least for File s) for a couple of reasons, but I just wanted to demonstrate an alternative.

---

Automatic memory management:

data Malloc s :: Effect
type instance DispatchOf (Malloc s) = Static WithSideEffects
data instance StaticRep (Malloc s) = Malloc

newtype Ptr s a = Ptr (Foreign.Ptr a)

withMalloc :: (Storable a, IOE :> es) => a -> (forall s. Ptr s a -> Eff (Malloc s : es) a) -> Eff es a
withMalloc a k = bracket (new a) free $ \ptr ->
  evalStaticRep Malloc $ k (Ptr ptr)

peekElemOffEff :: (Storable a, Malloc s :> es) => Ptr s a -> Int -> Eff es a
peekElemOffEff (Ptr ptr) idx = unsafeEff_ $ Foreign.peekElemOff ptr idx

[qrpnxz]

A tweak of the instance fix from #98 works here: (and in transformer stacks, btw!)

instance {-# INCOHERENT #-} File s :> (File s : es) where
  reifyIndex = 0

instance {-# INCOHERENT #-} File s :> es => File s :> (File s' : es) where
  reifyIndex = 1 + reifyIndex @(File s) @es

Now we can

main = runEff $
  withFile "/usr/bin/bash" ReadMode $ \bashHandle ->
    withFile "/usr/bin/grep" ReadMode $ \grepHandle -> do
      (liftIO . print) =<< hFileSize grepHandle
      (liftIO . print) =<< hFileSize bashHandle

But I found an even more general fix:

instance e :> (e : es) where
  reifyIndex = 0

instance {-# INCOHERENT #-} e :> es => e :> (x : es) where
  reifyIndex = 1 + reifyIndex @e @es

This makes File and Malloc behave correctly. (@arybczak would you mind trying these out in some of your projects? So far they work better for me.)

These don't help STE. I'm guessing because there's no token passed around that will help GHC entangle uses of the effect with the runner, but the fix from the showcase does work:

instance {-# INCOHERENT #-} s1 ~ s2 => STE s1 :> (STE s2 : es) where
  reifyIndex = 0

[arybczak]

A tweak of the instance fix

What's wrong with the original, i.e.

instance {-# INCOHERENT #-} s1 ~ s2 => File s1 :> (File s2 : es) where
  reifyIndex = 0

?

@arybczak would you mind trying these out in some of your projects? So far they work better for me

It doesn't work properly, the testsuite of effectful doesn't compile if you do this.

[qrpnxz]

What's wrong with the original

I couldn't tell you why it doesn't quite work. I just get this:

720:28: error:
    • Couldn't match type ‘s1’ with ‘s’
        arising from a use of ‘fileSizeEff’
      ‘s1’ is a rigid type variable bound by
        a type expected by the context:
          forall s1. THandle s1 -> Eff '[File s1, File s, IOE] ()
        at parsing/Bench/Generic.hs:(718,44)-(720,41)
      ‘s’ is a rigid type variable bound by
        a type expected by the context:
          forall s. THandle s -> Eff '[File s, IOE] ()
        at parsing/Bench/Generic.hs:(717,51)-(720,41)
    • In the second argument of ‘(=<<)’, namely ‘fileSizeEff p1’
      In a stmt of a 'do' block: (liftIO . print) =<< fileSizeEff p1
      In the expression:
        do (liftIO . print) =<< fileSizeEff p2
           (liftIO . print) =<< fileSizeEff p1
    • Relevant bindings include
        p2 :: THandle s1 (bound at parsing/Bench/Generic.hs:718:45)
        p1 :: THandle s (bound at parsing/Bench/Generic.hs:717:52)
    |       
720 |       (liftIO . print) =<< fileSizeEff p1

whereas the modification just has no problem.

It doesn't work properly, the testsuite of effectful doesn't compile if you do this.

Hmm, alright. I'll try to run it later to see if it can be tweaked more.

[arybczak]

FWIW the incoherent instance from my above comment doesn't fully work. It unifies s when monomorphic stack is used, but does nothing to aid type inference if polymorphic stacks and :> constraints are used, so in the end it's not very useful.

[arybczak]

Closing as out of scope for the core library. If you (or anyone else) is interested, this can be provided in a standalone library.