Skip to content

Instantly share code, notes, and snippets.

@ajhager

ajhager/cont.ipkg

Created May 7, 2014 05:34
Show Gist options
  • Save ajhager/f47143474b3c2e0323b2 to your computer and use it in GitHub Desktop.
Save ajhager/f47143474b3c2e0323b2 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
cont.ipkg
package cont
modules = main
opts = "--codegen javascript -o cont.js"
Raw
index.html
<!DOCTYPE html>
<html>
<head>
<title>Idris Continuation Monad</title>
</head>
<body>
<script type="text/javascript" src="cont.js"></script>
</body>
</html>
Raw
main.idr
module Main
record ContT : Type -> (Type -> Type) -> Type -> Type where
CT : {m : Type -> Type} ->
(runContT : (a -> m r) -> m r) -> ContT r m a
liftContT : Monad m => m a -> ContT r m a
liftContT m = CT (\x => m >>= x)
instance Functor f => Functor (ContT x f) where
map f (CT g) = CT $ \c => g (\a => c (f a))
instance Monad f => Applicative (ContT x f) where
pure r = CT $ \ret => ret r
(CT mf) <$> (CT mx) = CT $ \ret => mf (\f => mx (\x => ret (f x)))
instance Monad m => Monad (ContT r m) where
(CT f) >>= k = CT $ \c => f (\a => do let CT ka = k a; ka c)
Deferred : Type -> Type
Deferred a = ContT () IO a
sync : (t -> (a -> IO r) -> IO r) -> t -> ContT r IO a
sync m a = CT $ \c => m a c
setTimeout : Float -> (() -> IO ()) -> IO ()
setTimeout t f = do
e <- mkForeign (FFun "setTimeout(%0,%1)" [FFunction FUnit (FAny (IO ())), FFloat] FInt) f t
return ()
demo : Deferred ()
demo = do
liftContT $ putStrLn "Start!"
sync setTimeout 1000
liftContT $ putStrLn "Middle!"
sync setTimeout 2000
liftContT $ putStrLn "End!"
main : IO ()
main = runContT demo (const (return ()))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment