Enforcing correct API usage via types

Learn
#1

Hi, I am trying to write type-safe interface to a key-value store (gdbm), C
interface of which can be simplified to following:

data DB
openRead :: FilePath -> IO DB
openWrite :: FilePath -> IO DB
close :: DB -> IO ()
fetch :: DB -> ByteString -> IO (Maybe ByteString)
store :: DB -> ByteString -> ByteString -> IO ()
firstkey :: DB -> IO (Maybe ByteString)
nextkey :: DB -> ByteString -> IO (Maybe ByteString)

And there are following rules about this interface:

  • store can only be called on database open with openWrite.
  • You should call close as soon you don’t need database anymore.
  • You may not use DB object once you closed it.
  • Functions firstkey and nextkey allow you to iterate keys, but you may
    not call store between call of firstkey and nextkey.
  • User not necessary want to iterate all keys.
  • User may want to work with multiple databases.

Here is my attempt to tackle the problem. I used
regions library to address
second and third points, and phantom parameter to track if database is in write
mode (ignore Either ByteString part, it is about error reporting). You can
take a look at compilable source here

openRead :: (RegionIOControl pr, r ~ RegionT s pr) => FilePath -> r (Either ByteString (GDBM ReadMode r))
openWrite :: (RegionIOControl pr, r ~ RegionT s pr) => FilePath -> r (Either ByteString (GDBM WriteMode r))
fetch :: (MonadIO cr, AncestorRegion pr cr) => GDBM m pr -> ByteString -> cr (Maybe ByteString)
store :: (MonadIO cr, AncestorRegion pr cr) => GDBM WriteMode pr -> ByteString -> ByteString -> cr ()

And now I need somehow to do key iteration. I imagine I could have type like
following:

iterate :: (Monoid m, MonadIO cr, AncestorRegion pr cr) => GDBM m pr -> (m -> ByteString -> cr (m, Bool)) -> cr ()
iterate db f = do ...

where Bool value designates if user wants to continue iterating or want to
break. Problem is that there is nothing stopping user from using db argument
inside f to call store, at which point we lose. Effectively, I need to
temporary revoke access to database handle from outer scope, and I am not aware
of any mechanisms for doing so.

Am I holding it wrong?

2 Likes
#2

Why not limit iteration to ReadMode?

Also, why not use linear types?

#3

It is perfectly reasonable to open database in WriteMode, law-abidingly enumerate keys, and that store something into database.

EDIT: Plus, I didn’t mention it in original question, but writer claims exclusive lock, so re-opening database is also prone to race conditions.

Can you elaborate a bit on how linear types can solve the problem?

#4

I was thinking: open the database in ReadMode, iterate over it, close it, open it in WriteMode and then write to it? But I guess that is perhaps annoying to do every time.

With linear types you can switch to a new mode on the fly while preventing the user from accessing the database with the old mode.

#5

LinearTypes is a relatively recent Haskell extension that can enforce invariants like "can’t do anything on the database once you call close".

I have a rough sketch in this gist of how your api might look with linear types, but it might contain some errors. It’s easy to inadventently leave loopholes in linear APIs.

Linear types in haskell have some disadvantages:

  • They aren’t widespread, and they aren’t well supported in base. Usually you need to use linear-base instead, especially when dealing with (linear) IO.

  • They have some special idioms. For example, resource allocation is usually done in continuation-passing style to enforce linearity. The Ur type is used to represent “unrestricted” values.

  • Another idiom is that linear functions “thread” the handles that they receive linearly:

    fetch ::
  ByteString ->
  DB m %1 ->
  IO (DB m, Ur (Maybe ByteString))

    And you must continue working with the returned handle, as the one received as input becomes inaccesible. This creates a constant need for new names (or shadowed identifiers).

  • Sometimes type errors aren’t exactly clear.

  • Some constructs like let are not completely supported and require some annoying workarounds.

  • Not sure what is the recommended approach to deal with exceptions in linear IO.

On the good side, I think the linear API would allow you to work with multiple databases without problems.

2 Likes
#6

And you must continue working with the returned handle, as the one received as input becomes inaccesible. This creates a constant need for new names (or shadowed identifiers).

I feel a linear-control Monad could take care of that, and the handle be essentially threaded as if it were an effect.

#7

I feel a linear-control Monad could take care of that, and the handle be essentially threaded as if it were an effect.

Yes. This nice linear quicksort example uses the UrT transformer and a linear state monad to avoid boilerplate (here is the monad-less version). I’m not sure how to extend the technique to multiple simultaneous linear resources, however.

Apparently, adding linear constraints to the language would be another way of reducing the required bureaucracy.

#8

Another option is to separate store updates from store retrievals:

…where the lazy retrieval is accomplished by way of versions:

This separation of concerns may help to limit the proliferation of monadic code in your project…

#9

I would like to jump in and mention that you don’t need to reach out for LinearTypes for some of the stuff. Sometimes, simple Haskell is enough.

For example, to satisfy the following two requirements:

You can provide a single function in the bracket-like style that handles DB open and close:

withDB :: (DB -> IO a) -> IO a

And you don’t provide open and close functions so users can’t misuse them (or you can provide as a part of internal API if people know what they’re doing).

3 Likes
#10 
iHaveEscaped <- withDB pure

You’d have to use the phantom type parameter trick like ST also does:

withDB :: (forall s. DB s -> IO a) -> IO a
6 Likes
#11

Thank you. I’ll dig into linear-base and will try to see how it feels. From what I read so far, it seems like linear types require whole new universe, not unlike python’s async, but hopefully I am wrong.

#12

An alternative might be to not necessarily think about opening/closing a database handle, but instead having the concept of a Transaction that you can run against a database:

data Transaction a
runTransaction :: FilePath -> Transaction a -> IO a
fetch :: ByteString -> Transaction (Maybe ByteString)
store :: ByteString -> ByteString -> Transaction ()

etc.

Essentially we’re intentionally reducing the degrees of freedom in the API to just what we need. This design satisfies:

store can only be called on database open with openWrite

You could inspect the Transaction to see if it contains a call to store.

You should call close as soon you don’t need database anymore.

There is no close here, so you can trust runTransaction to deal with that.

You may not use DB object once you closed it.

Same as above.

Functions firstkey and nextkey allow you to iterate keys, but you may not call store between call of firstkey and nextkey.

The design above doesn’t solve this, but it sounds like firstkey/nextkey is the problematic part, and it would be better to have something like:

foldKeys :: ByteString -> CursorQuery a -> Transaction a

but I don’t really know what keys are in this context so I think you need more domain context to come up with the right design here.

There is a tradeoff in this design, which is that opening/closing the database might be an expensive operation. I think that’s something you would have to evaluate.

2 Likes