{-# OPTIONS_GHC -w #-} {-# LANGUAGE RebindableSyntax, NoImplicitPrelude #-} -- | -- Module : Control.Delimited.Tutorial -- Copyright : (c) Oleg Kiselyov 2007-2013, (c) Austin Seipp 2012-2013 -- License : MIT -- -- Maintainer : mad.one@gmail.com -- Stability : experimental -- Portability : portable -- -- This module provides an introductory tutorial in the -- \"Introduction\" section and beyond, followed by examples. Finally, -- there's some discussion behind the theory and design of the -- library, with references. -- module Control.Delimited.Tutorial ( -- * Introduction -- $intro -- * An primer on continuations -- $callcc-primer -- ** Delimited -- $primer-delimcc -- * Examples -- $examples -- ** Simple answer-type modification -- $example-simple -- ** First-class @printf@ -- $example-printf -- ** Walking binary trees -- $example-btrees -- * Other notes -- $othernotes -- ** Indexed monads -- $pmonads -- ** Using @do@-notation -- $donotation -- ** Rank-2 typing -- $rankntypes -- * Further reading -- $morereading -- * References -- $refs ) where import Control.Indexed.Prelude import Control.Delimited {- $intro @asai@ is a minimal library for /delimited continuations/, a \'slice\' of a continuation that can be invoked as a function and composed. -} {- $callcc-primer Continuations are a well known abstraction for 'picking up where you left off.' When you use @call/cc@ traditionally in something like scheme, you pass it a function @f@ which receives a function @k@, and when @k@ is invoked you 'call the continuation' and return where @call/cc@ left off. In this sense, @k@ is a reification of the state you were in when you invoked @f@. But there is another type of continuation: a delimited one. With delimited continuations, it is possible to exert control over the exact /frame/ of the computation that is captured. By being able to slice just small execution contexts, we can compose delimited continuations very easily. In the same way that continuations form a monad, so do delimited continuations. This package provides a delimited continuation monad which implements truly polymorphic @shift@ and @reset@ operators, via /answer type polymorphism/, which allows the results of a delimited computation to vary. This implementation (using indexed monads) was first implemented by - and this package derived from - Oleg Kiselyov [1]. It directly implements the typing rules of Kenichi Asai's lambda/shift calculus [2], featuring answer type polymorphism and modification. A general tutorial on delimited continuations in OchaCaml (with code in Haskell and OCaml) from Asai/Kiselyov is available [3]. A more traditional delimited continuation monad is available in the @CC-delcont@ package [4]. The @CC-delcont@ tutorial [5] serves as a basis for this tutorial (thanks to Dan Doel!) -} {- $primer-delimcc Let us consider the expression: -} {- $examples In the subsequent sections, we'll cover some examples of using this library in a few simple forms, which should form a basis for reasoning about how to use it. The same ideas should apply to other delimited continuation libraries or interfaces (i.e. scheme, ocaml, ochacaml, etc.) -} {- $example-simple Basic answer type modification is very simple to demonstrate. Consider that we @shift@ some computation and discard the continuation @k@. Then the answer type of the enclosing @'reset'@ changes to the return type of the @shift@ed block. For example: >>> runDelim $ reset $ shift2 (\_ -> returnI "hello") !>>= \r -> returnI (r + 1) "hello" Here, the initial answer type of the enclosing @'reset'@ is initially @Int@, because the return of the reset is @Int@. However, we use @'shift2'@, which changes the answer type by /discarding/ the delimited continuation, and simply returning a @'String'@. On the other hand, it is also clear when the answer type is polymorphic and cannot be changed. Instead consider this example: >>> :t runDelim $ reset $ shift2 (\k -> returnI k) !>>= \r -> returnI (r + (1::Int)) runDelim $ reset $ shift2 (\k -> returnI k) !>>= \r -> returnI (r + (1::Int)) :: Int -> Delim s s Int Here, the answer type is /not/ changed by the call to @'shift2'@: the continuation k is not discarded, but returned. This \'carries'\ the answer type variables with the value, enforcing the input and output answer types are the same. And so if we were to invoke @k@, then the answer type of the @'reset'@ may still only be 'Int': that is the only type of value we may place in the hole left by @'shift2'@. -} {- $example-printf We will now write a simple, typesafe @printf@ function using delimited continuations. The key observation is that when we write a term like: @ printf \"foo %s bar %d\" x y @ we are actually filling in /holes/ in place of the @%s@ and @%d@ specifiers. Instead, we can write a type safe formatter that 'fills in' the holes correctly by construction. Let us first define formatting functions that will properly convert arguments to a @'String'@. The trivial one for a @'String'@ itself is obvious: @ str :: String -> String str = id @ We may also write one for @'Int'@s: @ int :: Int -> String int = show @ We observe that a call to @printf@ is similar to delimiting the computation of the format string argument. So we define @printf@ as: @ printf p = 'reset' p @ Now we will define a type-safe formatter, that will \'plug\' the value into our string properly: @ fmt to = 'shift2' (\\k -> 'returnI' (k . to)) @ When we call @fmt@, we will /abort/ back to the enclosing @'reset'@, returning a function. The function is @k . to@, which will convert our value to a @'String'@ and plug it into the enclosing hole that @fmt@ left behind. Now we will define some operators for chaining these function returns, and concatenating the string results: @ f $$ x = f '!>>=' ($ x) infixl 1 $$ f ^$ g = 'liftIxM2' (++) f g run = 'runDelim' @ Now, we can write: @ test1 :: String test1 = run $ printf ('returnI' \"hello world!\") @ And more interestingly: @ test2 :: String test2 = run $ sprintf (fmt int) $$ 1 @ We may also format multiple arguments in a type safe manner, by concatenating the formatters with @^$@ and passing arguments via @$$@: @ test3, test4 :: String test3 = run $ sprintf ('returnI' \"goodbye \" ^$ fmt str ^$ 'returnI' \"!\") $$ \"world\" test4 = run $ sprintf (fmt str ^$ 'returnI' \" = \" ^$ fmt int) $$ \"x\" $$ 3 @ It is an error to pass a value of an incorrect type to the corresponding formatter. The full code is available in @examples/Printf.hs@. -} {- $example-btrees Here, we will... @ [-\# LANGUAGE RankNTypes \#-] module Tree where import Control.Delimited \-- Binary trees data Tree a = Leaf | Node (Tree a) (Tree a) a deriving (Show, Eq) make_tree :: Int -> Tree Int make_tree j = go j 1 where go 0 _ = Leaf go i x = Node (go (i-1) $ 2*x) (go (i-1) $ 2*x+1) x tree1 = make_tree 3 tree2 = make_tree 4 \-- Coroutines as monadic lists. data Coro a = Done | Resume a (forall s. 'Delim' s s (Coro a)) walk_tree x = 'runDelim' (walk_tree' x '!>>' 'returnI' Done) walk_tree' Leaf = 'returnI' () walk_tree' (Node l r x) = walk_tree' l '!>>' yield x '!>>' walk_tree' r where yield n = 'shift2' (\\k -> 'returnI' $ Resume n $ k ()) walk1 :: Show a => Tree a -> IO () walk1 t = go (walk_tree t) where go Done = return () go (Resume x k) = print x >> go ('runDelim' k) @ The full code is available in @examples/Tree.hs@. -} {- $othernotes Here we discuss some of the design aspects of the library, particularly for those wondering why we need indexed (or /indexed/) monads, and how we can reconcile this with @do@-notation. -} {- $pmonads While reading this tutorial, you may wonder why we use special operators (like '!>>=' that mimmick 'Prelude.>>=') for delimited computations, instead of regular operators from the 'Monad' typeclass. The reason for this is that in order to ensure the answer type of delimited computation is polymorphic, we need the monad to \'carry\' the answer types around. Consider the vanilla 'Monad' typeclass. It is defined like this (with explicit kind signatures): @ class 'Monad' (m :: * -> *) where ... @ The @m@ type constructor abstracts over a single type variable. It is possible to make types with multiple type variables an instance of 'Monad' of course, but their non-abstracted type variables must be fixed. As an example, considering the instance for @'Either' e@: @ instance 'Monad' ('Either' e) where ... @ Note the type variable @e@ is fixed over the definition of a term of type @'Either' e :: * -> *@. If you have something like: @ thing :: a -> 'Either' String a thing a = do ... @ Then in the body we may say: @ x <- Left \"oh no!\" @ But we can never say: @ x <- Left False @ because @e@ is fixed to 'String'. Another example is that the 'Control.Monad.State.State' monad always has a fixed state type, and it may never change over the course of the computation. Indexed monads solve this problem by \'expanding\' the kind of @m@ in the 'Monad' typeclass. The result is 'IxMonad', which is defined as: @ class 'IxMonad' (m :: * -> * -> * -> *) where 'returnI' :: t -> m a a t ('!>>=') :: m b g s -> (s -> m a b t) -> m a g t @ Note the new type variables: these represent the input and output answer types of a delimited computation. We can see that 'returnI' is fully polymorphic in its answer type: a statement of @returnI foo@ in a 'Delim' simply does not change the answer type at all. Note the answer types present in 'Control.Indexed.Monad.!>>=': we have an answer type of @a b@ and @b g@, meaning we can get an overall answer type of @a g@. This polymorphism in the definition of 'Control.Indexed.Monad.!>>=' is what gives us answer type polymorphism: it means delimited computations may change the output answer type. -} {- $donotation It's possible to use GHC's @RebindableSyntax@ extension to re-define @do@ notation to use the 'IxMonad' type class. Begin your module by hiding the regular 'Monad' methods, and then redefine 'Prelude.>>=' and 'Prelude.return'. Feel free to redefine other operators too. Here's an example (you'll need to fix the @LANGUAGE@ pragma yourself on the first line, since Haddock eats it otherwise): @ [-\# LANGUAGE RebindableSyntax \#-] module Foo where import Control.Indexed.Prelude import Control.Delimited \-- After importing the indexed prelude, we can use do notation \-- Lifting ordinary monads io1 :: IO () io1 = 'runI' $ do 'lift' $ putStrLn \"hi!\" 'lift' $ putStrLn \"hi!\" return () test1 :: String test1 = 'runDelim' $ 'reset' $ do r <- 'shift1' (const $ return \"hello\") return (r + 1) \-- This is equivalent to the OchaCaml term: \-- reset (fun () -> 1 + shift (fun _ -> \"hello\")) ;; @ See @examples/Simple.hs@ (included in the distribution) for several more examples. -} {- $rankntypes This package requires GHC's @RankNTypes@ extension, as it uses a rank-2 type for the definition of the @shift@ operators 'shift2' and 'shift3'. The original implementation by Kiselyov is Haskell98 (he defines @shift@ as the 'shift1' provided in this package, as opposed to 'shift2' which matches the typing rules of the lambda/shift calculus.) Strictly speaking, the rank-2 type is probably not necessary, but it is not very controversial either, and it makes the intent much clearer. For a lot of cases, you will need to use @RankNTypes@ if you want to abstract over the answer type variables properly (for example, in a recursive data structure.) -} {- $morereading Lorem ipsum... -} {- $refs 1. /Genuine shift\reset in Haskell98/, by Kiselyov, on /haskell-cafe/: <http://okmij.org/ftp/continuations/implementations.html#genuine-shift> 2. /Polymorphic Delimited Continuations/, by Asai, Kameyama in /APLAS '07/: <http://logic.cs.tsukuba.ac.jp/~kam/paper/aplas07.pdf> 3. /Introduction to programming with shift and reset/, by Kiselyov, Asai, in /CW2011/: <http://okmij.org/ftp/continuations/index.html#tutorial> 4. /CC-delcont: Delimited continuations and dynamically scoped variables/: <http://hackage.haskell.org/package/CC-delcont> 5. /CC-delcont introduction/: <http://www.haskell.org/haskellwiki/Library/CC-delcont#CC-delcont> -}