Create a gist now

Instantly share code, notes, and snippets.

@edsko /Checked.hs
Last active Oct 26, 2016

Embed
Lightweight checked exceptions in Haskell
{-# LANGUAGE CPP #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
#if __GLASGOW_HASKELL__ >= 710
{-# LANGUAGE AllowAmbiguousTypes #-}
#endif
-- | Lightweight checked exceptions
--
-- See <http://www.well-typed.com/blog/2015/07/checked-exceptions/>.
-- Written by Edsko de Vries. Copyright 2015 Well-Typed LLP.
--
-- Tested with ghc 7.2, 7.4, 7.6, 7.8 and 7.10.
module Checked where
import Control.Exception (Exception, IOException)
import Unsafe.Coerce (unsafeCoerce)
import qualified Control.Exception as E
{-------------------------------------------------------------------------------
Main definitions
-------------------------------------------------------------------------------}
-- | Checked exceptions
class Throws e where
throwChecked :: e -> IO a
-- | Wrap an action that may throw a checked exception
--
-- This is used internally in 'rethrowUnchecked' to avoid impredicative
-- instantiation of the type of 'unsafeCoerce'.
newtype Wrap e a = Wrap (Throws e => IO a)
-- | Rethrow checked exceptions as unchecked (regular) exceptions
rethrowUnchecked :: forall e a. (Throws e => IO a) -> (Exception e => IO a)
rethrowUnchecked act = aux act E.throwIO
where
aux :: (Throws e => IO a) -> ((e -> IO a) -> IO a)
aux = unsafeCoerce . Wrap
-- | Catch a checked exception
--
-- This is the only way to discharge a 'Throws' type class constraint.
catchChecked :: Exception e => (Throws e => IO a) -> (e -> IO a) -> IO a
catchChecked = E.catch . rethrowUnchecked
{-------------------------------------------------------------------------------
Additional definitions
-------------------------------------------------------------------------------}
-- | 'catchChecked' with the arguments reversed
handleChecked :: Exception e => (e -> IO a) -> (Throws e => IO a) -> IO a
handleChecked act handler = catchChecked handler act
-- | Throw an unchecked exception
--
-- This is just an alias for 'throw', but makes it evident that this is a very
-- intentional use of an unchecked exception.
throwUnchecked :: Exception e => e -> IO a
throwUnchecked = E.throwIO
-- | Rethrow IO exceptions as checked exceptions
checkIO :: Throws IOException => IO a -> IO a
checkIO = E.handle $ \(ex :: IOException) -> throwChecked ex
{-------------------------------------------------------------------------------
Example
-------------------------------------------------------------------------------}
readFile' :: Throws IOException => FilePath -> IO String
readFile' = checkIO . readFile
readEtcPasswd :: IO String
readEtcPasswd = catchChecked (readFile' "/etc/passwd") $ \(ex :: IOException) ->
return "Could not read"
@edsko

This comment has been minimized.

Show comment
Hide comment
Owner

edsko commented Aug 14, 2015

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment