eio: IO with Exceptions tracked on the type-level

This is a package candidate release! Here you can preview how this package release will appear once published to the main package index (which can be accomplished via the 'maintain' link below). Please note that once a package has been published to the main package index it cannot be undone! Please consult the package uploading documentation for more information.

[maintain] [Publish]

IO with Exceptions tracked on the type-level. See README.md for more details.


[Skip to Readme]

Properties

Versions 0.0.0.0, 0.0.0.0
Change log CHANGELOG.md
Dependencies base (>=4.15.0.0 && <4.16), eio [details]
License MPL-2.0
Copyright 2021 Kowainik
Author Kowainik
Maintainer Kowainik <xrom.xkov@gmail.com>
Category Exceptions, IO, QualifiedDo
Home page https://github.com/kowainik/eio
Bug tracker https://github.com/kowainik/eio/issues
Source repo head: git clone https://github.com/kowainik/eio.git
Uploaded by shersh at 2021-03-20T16:28:42Z

Modules

Downloads

Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees


Readme for eio-0.0.0.0

[back to package description]

eio

GitHub CI Hackage MPL-2.0 license

IO with Exceptions tracked on the type-level.

Note: The package is considered to be used with the QualifiedDo feature, so hence the support only of GHC-9.0 and upper.

Usage example

Since this is a literate haskell file, we need to specify all our language extensions and imports up front.

{-# LANGUAGE QualifiedDo #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE DeriveAnyClass #-}

It is recomended to use eio library qualified, as it reimplements many standard functions.

import Control.Exception (Exception)
import EIO (EIO)

import qualified EIO

Let's also define our own exception to play with:

data MyErr = MyErr
    deriving stock (Show)
    deriving anyclass (Exception)

The main function of our module will look like this:

main :: IO ()
main = EIO.runEIO safeMain

Let's now write the safe main function that should not have any exceptions pushed to the actual main function, as the list of exceptions on type level should be empty.

This means, that if we throw the exception inside but don't handle it properly, it won't type check, as the list of exceptions in EIO will contain at least one element:

-- - Type error!
safeMainWrong :: EIO '[] ()
safeMainWrong = EIO.do
    EIO.throw MyErr

And the error will exactly point out to the fact that the empty list is expected, but got non-empty instead:

error:
    • Couldn't match type: '[MyErr]
                     with: '[]
      Expected: EIO '[] ()
        Actual: EIO '[MyErr] ()
    • In a stmt of a qualified 'do' block: EIO.throw MyErr
      In the expression: EIO.do EIO.throw MyErr
      In an equation for ‘safeMain’: safeMain = EIO.do EIO.throw MyErr
   |
xx |     EIO.throw MyErr
   |     ^^^^^^^^^^^^^^^

In order for it to type check, we need to handle each thrown exception properly, so that you have an empty list in the end:

safeMain :: EIO '[] ()
safeMain = EIO.do
    EIO.return ()
    EIO.throw MyErr `EIO.catch` (\MyErr -> EIO.return ())