Higher order effects, with context adding?

[MagicRB]

Hi, great library! I've been making a binding to libzfs and making an effectful interface on top of it, I ran into a little issue, which involves (I think) higher order effects, but I'm only not sure what to call the thing I want to happen, anyway, code explains well.

Here is the signature for the normal Haskell function I want to model as an effect:

withDataset :: MonadUnliftIO m => ZfsHandle -> String -> Int -> (DatasetHandle -> m a) -> m a

As you can see it a has a callback of sorts, that's how the C libzfs API works and it seems effective, I could later add monadic regions to enforce correctness even.1

And here is the corresponding effect:

data ZFS :: Effect where
  WithDataset :: Text -> Int -> _ -> ZFS m a

I'm not sure what to put instead of the type hole, if I do ZFSDataset m a I would need an inverse of send but that seems like something I can't have, I can't really imagine how it would work even abstractly. Or I can do Eff (ZFSDataset ': es) m, but now es is unbound, so I need to change the hind of ZFS to ZFS es :: * -> Effect or something like that, but then 'es' becomes very recursive in a function such as:

withDataset :: (ZFS es:> es) => Text -> Int -> Eff (ZFSDataset ': es) a -> Eff es a

I'm just not sure how to approach this, is what I'm attempting even possible or do I have to rethink the API?

[arybczak]

Hey, thanks :slightly_smiling_face:

Why not just

data ZFS :: Effect where
  WithDataset :: Text -> Int -> (DatasetHandle -> m a) -> ZFS m a

?

[MagicRB]

Because the DatasetHandle is a implementation specific datatype, which should not be necessary in tests for example, but to be honest, I don't really know, I'm stumbling my way through this essentially :D.

[arybczak]

which should not be necessary in tests

Perhaps. Can you think of a reasonable "mock" implementation of this effect? I don't know exactly what it does so I can't say, but it might not make sense, in which case trying to abstract it away is irrelevant.

I'd suggest going with my suggestion for now and trying to refine things later when you have a working real implementation.

[MagicRB]

Yeah fair, I do tend to overengineer I'll give you that much 😂

[MagicRB]

I'm having a real hard time letting this go, I'm learning something so I'll roll with it for now. What I'd need is the inverse of :>, meaning e :!> es, e is not part of es.

[ocharles]

We probably need a bit more information to answer that one. In general, Haskell can't deal with negative constraints, but if you want to make sure that es doesn't contain e, then the typical way to do that is simply to not provide e :> es.

That is, if we have

foo :: Eff es x

then while es might contain e, foo isn't aware of that, and has to be written as if e wasn't there.

Can you specify the reason you want e :!> es?

[MagicRB]

If I

data ZFS es :: Effect where
  WithDataset :: Text -> Int -> Eff (ZfsDataset ': es) a -> ZFS m a

And then

withDataset :: (ZFS es :> es) -> Text -> Int -> Eff (ZfsDataset ': es) a -> Eff es a
withDataset text int action = sent (WithDataset text int action)

To make the es in WithDataset equal with the one in withDataset I meed to pass it in, only way i found is by adding a type parameter to ZFS, which then ends up being [Effect] -> Effect, but then the type of ZFS es ends up similar to ZFS [ ZFS [ IOE, Error ZfsError ], IOE, Error ZfsError ].

Hopefully that make sense

[arybczak]

Parametrizing an effect with a list of current effects will not work.

If you want to gain access to the current list of effects, this is the way:

data ZFS :: Effect where
  WithDataset :: Text -> Int -> Eff (ZfsDataset : es) a -> ZFS (Eff es) a

[MagicRB]

Indeed that gets me farther, but now how can I specify that with the use of localSeqUnliftIO that Error ZfsError :> localEs? It's yelling at me that it cannot deduce Error ZfsError which makes sense when looking at the source code. I need to make a few changes then I'll know what to ask next :)

[arybczak]

If you need the answer to the question anyway, this is how you specify additional constraints on es (which is referred to as localEs in the effect handler):

data ZFS :: Effect where
  WithDataset :: Error ZfsError :> es => Text -> Int -> Eff (ZfsDataset : es) a -> ZFS (Eff es) a

[MagicRB]

Ok I did need the answer, so it works now, almost, but I'll leave it be and come back to it later. The user facing API is good it's just that this seems a bit weird:

  WithDataset :: (IOE :> es, Error ZfsError :> es) => Text -> Int -> Eff (ZFSDataset ': es) a -> ZFS (Eff es) a
  ZpoolIter :: (IOE :> es, Error ZfsError :> es, Monoid a) => Eff (ZFSPool ': es) a -> ZFS (Eff es) a

I don't really like that the IOE effect is imposed at the GADT level, but that's for later. Thanks for your help!

(for context)

runZfs :: (Error ZfsError :> es, IOE :> es) => Eff (ZFS ': es) a -> Eff es a
runZfs = interpret $ \env eff ->
  localSeqUnliftIO env $ \unliftIO ->
  Z.withZfs $ \zfsHandle ->
    case eff of
      WithDataset name int action ->
        Z.withDataset zfsHandle (T.unpack name) int (unliftIO . flip runZfsDataset action)
      ZpoolIter action ->
        Z.zpoolIter zfsHandle (unliftIO . flip runZpool action) >>= unliftIO . embedError

[Nexmean]

When I experimented with same things I found that best way to implement this is to make such effect definition:

data ZFS :: Effect where
  WithDataset :: Text -> Int -> ZFSDataset m a -> ZFS m a

and then to make function that interprets ZFSDataset effect passing messages to ZFS effect

[MagicRB]

That was what I initially attempted, but I don't understand how to get from Eff (ZFSDataset ': es) a to ZFSDataset m a in

withDataset :: Text -> Int -> Eff (ZFSDataset ': es) a -> Eff es a
withDataset path num action = send (WithDataset path num (something action))

[arybczak]

Closing as I believe the problem was solved.