gistfile1.hs

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

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

newtype Throws (es :: [k]) a = Throws (IO a)


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 Insert (e :: k) (es :: [k]) :: [k] where
  Insert e (e  ': es) = e ': es
  Insert e (e' ': es) = e' ': (Insert e es)
  Insert e '[] = '[e]
  
type family Merge (xs :: [k]) (ys :: [k]) :: [k] where
  Merge es '[] = es
  Merge ls (r ': rs) = Insert r (Merge ls rs)



-- class Error (s::Symbol)    -- No instances

-- type family Remove (e :: k) (es :: [k]) :: [k] where
--   Remove e (e  ': es) = es
--   Remove e (e' ': es) = e' ': (Remove e es)
--   Remove e '[] = Error "Remove: type not found in list"

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

testFalse :: Throws '[Bool, Char] a
testFalse = undefined

testTrue :: Throws '[Bool, Char, Int] a
testTrue = undefined

catch' :: (Exception e, Contains e es, Delete e es ~ es', Exceptions es)
       => Throws es a -> (e -> IO a) -> Throws es' a
catch' (Throws e) f = Throws (catch e f)

catchAll' :: Throws es a -> (SomeException -> IO a) -> Throws '[] a
catchAll' (Throws e) f = Throws (catch e f)

catch'' :: (Contains e es, Delete e es ~ es') => Throws es a -> (e -> IO a) -> Throws es' a
catch'' (Throws e) f = undefined

throw' :: (Exception e) => e -> Throws '[e] a
throw' e = Throws (throw e)

(>>==) :: Throws es a -> (a -> Throws es' b) -> Throws (Merge es es') b
(Throws i) >>== f = Throws $ do
  a <- i
  let (Throws i') = f a
  i'

execute :: Throws '[] a -> IO a
execute (Throws i) = i

liftClean :: IO a -> Throws '[] a
liftClean i = Throws i

liftDirty :: forall (es :: [k]) a. IO a -> Throws es a
liftDirty i = Throws i