Last active
May 10, 2018 20:11
-
-
Save erdeszt/e38ea85eb6f7520e3d5e99fd75520086 to your computer and use it in GitHub Desktop.
Indexed ResourceT monad (repl.it link: https://repl.it/repls/EsteemedDeficientArea)
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE KindSignatures | |
, PolyKinds | |
, DataKinds | |
, TypeFamilies | |
, TypeOperators | |
, GADTs | |
#-} | |
module IxResourceT where | |
class IxMonad (m :: state -> state -> * -> *) where | |
ireturn :: a -> m s s a | |
ibind :: m i o a -> (a -> m o o' b) -> m i o' b | |
data Deallocator m a = Deallocator { runDeallocator :: m () } | |
data IxResourceT :: (* -> *) -> [*] -> [*] -> * -> * where | |
IxResourceT :: m a -> IxResourceT m rsi rso a | |
instance (Monad m) => IxMonad (IxResourceT m) where | |
ireturn = IxResourceT .return | |
(IxResourceT ma) `ibind` f = IxResourceT $ do | |
a <- ma | |
let (IxResourceT mb) = f a | |
mb | |
lift :: (Monad m) => m a -> IxResourceT m rs rs a | |
lift = IxResourceT | |
type family Elem (x :: k) (xs :: [k]) :: Bool where | |
Elem x '[] = 'False | |
Elem x (x ': xs) = 'True | |
Elem x (y ': xs) = Elem x xs | |
type family Remove (x :: k) (xs :: [k]) :: [k] where | |
Remove x '[] = '[] | |
Remove x (x ': xs) = xs | |
Remove x (y ': xs) = Remove x xs | |
allocate :: (Monad m) => (m a, a -> m ()) -> IxResourceT m rs (a ': rs) (a, Deallocator m a) | |
allocate (allocateResource, deallocateResource) = IxResourceT $ do | |
resource <- allocateResource | |
return (resource, Deallocator (deallocateResource resource)) | |
release :: (Monad m, Elem a rs ~ True) => Deallocator m a -> IxResourceT m rs (Remove a rs) () | |
release deallocator = IxResourceT (runDeallocator deallocator) | |
runIxResourceT :: (Monad m) => IxResourceT m '[] '[] a -> m a | |
runIxResourceT (IxResourceT ma) = ma |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE DataKinds | |
, RebindableSyntax | |
#-} | |
module Main where | |
import IxResourceT | |
import qualified Prelude as P | |
import Prelude hiding ((>>=), (>>), return) | |
return :: (Monad m) => a -> IxResourceT m rs rs a | |
return = ireturn | |
(>>=) :: (Monad m) | |
=> IxResourceT m rs rs' a | |
-> (a -> IxResourceT m rs' rs'' b) | |
-> IxResourceT m rs rs'' b | |
(>>=) = ibind | |
(>>) :: (Monad m) | |
=> IxResourceT m rs rs' a | |
-> IxResourceT m rs' rs'' b | |
-> IxResourceT m rs rs'' b | |
ma >> mb = ma >>= \_ -> mb | |
-- Can't run it with runIxResourceT because Int resource is not cleaned up | |
ixResourceTEx1 :: IxResourceT IO '[] '[Int] () | |
ixResourceTEx1 = do | |
allocate (allocateInt 2, releaseInt) | |
return () | |
ixResourceTEx2 :: IxResourceT IO '[] '[] () | |
ixResourceTEx2 = do | |
(intResource, releaseIntResource) <- allocate (allocateInt 2, releaseInt) | |
(strResource, releaseStrResource) <- allocate (allocateString "asd", releaseString) | |
lift (print $ "Acquired resource: " ++ show intResource) | |
-- release (Deallocator (P.return ()) :: Deallocator IO Double) -- Doesn't work because no Doubles to free | |
release releaseStrResource | |
-- release (Deallocator (P.return ()) :: Deallocator IO String) -- Doesn't work because no more Strings to free | |
release releaseIntResource | |
allocateInt :: Int -> IO Int | |
allocateInt n = print ("Allocating[Int]: " ++ show n) P.>> P.return n | |
releaseInt :: Int -> IO () | |
releaseInt n = print ("Releasing[Int]: " ++ show n) P.>> P.return () | |
main :: IO () | |
main = runIxResourceT ixResourceTEx2 |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment