Tracked Exceptions.hs

{-# LANGUAGE ConstraintKinds, DataKinds, PolyKinds, TypeFamilies, 
  TypeOperators, RankNTypes, TypeFamilies, UndecidableInstances #-}

import GHC.Prim (Constraint)
import Control.Exception -- (Exception, SomeException, catch, throw)
import Control.Monad (ap)



type family If (b :: Bool) :: Constraint where
  If 'True  = ()
  If 'False = ("Error" ~ "If: False")

type family Contains (e :: k) (es :: [k]) :: Constraint where
  Contains e (e ': es) = ()
  Contains x (e ': es) = Contains x es
  Contains x '[] = ("Error" ~ "Exception not found in thrown exceptions")

type family DoesntContain (e :: k) (es :: [k]) :: Constraint where
  DoesntContain e (e ': es) = ("Error" ~ "DoesntContain: type found in list when it wasn't expected")
  DoesntContain x (e ': es) = DoesntContain x es
  DoesntContain x '[] = ()

type family Exceptions (es :: [k]) :: Constraint where
  Exceptions '[] = ()
  Exceptions (e ': es) = (Exception e, Exceptions es)
  
type family AllInClass (c :: k -> Constraint) (xs :: [k]) :: Constraint where
  AllInClass c '[] = ()
  AllInClass c (x ': xs) = (c x, AllInClass c xs)

type family InClasses (a :: k) (cs :: [k -> Constraint]) :: Constraint where
  InClasses a (c ': cs) = (c a, InClasses a cs)
  InClasses a '[] = ()

type family Insert (e :: k) (es :: [k]) :: [k] where
  Insert e (e  ': es) = e ': es
  Insert x (e ': es) = e ': (Insert x es)
  Insert x '[] = '[x]

type family Concat (es :: [k]) (fs :: [k]) :: [k] where
  Concat es '[] = es
  Concat es (f ': fs) = Concat (Insert f es) fs

type family Merge (xs :: [k]) (ys :: [k]) :: [k] where
  Merge es '[] = es
  Merge ls (r ': rs) = Merge (Insert r ls) rs

type family Delete (e :: k) (es :: [k]) :: [k] where
  Delete e (e  ': es) = es
  Delete x (e ': es) = e ': (Delete x es)
  Delete x '[] = '[]

-- openFile :: Throws '[FilenotfoundException, PermissionError] String

type CommonExceptions = 
  '[ArithException
  , ErrorCall
  , PatternMatchFail
  , ArrayException
  ]


newtype ThrowsI i j a = ThrowsI (IO a)

instance IxFunctor ThrowsI where
  imap f (ThrowsI i) = ThrowsI (fmap f i)
  
instance IxPointed ThrowsI where
  ireturn x = ThrowsI (return x)

instance IxApplicative ThrowsI where
  iap (ThrowsI fi) (ThrowsI ai) = ThrowsI (ap fi ai)

instance IxMonad ThrowsI where
  -- ibind :: (a -> ThrowsI j k b) -> ThrowsI i j a -> ThrowsI i k b
  ibind f (ThrowsI i) = ThrowsI $ do
    x <- i
    let ThrowsI r = f x
    r

type Throwing e es a = Throws es (Insert e es) a

test0 :: ThrowsI es es a
test0 = undefined

test1 :: ThrowsI es (Insert ArithException es) a
test1 = undefined

test2 :: ThrowsI es (Insert NonTermination es) a
test2 = undefined

test3 :: ThrowsI es (Insert PatternMatchFail es) a
test3 = undefined


catch'' :: (Contains e es, Exception e) => ThrowsI fe es a -> (e -> IO a) -> ThrowsI fe (Delete e es) a
catch'' (ThrowsI i) h = ThrowsI (catch i h)


throw'' :: (Exception e) => e -> ThrowsI es (Insert e es) a
throw'' e = ThrowsI (throw e)

try'' :: (Contains e es, Exception e) => ThrowsI fs es a -> ThrowsI fs (Delete e es) (Either e a)
try'' (ThrowsI i) = ThrowsI (try i)

runSafe :: ThrowsI CommonExceptions '[] a -> IO a
runSafe (ThrowsI i) = i >>= evaluate

runUnsafe :: ThrowsI fs es a -> IO a
runUnsafe (ThrowsI i) = i >>= evaluate


-- ============ Control.Monad.Indexed =========

class IxFunctor f where
	imap :: (a -> b) -> f j k a -> f j k b

class IxPointed m => IxApplicative m where
	iap :: m i j (a -> b) -> m j k a -> m i k b

class IxFunctor m => IxPointed m where
        ireturn :: a -> m i i a

class IxFunctor w => IxCopointed w where
	iextract :: w i i a -> a

class IxApplicative m => IxMonad m where
	ibind :: (a -> m j k b) -> m i j a -> m i k b


ijoin :: IxMonad m => m i j (m j k a) -> m i k a 
ijoin = ibind id

infixr 1 =<<<
infixl 1 >>>=

(>>>=) :: IxMonad m => m i j a -> (a -> m j k b) -> m i k b
m >>>= k = ibind k m 

(=<<<) :: IxMonad m => (a -> m j k b) -> m i j a -> m i k b
(=<<<) = ibind

iapIxMonad :: IxMonad m => m i j (a -> b) -> m j k a -> m i k b
iapIxMonad f x = f >>>= \ f' -> x >>>= \x' -> ireturn (f' x')

-- ============= End Control.Monad.Indexed =========