Difference between revisions of "The Monad.Reader/Issue2/FunWithLinearImplicitParameters"
(halfhearted fmt attempt) 

Line 2:  Line 2:  
[[User:WouterSwierstraWouterSwierstra]] 14:12, 9 May 2008 (UTC) 
[[User:WouterSwierstraWouterSwierstra]] 14:12, 9 May 2008 (UTC) 

+  [attachment:Reflection.pdf PDF version of this article] 

−  [attachment:Reflection.pdf PDF version of this article] 

−  {{{ }}} 

[attachment:Reflection.tar.gz Code from the article] 
[attachment:Reflection.tar.gz Code from the article] 

−  {{{ }}} 

[:IssueTwo/FeedBack/FunWithLinearImplicitParameters: Feedback] 
[:IssueTwo/FeedBack/FunWithLinearImplicitParameters: Feedback] 

 
 

−  = 
+  =Fun with Linear Implicit Parameters= 
−  == 
+  ==Monadic Reflection in Haskell== 
''by [:ThomasJ‰ger:Thomas J‰ger] for The Monad.Reader [:IssueTwo:Issue Two]'' 
''by [:ThomasJ‰ger:Thomas J‰ger] for The Monad.Reader [:IssueTwo:Issue Two]'' 

[[BR]] 
[[BR]] 

Line 21:  Line 19:  
In this article, we take the next step of impure programming by implementing 
In this article, we take the next step of impure programming by implementing 

−  Filinski's 
+  Filinski's <haskell>reflect</haskell> and <haskell>reify</haskell> functions for a wide class of monads. 
−  
−  == Introduction == 

+  ==Introduction== 

The following sections provide a short introduction into the various concepts 
The following sections provide a short introduction into the various concepts 

our implementation uses. You can download the implementation and the examples 
our implementation uses. You can download the implementation and the examples 

from the article [attachment:Reflection.tar.gz here], it has been successfully 
from the article [attachment:Reflection.tar.gz here], it has been successfully 

tested with ghc6.2.2 and ghc6.4. The examples of this article can be found 
tested with ghc6.2.2 and ghc6.4. The examples of this article can be found 

−  in the file 
+  in the file <haskell>Article.hs</haskell>, the implementation of the library in 
−  +  <haskell>Reflection.hs</haskell>. 

−  === 
+  ===Shift and Reset=== 
−  The 
+  The <haskell>shift</haskell> and <haskell>reflect</haskell> control operators provide a way to manipulate 
delimited continuations, which are similar to the undelimited continuation the 
delimited continuations, which are similar to the undelimited continuation the 

−  familiar 
+  familiar <haskell>call/cc</haskell> uses, but more powerful. There are more detailed 
−  descriptions available e.g. in Danvy & Filinski [[#ref1 1]] and Shan 
+  descriptions available e.g. in Danvy & Filinski [[#ref1 1]] and Shan 
[[#ref2 2]]; moreover, Dybvig, Peyton Jones, Sabry [[#ref3 3]] give a unifying 
[[#ref2 2]]; moreover, Dybvig, Peyton Jones, Sabry [[#ref3 3]] give a unifying 

treatment of various forms of other "subcontinuations". 
treatment of various forms of other "subcontinuations". 

−  Instead of capturing an undelimited continuation as 
+  Instead of capturing an undelimited continuation as <haskell>call/cc</haskell>, <haskell>shift</haskell> 
−  only captures the subcontinuation/context up to the the next 
+  only captures the subcontinuation/context up to the the next <haskell>reset</haskell>, and 
reifies it into a function value. The result of the evaluation of the body then 
reifies it into a function value. The result of the evaluation of the body then 

−  becomes the result of the 
+  becomes the result of the <haskell>reset</haskell>. For example in 
−  +  <haskell>#!syntax haskell 

reset (1 + shift (\k > k 1 + k 2)) :: Int 
reset (1 + shift (\k > k 1 + k 2)) :: Int 

−  }}} 

+  </haskell> 

−  the context of 
+  the context of <haskell>shift</haskell> is <haskell>k = \x > x + 1</haskell>, so the expression 
−  evaluates to 
+  evaluates to <haskell>k 1 + k 2 = 2 + 3 = 5</haskell>. 
−  The interpretation of 
+  The interpretation of <haskell>shift</haskell> and <haskell>reset</haskell> is very easy in the 
continuation monad. 
continuation monad. 

−  +  <haskell>#!syntax haskell 

 An action in the continuation monad maps a continuation, 
 An action in the continuation monad maps a continuation, 

 i.e the "rest" of the computation, to a final result of type r. 
 i.e the "rest" of the computation, to a final result of type r. 

Line 56:  Line 55:  
instance Functor (Cont r) where { ... } 
instance Functor (Cont r) where { ... } 

−  instance Monad 
+  instance Monad (Cont r) where { ... } 
 NB. In the attached Article.hs file, these are called shiftC and resetC. 
 NB. In the attached Article.hs file, these are called shiftC and resetC. 

Line 66:  Line 65:  
 The above example written in monadic style 
 The above example written in monadic style 

−  *Main> reset $ (1 +) `fmap` shift (\k > return $ k 1 + k 2) 
+  * Main> reset $ (1 +) `fmap` shift (\k > return $ k 1 + k 2) 
5 
5 

−  }}} 

+  </haskell> 

−  As we can see, 
+  As we can see, <haskell>reset e</haskell> delimits all effects of <haskell>e</haskell> and returns a pure 
−  value; 
+  value; <haskell>shift</haskell> lets us explicitly construct the mapping from continuations 
−  to final results, so it is very similar to the data constructor 
+  to final results, so it is very similar to the data constructor <haskell>Cont</haskell>. 
−  Therefore 
+  Therefore <haskell>shift</haskell> and <haskell>reset</haskell> give us full control over the underlying 
−  continuation monad and are thereby strictly more expressive than 
+  continuation monad and are thereby strictly more expressive than <haskell>call/cc</haskell>, 
−  which is polymorphic in the answer type 
+  which is polymorphic in the answer type <haskell>r</haskell>. 
−  To treat the directstyle 
+  To treat the directstyle <haskell>shift</haskell> and <haskell>reset</haskell> safely in a typed 
setting, it is necessary to express the answer type of the underlying 
setting, it is necessary to express the answer type of the underlying 

continuation monad in the types. The HindleyMilner type system cannot express 
continuation monad in the types. The HindleyMilner type system cannot express 

Line 84:  Line 83:  
Filinski's implementation in SML. 
Filinski's implementation in SML. 

−  === 
+  ===Monadic Reflection=== 
Monadic reflection [[#ref4 4]] enables us to write monadic code in direct style. 
Monadic reflection [[#ref4 4]] enables us to write monadic code in direct style. 

−  +  <haskell>reflect</haskell> "reflects" a monadic value into a firstclass value of our 

language. The side effects can then be observed by "reifing" a value back into 
language. The side effects can then be observed by "reifing" a value back into 

−  monadic form. 
+  monadic form. For example, 
−  +  <haskell>#!syntax haskell 

> reify (reflect [0,2] + reflect [0,1]) :: [Int] 
> reify (reflect [0,2] + reflect [0,1]) :: [Int] 

and 
and 

> liftM2 (+) [0,2] [0,1] 
> liftM2 (+) [0,2] [0,1] 

−  }}} 

+  </haskell> 

−  both yield the same result, namely 
+  both yield the same result, namely <haskell>[0,1,2,3]</haskell> 
In order to understand how monadic reflection can be implemented, we combine 
In order to understand how monadic reflection can be implemented, we combine 

−  the observation that 
+  the observation that <haskell>shift</haskell> and <haskell>reset</haskell> give us the full power over an 
underlying continuation monad with an arbitrary answer type with Wadler's 
underlying continuation monad with an arbitrary answer type with Wadler's 

[[#ref5 5]] observation that every monad can be embedded in the continuation 
[[#ref5 5]] observation that every monad can be embedded in the continuation 

−  monad. So using a directstyle 
+  monad. So using a directstyle <haskell>shift</haskell> and <haskell>reset</haskell>, we can write 
arbitrary monadic code in direct style. 
arbitrary monadic code in direct style. 

Explicitly (but hiding the wrapping necessary for the ContT monad 
Explicitly (but hiding the wrapping necessary for the ContT monad 

transformer), Wadler's transformation is as follows 
transformer), Wadler's transformation is as follows 

−  +  <haskell>#!syntax haskell 

embed :: Monad m => m a > (forall r. (a > m r) > m r) 
embed :: Monad m => m a > (forall r. (a > m r) > m r) 

embed m = \k > k =<< m 
embed m = \k > k =<< m 

Line 112:  Line 111:  
project :: Monad m => (forall r. (a > m r) > m r) > m a 
project :: Monad m => (forall r. (a > m r) > m r) > m a 

project f = f return 
project f = f return 

−  }}} 

+  </haskell> 

−  Here, 
+  Here, <haskell>project . embed === id</haskell> and the property of <haskell>embed</haskell> and 
−  +  <haskell>project</haskell> constituting monad morphisms between the monad <haskell>m</haskell> and the 

−  monad 
+  monad <haskell>forall r. ContT m r a</haskell> can easily be checked. 
Translating these morphisms into direct style, we immediately arrive at 
Translating these morphisms into direct style, we immediately arrive at 

−  Filinski's 
+  Filinski's <haskell>reflect</haskell> and <haskell>reify</haskell> operations 
−  +  <haskell>#!syntax haskell 

reflect m = shift (\k > k =<< m) 
reflect m = shift (\k > k =<< m) 

reify t = reset (return t) 
reify t = reset (return t) 

−  }}} 

+  </haskell> 

Now let us have a closer look at the above example to see how it works 
Now let us have a closer look at the above example to see how it works 

operationally. 
operationally. 

−  +  <haskell>#!syntax haskell 

e = reify (reflect [0,2] + reflect [0,1]) 
e = reify (reflect [0,2] + reflect [0,1]) 

−  }}} 

+  </haskell> 

Substituting the definitions, this becomes 
Substituting the definitions, this becomes 

−  +  <haskell>#!syntax haskell 

e = reset (return (shift (\k > k =<< [0,2]) + shift (\k > k =<< [0,1]))) 
e = reset (return (shift (\k > k =<< [0,2]) + shift (\k > k =<< [0,1]))) 

−  }}} 

+  </haskell> 

which simplifies to 
which simplifies to 

−  +  <haskell>#!syntax haskell 

e = reset [shift (\k > k 0 ++ k 2) + shift (\k' > k' 0 ++ k' 1)] 
e = reset [shift (\k > k 0 ++ k 2) + shift (\k' > k' 0 ++ k' 1)] 

−  }}} 

+  </haskell> 

Assuming left to right evaluation, the result of this expression is 
Assuming left to right evaluation, the result of this expression is 

−  +  <haskell>k 0 ++ k 2</haskell> where <haskell>k</haskell> is bound to the subcontinuation 

−  +  <haskell>#!syntax haskell 

k = \x > reset [x + shift (\k' > k' 0 ++ k' 1)] 
k = \x > reset [x + shift (\k' > k' 0 ++ k' 1)] 

−  }}} 

+  </haskell> 

−  Again, in this term, 
+  Again, in this term, <haskell>k'</haskell> is bound to <haskell>\y > reset [x + y]</haskell>, so <haskell>k</haskell> is the function 
−  +  <haskell>#!syntax haskell 

k = \x > [x + 0] ++ [x + 1] = \x > [x,x+1] 
k = \x > [x + 0] ++ [x + 1] = \x > [x,x+1] 

−  }}} 

+  </haskell> 

Therefore, as we expected, the whole expression evaluates to 
Therefore, as we expected, the whole expression evaluates to 

−  +  <haskell>#!syntax haskell 

e = k 0 ++ k 2 = [0,1] ++ [2,3] = [0,1,2,3] 
e = k 0 ++ k 2 = [0,1] ++ [2,3] = [0,1,2,3] 

−  }}} 

+  </haskell> 

−  === 
+  ===Implicit Parameters=== 
Implicit parameters [[#ref6 6]] are GHCspecific type system extension 
Implicit parameters [[#ref6 6]] are GHCspecific type system extension 

providing dynamically bound variables. They are passed in the same way as type 
providing dynamically bound variables. They are passed in the same way as type 

Line 159:  Line 158:  
expects appear in type contexts which now make sense at arbitrary argument 
expects appear in type contexts which now make sense at arbitrary argument 

positions. 
positions. 

−  +  <haskell>#!syntax haskell 

addThree :: (?foo :: Int) => Int 
addThree :: (?foo :: Int) => Int 

addThree = 3 + ?foo 
addThree = 3 + ?foo 

Line 165:  Line 164:  
withFour :: ((?foo :: Int) => a) > a 
withFour :: ((?foo :: Int) => a) > a 

withFour x = let ?foo = 4 in x 
withFour x = let ?foo = 4 in x 

−  
+  * Main> withFour addThree 

−  *Main> withFour addThree 

7 
7 

−  }}} 

+  </haskell> 

We see that implicit parameters act like a reader monad written in direct 
We see that implicit parameters act like a reader monad written in direct 

−  style. 
+  style. The commutativity of the reader monad ensures that the code still is 
referentially transparent (the monomorphic recursion issue aside that will be 
referentially transparent (the monomorphic recursion issue aside that will be 

discussed below). 
discussed below). 

Line 177:  Line 175:  
Linear implicit parameters [[#ref6 6]] work very much like regular implicit 
Linear implicit parameters [[#ref6 6]] work very much like regular implicit 

parameters, but the type of the parameter is required to be an instance of the 
parameters, but the type of the parameter is required to be an instance of the 

−  class 
+  class <haskell>GHC.Exts.Splittable</haskell> with the single method 
−  +  <haskell>split :: a > (a,a)</haskell>. At each branching point of the computation, the 

−  parameter gets split, so that each value is used only once. 
+  parameter gets split, so that each value is used only once. However, as we shall 
−  later see, this linearity is not enforced in all circumstances, with higher order 
+  later see, this linearity is not enforced in all circumstances, with higher order 
functions and a certain class of recursive functions being the notable exceptions. 
functions and a certain class of recursive functions being the notable exceptions. 

Possible uses are random number distribution, fresh name generation (if you do 
Possible uses are random number distribution, fresh name generation (if you do 

−  not mind the names becoming very long) or a directstyle !QuickCheck 
+  not mind the names becoming very long) or a directstyle !QuickCheck 
[[#ref7 7]]. In this article, they will be used to store a subcontinuation from 
[[#ref7 7]]. In this article, they will be used to store a subcontinuation from 

−  an enclosing 
+  an enclosing <haskell>reset</haskell>. The syntax is exactly the same as in the implicit 
−  case with the 
+  case with the <haskell>?</haskell> replaced by <haskell>%</haskell>. We give a small example 
illustrating their intended use. 
illustrating their intended use. 

−  +  <haskell>#!syntax haskell 

import qualified System.Random as R 
import qualified System.Random as R 

Line 196:  Line 194:  
randInts :: R.StdGen > (Int, Int, Int) 
randInts :: R.StdGen > (Int, Int, Int) 

randInts gen = let %gen = gen in (rand, rand, rand) where 
randInts gen = let %gen = gen in (rand, rand, rand) where 

−  +  rand :: (%gen :: R.StdGen) => Int 

−  +  rand = fst $ R.random %gen 

−  +  * Main> print . randInts =<< R.getStdGen 

−  *Main> print . randInts =<< R.getStdGen 

(1305955622,1639797044,945468976) 
(1305955622,1639797044,945468976) 

−  }}} 

+  </haskell> 

−  
As in the implicit case, the semantics of linear implicit parameters can be 
As in the implicit case, the semantics of linear implicit parameters can be 

described in terms of a "monad", which, however, does not obey the monad 
described in terms of a "monad", which, however, does not obey the monad 

laws in any nontrivial case. 
laws in any nontrivial case. 

−  +  <haskell>#!syntax haskell 

newtype Split r a = Split { runSplit :: r > a } 
newtype Split r a = Split { runSplit :: r > a } 

instance Functor (Split r) where 
instance Functor (Split r) where 

−  +  f `fmap` Split x = Split $ f . x 

instance Splittable r => Monad (Split r) where 
instance Splittable r => Monad (Split r) where 

−  +  return x = Split $ const x 

−  +  Split x >>= f = Split $ \s > 

−  +  let (s1,s2) = split s in f (x s1) `runSplit` s2 

toSplit :: ((%foo :: r) => a) > Split r a 
toSplit :: ((%foo :: r) => a) > Split r a 

Line 222:  Line 219:  
fromSplit :: Split r a > ((%foo :: r) => a) 
fromSplit :: Split r a > ((%foo :: r) => a) 

fromSplit (Split f) = f %foo 
fromSplit (Split f) = f %foo 

−  }}} 

+  </haskell> 

The ability to freely transform between "monadic" and "implicit" style is 
The ability to freely transform between "monadic" and "implicit" style is 

Line 228:  Line 225:  
contexts in a mutually recursive group must all be identical. 
contexts in a mutually recursive group must all be identical. 

−  === 
+  ===Unsafe Operations=== 
The code below uses two unsafe operations [[#ref8 8]]. We briefly discuss which 
The code below uses two unsafe operations [[#ref8 8]]. We briefly discuss which 

conditions must be checked in order to ensure that they are used in a "safe" 
conditions must be checked in order to ensure that they are used in a "safe" 

way. 
way. 

−  +  <haskell>#!syntax haskell 

unsafePerformIO :: IO a > a 
unsafePerformIO :: IO a > a 

−  unsafeCoerce# 
+  unsafeCoerce# :: a > b 
−  +  </haskell> 

−  The 
+  The <haskell>unsafePerformIO</haskell> function executes an <haskell>IO</haskell> action and returns the 
result as a pure value. Thus, it should only be used if the result of the 
result as a pure value. Thus, it should only be used if the result of the 

action does not depend on the state of the external world. However, we do not 
action does not depend on the state of the external world. However, we do not 

demand that the result of the computation be independent of the evaluation 
demand that the result of the computation be independent of the evaluation 

order. Furthermore, we must be aware that the compiler may inline function 
order. Furthermore, we must be aware that the compiler may inline function 

−  definitions, so that two invocations of 
+  definitions, so that two invocations of <haskell>unsafePerformIO</haskell> might be 
−  unexpectedly shared or duplicated. 
+  unexpectedly shared or duplicated. The <haskell>{# NOINLINE foo #</haskell>} pragma can 
be used to forbid inlining in such cases. 
be used to forbid inlining in such cases. 

−  The 
+  The <haskell>unsafeCoerce#</haskell> function is used to convert a value between two types that 
are known to be equal although the type system cannot proof this fact. If the 
are known to be equal although the type system cannot proof this fact. If the 

types do not match, its behavior is undefined; usually, the program will crash 
types do not match, its behavior is undefined; usually, the program will crash 

or return a wrong result. 
or return a wrong result. 

−  === 
+  ===Dynamic Exceptions=== 
In addition to exceptions that only print an error message, the Hierarchical 
In addition to exceptions that only print an error message, the Hierarchical 

−  Libraries provide the 
+  Libraries provide the <haskell>throwDyn</haskell> and <haskell>catchDyn</haskell> functions that throw and catch 
exceptions of an arbitrary instance of the class Typeable. 
exceptions of an arbitrary instance of the class Typeable. 

However, there is a tricky aspect of exceptions because of Haskell's laziness. 
However, there is a tricky aspect of exceptions because of Haskell's laziness. 

Consider 
Consider 

−  +  <haskell>#!syntax haskell 

−  *Main> print =<< evaluate ([1,throwDyn "escape"]) 
+  * Main> print =<< evaluate ([1,throwDyn "escape"]) 
−  +  `catchDyn` \"escape" > return [2] 

[1,*** Exception: (unknown) 
[1,*** Exception: (unknown) 

−  }}} 

+  </haskell> 

Here the evaluation of the list only determines whether the list is empty, but 
Here the evaluation of the list only determines whether the list is empty, but 

the list is inspected when the expression is printed, and thus the exception 
the list is inspected when the expression is printed, and thus the exception 

−  escapes the 
+  escapes the <haskell>catchDyn</haskell> exception handler. 
When all thrown exception have to be caught, 
When all thrown exception have to be caught, 

we must evaluate the expression fully before handling the exception, which can 
we must evaluate the expression fully before handling the exception, which can 

−  be ensured with the 
+  be ensured with the <haskell>DeepSeq</haskell> [[#ref9 9]] class. 
−  +  <haskell>#!syntax haskell 

infixr 0 `deepSeq`, $!! 
infixr 0 `deepSeq`, $!! 

class DeepSeq a where 
class DeepSeq a where 

−  +  deepSeq :: a > b > b 

($!!) :: (DeepSeq a) => (a > b) > a > b 
($!!) :: (DeepSeq a) => (a > b) > a > b 

f $!! x = x `deepSeq` f x 
f $!! x = x `deepSeq` f x 

−  }}} 

+  </haskell> 

−  Not all types can be made an instance of 
+  Not all types can be made an instance of <haskell>DeepSeq</haskell>. In particular, functions 
−  with an infinite domain and 
+  with an infinite domain and <haskell>IO</haskell> actions cannot be fully evaluated in a 
sensible way. 
sensible way. 

−  == 
+  ==Implementation== 
This section discusses the implementation of the monadic reflection library. It 
This section discusses the implementation of the monadic reflection library. It 

safely be skipped, especially the first two subsections are very technical. 
safely be skipped, especially the first two subsections are very technical. 

−  === 
+  ===Basic Declarations=== 
−  +  <haskell>k :> v</haskell> is just an abstract representation of a finite map from k to v, 

−  The type 
+  The type <haskell>Position</haskell> will be used to store the context of the evaluation, so 
it should have the property that different sequences of applications of 
it should have the property that different sequences of applications of 

−  +  <haskell>leftPos</haskell> and <haskell>rightPos</haskell> to an <haskell>initPos</haskell> yield different values. A 

−  +  <haskell>Cell</haskell> stores a value of arbitrary type. The most interesting declaration 

−  is that of 
+  is that of <haskell>Prompt</haskell>. The field <haskell>position</haskell> saves the position of the 
−  current expression relative to the next enclosing reset, 
+  current expression relative to the next enclosing reset, <haskell>prompt</haskell> is the 
−  expression this next enclosing 
+  expression this next enclosing <haskell>reset</haskell> computes, <haskell>facts</haskell> stores the 
−  subexpressions that already have been assigned a value, and 
+  subexpressions that already have been assigned a value, and <haskell>promptID</haskell> will 
be used for exception handling. 
be used for exception handling. 

−  +  <haskell>#!syntax haskell 

infixr 9 :> 
infixr 9 :> 

lookup :: Ord k => (k :> v) > k > Maybe v 
lookup :: Ord k => (k :> v) > k > Maybe v 

insert :: Ord k => (k :> v) > k > v > k :> v 
insert :: Ord k => (k :> v) > k > v > k :> v 

−  empty 
+  empty :: k :> v 
−  leftPos 
+  leftPos :: Position > Position 
rightPos :: Position > Position 
rightPos :: Position > Position 

−  initPos 
+  initPos :: Position 
type Facts = Position :> Cell 
type Facts = Position :> Cell 

Line 316:  Line 313:  
data Prompt r = Prompt { 
data Prompt r = Prompt { 

−  +  position :: Position, 

−  +  prompt :: Direct r r, 

−  +  facts :: Facts, 

−  +  promptID :: Unique 

} 
} 

Line 325:  Line 322:  
instance Splittable (Prompt r) where 
instance Splittable (Prompt r) where 

−  +  split p = (p {position = leftPos pos}, 

−  +  p {position = rightPos pos}) where 

−  +  pos = position p 

type Direct r a = (%ans :: Prompt r) => a 
type Direct r a = (%ans :: Prompt r) => a 

−  }}} 

+  </haskell> 

−  === 
+  ===Shift and Reset=== 
+  <haskell>shift</haskell> first saves the <haskell>Prompt</haskell> and checks if this <haskell>shift</haskell> has 

+  already been assigned a value using the <haskell>facts</haskell> dictionary. If so, it just 

+  returns that value, otherwise, the outer <haskell>reset</haskell> should return the value of 

+  <haskell>f</haskell> applied to the subcontinuation from the <haskell>shift</haskell> to the <haskell>reset</haskell>. 

+  The subcontinuation we pass to <haskell>f</haskell> creates a new copy of the <haskell>Prompt</haskell> on 

+  every invocation, updates the <haskell>facts</haskell> dictionary with the additional 

+  information that instead of the current <haskell>shift</haskell>, the value <haskell>x</haskell> should 

+  be returned, and finally executes the <haskell>prompt</haskell> computation of the enclosing 

+  <haskell>reset</haskell>. In order to pass the result of <haskell>f</haskell> up to the next <haskell>reset</haskell>, 

+  we use exception handling, the unique ID of the <haskell>Prompt</haskell> ensures that it is 

+  handled at the right place; the value, although known to be of type <haskell>r</haskell> is 

+  put in a <haskell>Cell</haskell> because we do not know whether <haskell>r</haskell> is an instance of 

+  the class <haskell>Typeable</haskell>. 

−  {{{shift}}} first saves the {{{Prompt}}} and checks if this {{{shift}}} has 

+  Now all <haskell>reset</haskell> has to do is evaluate the expression with a fresh 

−  already been assigned a value using the {{{facts}}} dictionary. If so, it just 

+  <haskell>Prompt</haskell>, and return the thrown value instead if an exception is caught. 

−  returns that value, otherwise, the outer {{{reset}}} should return the value of 

−  {{{f}}} applied to the subcontinuation from the {{{shift}}} to the {{{reset}}}. 

−  The subcontinuation we pass to {{{f}}} creates a new copy of the {{{Prompt}}} on 

−  every invocation, updates the {{{facts}}} dictionary with the additional 

−  information that instead of the current {{{shift}}}, the value {{{x}}} should 

−  be returned, and finally executes the {{{prompt}}} computation of the enclosing 

−  {{{reset}}}. In order to pass the result of {{{f}}} up to the next {{{reset}}}, 

−  we use exception handling, the unique ID of the {{{Prompt}}} ensures that it is 

−  handled at the right place; the value, although known to be of type {{{r}}} is 

−  put in a {{{Cell}}} because we do not know whether {{{r}}} is an instance of 

−  the class {{{Typeable}}}. 

−  
−  Now all {{{reset}}} has to do is evaluate the expression with a fresh 

−  {{{Prompt}}}, and return the thrown value instead if an exception is caught. 

This gets a little more complicated because we need to be able to handle the 
This gets a little more complicated because we need to be able to handle the 

−  effects of nested 
+  effects of nested <haskell>resets</haskell>. 
−  +  <haskell>#!syntax haskell 

shift :: ((a > r) > Direct r r) > Direct r a 
shift :: ((a > r) > Direct r r) > Direct r a 

shift f :: Direct r a = 
shift f :: Direct r a = 

−  +  let ans :: Prompt r 

−  +  ans = %ans 

−  +  in case lookup (facts ans) (position ans) of 

−  +  Just (Cell a) > unsafeCoerce# a 

−  +  Nothing > throwDyn . (,) (promptID ans) . Cell . f $ \x > 

−  +  let %ans = newPrompt 

−  +  (insert (facts ans) (position ans) (Cell x)) 

−  +  (prompt ans) 

−  +  in prompt ans 

reset :: DeepSeq r => Direct r r > r 
reset :: DeepSeq r => Direct r r > r 

reset e :: r = let %ans = newPrompt empty res in res where 
reset e :: r = let %ans = newPrompt empty res in res where 

−  +  res :: Direct r r 

−  +  res = unsafePerformIO $ do 

−  +  let catchEsc e' = evaluate (id $!! e') `catchDyn` 

−  +  \err@(i, Cell result) > 

−  +  if i == promptID %ans 

−  +  then catchEsc $ unsafeCoerce# result 

−  +  else throwDyn err 

−  +  catchEsc e 

−  +  </haskell> 

It is interesting to observe that in case of the error monad, this code uses 
It is interesting to observe that in case of the error monad, this code uses 

−  the 
+  the <haskell>IO</haskell> monad's exception handling mechanism to propagate the error. 
Finally, we need to check the unsafe features are used in a safe way as 
Finally, we need to check the unsafe features are used in a safe way as 

−  described above. The 
+  described above. The <haskell>unsafeCoerce#</haskell> calls are always coercing to type 
−  +  <haskell>r</haskell> and it is clear that always the same <haskell>r</haskell> is in scope which we are 

−  ensuring using the 
+  ensuring using the <haskell>i == promptID</haskell> check. <haskell>unsafePerformIO</haskell> is only 
used for a "pure exception handling", which destroys purity, but still 
used for a "pure exception handling", which destroys purity, but still 

satisfies the weaker condition that the behavior does not depend on the outside 
satisfies the weaker condition that the behavior does not depend on the outside 

Line 390:  Line 373:  
performs exactly the same steps when rerun. 
performs exactly the same steps when rerun. 

−  
+  ===Reflection and Reification=== 

−  === Reflection and Reification === 

+  With working <haskell>shift</haskell> and <haskell>reset</haskell> functions, we can now turn to monadic 

−  With working {{{shift}}} and {{{reset}}} functions, we can now turn to monadic 

reflection primitives. We first consider the case of the continuation monad. 
reflection primitives. We first consider the case of the continuation monad. 

−  ==== 
+  ====Reflecting the Cont Monad==== 
−  +  <haskell>#!syntax haskell 

reflectCont :: Cont r a > Direct r a 
reflectCont :: Cont r a > Direct r a 

reflectCont (Cont f) = shift f 
reflectCont (Cont f) = shift f 

Line 402:  Line 384:  
reifyCont :: DeepSeq r => Direct r a > Cont r a 
reifyCont :: DeepSeq r => Direct r a > Cont r a 

reifyCont e = Cont $ \k > reset (k e) 
reifyCont e = Cont $ \k > reset (k e) 

−  }}} 

+  </haskell> 

−  As an example, we lift the function 
+  As an example, we lift the function <haskell>callCC</haskell> from <haskell>Control.Monad.Cont</haskell> 
to directstyle. 
to directstyle. 

−  +  <haskell>#!syntax haskell 

callCC' :: DeepSeq r => ((a > b) > Direct r a) > Direct r a 
callCC' :: DeepSeq r => ((a > b) > Direct r a) > Direct r a 

callCC' f = reflectCont $ callCC $ \c > reifyCont $ f $ reflectCont . c 
callCC' f = reflectCont $ callCC $ \c > reifyCont $ f $ reflectCont . c 

−  }}} 

+  </haskell> 

−  However, the 
+  However, the <haskell>call/cc</haskell> operation can be implemented much more nicely using 
−  only two 
+  only two <haskell>shift</haskell>s, as in 
−  +  <haskell>#!syntax haskell 

callCC' :: ((forall b. a > b) > Direct r a) > Direct r a 
callCC' :: ((forall b. a > b) > Direct r a) > Direct r a 

callCC' f = shift $ \k > k $ f (\x > shift $ \_ > k x) 
callCC' f = shift $ \k > k $ f (\x > shift $ \_ > k x) 

−  }}} 

+  </haskell> 

In both versions, the expression 
In both versions, the expression 

−  +  <haskell>#!syntax haskell 

reset (callCC' (\k x > k (x+)) 5) :: Int 
reset (callCC' (\k x > k (x+)) 5) :: Int 

−  }}} 

+  </haskell> 

−  correctly evaluates to 
+  correctly evaluates to <haskell>10</haskell>. It is a nice exercise to do this in Haskell's 
continuation monad; but be warned that it is a little harder than the above 
continuation monad; but be warned that it is a little harder than the above 

directstyle version. 
directstyle version. 

−  ==== 
+  ====Reflecting Arbitrary Monads==== 
−  Now, implementing 
+  Now, implementing <haskell>reflect</haskell> and <haskell>reify</haskell> is easier than in Filinski's 
−  implementation in SML, because the stronger static guarantees of our 
+  implementation in SML, because the stronger static guarantees of our <haskell>shift</haskell> 
−  and 
+  and <haskell>reset</haskell> functions eliminate the need for unsafe coercion functions. 
−  +  <haskell>#!syntax haskell 

 Type alias for more concise type signatures of directstyle code. 
 Type alias for more concise type signatures of directstyle code. 

type Monadic m a = forall r. Direct (m r) a 
type Monadic m a = forall r. Direct (m r) a 

Line 440:  Line 422:  
reify :: (DeepSeq (m a), Monad m) => Monadic m a > m a 
reify :: (DeepSeq (m a), Monad m) => Monadic m a > m a 

reify t = reset (return t) 
reify t = reset (return t) 

−  }}} 

+  </haskell> 

−  == 
+  ==Interface== 
For quick reference, we repeat the type signatures of the most important 
For quick reference, we repeat the type signatures of the most important 

library functions. 
library functions. 

−  +  <haskell>#!syntax haskell 

type Direct r a = (%ans :: Prompt r) => a 
type Direct r a = (%ans :: Prompt r) => a 

shift :: ((a > r) > Direct r r) > Direct r a 
shift :: ((a > r) > Direct r r) > Direct r a 

Line 453:  Line 435:  
reflect :: Monad m => m a > Monadic m a 
reflect :: Monad m => m a > Monadic m a 

reify :: (DeepSeq (m a), Monad m) => Monadic m a > m a 
reify :: (DeepSeq (m a), Monad m) => Monadic m a > m a 

−  }}} 

+  </haskell> 

−  == 
+  ==Resolving Ambiguities== 
The use of linear implicit parameters comes with a few surprises. 
The use of linear implicit parameters comes with a few surprises. 

The GHC manual [[#ref6 6]] even writes 
The GHC manual [[#ref6 6]] even writes 

−  ##quote 
+  ## quote 
−  +  <haskell> 

So the semantics of the program depends on whether or not foo has a type 
So the semantics of the program depends on whether or not foo has a type 

signature. Yikes! 
signature. Yikes! 

You may say that this is a good reason to dislike linear implicit parameters 
You may say that this is a good reason to dislike linear implicit parameters 

and you'd be right. That is why they are an experimental feature. 
and you'd be right. That is why they are an experimental feature. 

−  }}} 

+  </haskell> 

However, most of the problems can be circumvented quite easily, and the 
However, most of the problems can be circumvented quite easily, and the 

property that the meaning of a program can depend on the signatures given 
property that the meaning of a program can depend on the signatures given 

is actually a good thing. 
is actually a good thing. 

−  === 
+  ===Recursive Functions=== 
Indeed, omitting a type signature can sometimes result in a different 
Indeed, omitting a type signature can sometimes result in a different 

behavior. Consider the following code, where 
behavior. Consider the following code, where 

−  +  <haskell>shift (\k > k n)</haskell> and <haskell>n</haskell> should behave identically. 

−  +  <haskell>#!syntax haskell 

 Without the explicit signature for k GHC does not infer a 
 Without the explicit signature for k GHC does not infer a 

 sufficiently general type. 
 sufficiently general type. 

−  down 0 
+  down 0 = [] 
down (n+1) = shift (\(k::Int > [Int]) > k n): down n 
down (n+1) = shift (\(k::Int > [Int]) > k n): down n 

−  
+  * Main> reset (down 4) 

−  *Main> reset (down 4) 

[3,3,3,3]  wrong! 
[3,3,3,3]  wrong! 

−  }}} 

+  </haskell> 

−  GHC considers the function 
+  GHC considers the function <haskell>down</haskell> to be monomorphically recursive, but in 
−  fact the recursive call to 
+  fact the recursive call to <haskell>down</haskell> should be in a different context (with 
−  the implicit parameter bound to a different value), so 
+  the implicit parameter bound to a different value), so <haskell>down</haskell> should 
actually be polymorphically recursive. This is semantically different and 
actually be polymorphically recursive. This is semantically different and 

ensures the linearity. We can persuade GHC to treat it correctly by giving the 
ensures the linearity. We can persuade GHC to treat it correctly by giving the 

function an explicit signature. 
function an explicit signature. 

−  +  <haskell>#!syntax haskell 

down' :: Int > Direct [Int] [Int] 
down' :: Int > Direct [Int] [Int] 

{ ... } 
{ ... } 

−  *Main> reset (down' 4) 
+  * Main> reset (down' 4) 
[3,2,1,0]  right! 
[3,2,1,0]  right! 

−  }}} 

+  </haskell> 

Furthermore, we have to watch out for a GHC bug [[#ref10 10]] that appears 
Furthermore, we have to watch out for a GHC bug [[#ref10 10]] that appears 

to happen when expressions with differently polymorphic linear implicit 
to happen when expressions with differently polymorphic linear implicit 

parameter constraints are unified. In the above example, this occurs when 
parameter constraints are unified. In the above example, this occurs when 

−  +  <haskell>k</haskell>'s explicit type signature is dropped and the signature of <haskell>down</haskell> is 

−  not generalized to 
+  not generalized to <haskell>Int > Direct r [Int]</haskell>. 
−  === 
+  ===Higher order functions=== 
Implicit parameters are particularly tricky when functions using implicit 
Implicit parameters are particularly tricky when functions using implicit 

parameters are passed to higher order functions. Consider the following 
parameters are passed to higher order functions. Consider the following 

example. 
example. 

−  +  <haskell>#!syntax haskell 

 The prelude definition of the function map 
 The prelude definition of the function map 

map :: (a > b) > [a] > [b] 
map :: (a > b) > [a] > [b] 

−  map _ [] 
+  map _ [] = [] 
map f (x:xs) = f x : map f xs 
map f (x:xs) = f x : map f xs 

foo :: [[Int]] 
foo :: [[Int]] 

foo = reify (map f [1,2,3]) where 
foo = reify (map f [1,2,3]) where 

−  +  f :: Int > Monadic [] Int 

−  +  f x = reflect [x,x] 

−  +  * Main> foo 

−  *Main> foo 

[[1,1,1],[1,1,1]]  wrong! 
[[1,1,1],[1,1,1]]  wrong! 

−  }}} 

+  </haskell> 

The first surprise is that this code type checks at all: The type of the 
The first surprise is that this code type checks at all: The type of the 

−  function 
+  function <haskell>f</haskell> is <haskell>Int > Monadic [] Int</haskell> but in order to be passed to 
−  +  <haskell>map</haskell>, the function <haskell>f</haskell> must have the different type 

−  +  <haskell>Monadic [] (Int > Int)</haskell>. 

GHC pushes contexts at covariant argument positions as far to the 
GHC pushes contexts at covariant argument positions as far to the 

left as possible using a technique called forallhoisting [[#ref6 6]], 
left as possible using a technique called forallhoisting [[#ref6 6]], 

Line 532:  Line 513:  
as parameters, but at least we can copy the implementation of the higher order 
as parameters, but at least we can copy the implementation of the higher order 

functions we want to use. 
functions we want to use. 

−  +  <haskell>#!syntax haskell 

map' :: (a > Direct r b) > [a] > Direct r [b] 
map' :: (a > Direct r b) > [a] > Direct r [b] 

{ Implementation as above } 
{ Implementation as above } 

foo = reify (map' f [1,2,3]) where { ... } 
foo = reify (map' f [1,2,3]) where { ... } 

−  
+  * Main> foo 

−  *Main> foo 

[[1,2,3],[1,2,3],[1,2,3],[1,2,3],[1,2,3],[1,2,3],[1,2,3], 
[[1,2,3],[1,2,3],[1,2,3],[1,2,3],[1,2,3],[1,2,3],[1,2,3], 

[1,2,3]]  right! 
[1,2,3]]  right! 

−  }}} 

+  </haskell> 

−  === 
+  ===The Monomorphism Restriction=== 
What should the expression 
What should the expression 

−  +  <haskell>#!syntax haskell 

reify (let x = reflect [0,1] in [x,x+2,x+4]) 
reify (let x = reflect [0,1] in [x,x+2,x+4]) 

−  }}} 

+  </haskell> 

evaluate to? Two possibilities come to mind: Either we choose a value for the 
evaluate to? Two possibilities come to mind: Either we choose a value for the 

−  variable 
+  variable <haskell>x</haskell> first, and then evaluate the lists <haskell>[x,x+2,x+4]</haskell> or we 
−  view 
+  view <haskell>x</haskell> as the reflected list <haskell>[0,1]</haskell> and the choice whether <haskell>x</haskell> 
−  stands for 
+  stands for <haskell>0</haskell> or <haskell>1</haskell> is made whenever <haskell>x</haskell> it is evaluated. It is 
immediately clear how both variants can be achieved in monadic style. 
immediately clear how both variants can be achieved in monadic style. 

−  +  <haskell>#!syntax haskell 

−  *Main> do x < [0,1]; return [x,x+2,x+4] 
+  * Main> do x < [0,1]; return [x,x+2,x+4] 
[[0,2,4],[1,3,5]] 
[[0,2,4],[1,3,5]] 

−  *Main> let x = [0,1] in sequence [x,(+2) `fmap` x, (+4) `fmap` x] 
+  * Main> let x = [0,1] in sequence [x,(+2) `fmap` x, (+4) `fmap` x] 
[[0,2,4],[0,2,5],[0,3,4],[0,3,5],[1,2,4],[1,2,5],[1,3,4],[1,3,5]] 
[[0,2,4],[0,2,5],[0,3,4],[0,3,5],[1,2,4],[1,2,5],[1,3,4],[1,3,5]] 

−  }}} 

+  </haskell> 

In direct style, this is even easier, but the meaning of our code now depends 
In direct style, this is even easier, but the meaning of our code now depends 

on the type signature. 
on the type signature. 

−  +  <haskell>#!syntax haskell 

−  *Main> reify (let x :: Int; x = reflect [0,1] in [x,x+2,x+4]) 
+  * Main> reify (let x :: Int; x = reflect [0,1] in [x,x+2,x+4]) 
[[0,2,4],[1,3,5]] 
[[0,2,4],[1,3,5]] 

−  *Main> reify (let x :: Monadic [] Int; x = reflect [0,1] in [x,x+2,x+4]) 
+  * Main> reify (let x :: Monadic [] Int; x = reflect [0,1] in [x,x+2,x+4]) 
[[0,2,4],[0,2,5],[0,3,4],[0,3,5],[1,2,4],[1,2,5],[1,3,4],[1,3,5]] 
[[0,2,4],[0,2,5],[0,3,4],[0,3,5],[1,2,4],[1,2,5],[1,3,4],[1,3,5]] 

−  }}} 

+  </haskell> 

It is important that we give a real type signature: 
It is important that we give a real type signature: 

−  +  <haskell>x :: Int = reflect [0,1]</haskell> does not make any difference! 

This is a nice and very natural way to describe both situations, but the 
This is a nice and very natural way to describe both situations, but the 

answer to the question which one GHC chooses when no signature is given is less 
answer to the question which one GHC chooses when no signature is given is less 

satisfactory: It depends on the status of the flag 
satisfactory: It depends on the status of the flag 

−  +  <haskell>f(no)monomorphismrestriction</haskell>. 

−  With the monomorphism "restriction" [[#ref11 11]] turned on, 
+  With the monomorphism "restriction" [[#ref11 11]] turned on, <haskell>x</haskell> must have 
a monomorphic type, so the first situation applies, without the restriction 
a monomorphic type, so the first situation applies, without the restriction 

−  +  <haskell>x</haskell> gets the most general type which leads to the second behavior. In my 

opinion, it would be nice if there were a flag that, in order to give the 
opinion, it would be nice if there were a flag that, in order to give the 

programmer a chance to disambiguate his code, causes a warning to be emitted 
programmer a chance to disambiguate his code, causes a warning to be emitted 

Line 581:  Line 561:  
proven useful to detect numeric defaulting. 
proven useful to detect numeric defaulting. 

−  == 
+  ==Examples== 
−  We now present some examples reflecting the 
+  We now present some examples reflecting the <haskell>Cont</haskell> and <haskell>[]</haskell> monads. 
−  === 
+  ===Lazy Evaluation=== 
The use of monads in Haskell models an impure language with callbyvalue 
The use of monads in Haskell models an impure language with callbyvalue 

semantics. This is not surprising as one motivation for the use of monads is 
semantics. This is not surprising as one motivation for the use of monads is 

the need to do IO. For IO, evaluation order is important and callbyvalue 
the need to do IO. For IO, evaluation order is important and callbyvalue 

−  makes evaluation order easier to reason about. 
+  makes evaluation order easier to reason about. For the <haskell>IO</haskell> monad this 
−  certainly the right decision, and if desired, the 
+  certainly the right decision, and if desired, the <haskell>unsafeInterleaveIO</haskell> 
−  function can be used to execute 
+  function can be used to execute <haskell>IO</haskell> operations lazily. 
But such a lazy monadic behavior would be practical for other monads, too: The 
But such a lazy monadic behavior would be practical for other monads, too: The 

Line 596:  Line 576:  
The reflected list monad, however, is often closer to the desired behavior, 
The reflected list monad, however, is often closer to the desired behavior, 

as the following examples suggest. 
as the following examples suggest. 

−  +  <haskell>#!syntax haskell 

 Lazy repeat, Prelude.repeat would allow the side effect 
 Lazy repeat, Prelude.repeat would allow the side effect 

 of the argument to take place only once 
 of the argument to take place only once 

repeat' :: Direct r a > Direct r [a] 
repeat' :: Direct r a > Direct r [a] 

repeat' x = x:repeat' x 
repeat' x = x:repeat' x 

−  
+  * Main> take 3 `fmap` sequence (repeat [1,2::Int]) 

−  *Main> take 3 `fmap` sequence (repeat [1,2::Int]) 

<< Does not terminate. >> 
<< Does not terminate. >> 

−  *Main> reify (take 3 $ repeat' (reflect [1,2::Int])) 
+  * Main> reify (take 3 $ repeat' (reflect [1,2::Int])) 
[[1,1,1],[1,1,2],[1,2,1],[1,2,2],[2,1,1],[2,1,2],[2,2,1],[2,2,2]] 
[[1,1,1],[1,1,2],[1,2,1],[1,2,2],[2,1,1],[2,1,2],[2,2,1],[2,2,2]] 

−  
+  * Main> fst `fmap` liftM2 (,) [1,2::Int] [3,4::Int] 

−  *Main> fst `fmap` liftM2 (,) [1,2::Int] [3,4::Int] 

[1,1,2,2] 
[1,1,2,2] 

−  *Main> reify (fst (reflect [1,2::Int], reflect [3,4::Int])) 
+  * Main> reify (fst (reflect [1,2::Int], reflect [3,4::Int])) 
[1,2] 
[1,2] 

−  *Main> reify (fst $!! (reflect [1,2::Int], reflect [3,4::Int])) 
+  * Main> reify (fst $!! (reflect [1,2::Int], reflect [3,4::Int])) 
[1,1,2,2] 
[1,1,2,2] 

−  }}} 

+  </haskell> 

The last expression shows that we can easily revert to the eager version by 
The last expression shows that we can easily revert to the eager version by 

adding appropriate strictness annotations. 
adding appropriate strictness annotations. 

−  === 
+  ===Filtering Permutations=== 
As a typical problem where the lazy behavior of our implementation is 
As a typical problem where the lazy behavior of our implementation is 

advantageous, we consider a small combinatorial example: Find all permutations 
advantageous, we consider a small combinatorial example: Find all permutations 

of 
of 

−  +  <haskell>#!latex 

$(1,2,4,...,2^{n1})$ 
$(1,2,4,...,2^{n1})$ 

−  }}} 

+  </haskell> 

such that all the sums of the initial sequences of the permutations are primes. 
such that all the sums of the initial sequences of the permutations are primes. 

−  +  <haskell>#!syntax haskell 

 NB. This section's example code can be found in the files Perms.*. 
 NB. This section's example code can be found in the files Perms.*. 

 _very_ simple primality test. 
 _very_ simple primality test. 

isPrime :: Int > Bool 
isPrime :: Int > Bool 

isPrime n = n >= 2 && all (\k > n `mod` k /= 0) 
isPrime n = n >= 2 && all (\k > n `mod` k /= 0) 

−  +  (takeWhile (\k > k*k <= n) $ 2:[3,5..]) 

 check if all the initial sums are primes. 
 check if all the initial sums are primes. 

goodPerm :: [Int] > Bool 
goodPerm :: [Int] > Bool 

goodPerm xs = all isPrime (scanl1 (+) xs) 
goodPerm xs = all isPrime (scanl1 (+) xs) 

−  }}} 

+  </haskell> 

If we want to solve the problem in Haskell, we need to make a big compromise: 
If we want to solve the problem in Haskell, we need to make a big compromise: 

Either we take the easy road and generate a list of the permutations and then 
Either we take the easy road and generate a list of the permutations and then 

−  +  <haskell>filter</haskell> the good ones, which is unfortunately very slow because ''all'' 

permutations must be checked even if it already turns out after inspecting 
permutations must be checked even if it already turns out after inspecting 

a few list elements that no permutation starting this way can have the property. 
a few list elements that no permutation starting this way can have the property. 

Line 657:  Line 635:  
the nondeterminacy cannot be expressed on the type level. 
the nondeterminacy cannot be expressed on the type level. 

Using monadic reflection, we can do something very similar as follows. 
Using monadic reflection, we can do something very similar as follows. 

−  +  <haskell>#!syntax haskell 

 nondeterministic choice 
 nondeterministic choice 

(?) :: DeepSeq a => Monadic [] a > Monadic [] a > Monadic [] a 
(?) :: DeepSeq a => Monadic [] a > Monadic [] a > Monadic [] a 

Line 666:  Line 644:  
permute [] = [] 
permute [] = [] 

permute xs = y: permute ys where 
permute xs = y: permute ys where 

−  +  y::Int; ys::[Int] 

−  +  (y,ys) = select xs 

select :: [Int] > Monadic [] (Int,[Int]) 
select :: [Int] > Monadic [] (Int,[Int]) 

select [] = reflect [] 
select [] = reflect [] 

select (x:xs) = (x,xs) ? second (x:) (select xs) where 
select (x:xs) = (x,xs) ? second (x:) (select xs) where 

−  +   a special case of Control.Arrow.second 

−  +  second f (x,y) = (x,f y) 

−  +  </haskell> 

Now we only need to ensure that the computation fails when the permutation 
Now we only need to ensure that the computation fails when the permutation 

does not have the desired property. 
does not have the desired property. 

−  +  <haskell>#!syntax haskell 

solve :: Int > Monadic [] [Int] 
solve :: Int > Monadic [] [Int] 

solve n = if goodPerm xs then xs else reflect [] where 
solve n = if goodPerm xs then xs else reflect [] where 

−  +  xs :: [Int] 

−  +  xs = permute $ map (2^) [0..n1] 

−  +  * Main> reify (solve 17) 

−  *Main> reify (solve 17) 

[[2,1,4,1024,512,16,8,65536,128,4096,32,16384,32768,256,8192,64,2048], 
[[2,1,4,1024,512,16,8,65536,128,4096,32,16384,32768,256,8192,64,2048], 

[2,1,4,1024,512,16,2048,16384,8192,65536,32768,64,32,256,128,4096,8]] 
[2,1,4,1024,512,16,2048,16384,8192,65536,32768,64,32,256,128,4096,8]] 

−  }}} 

+  </haskell> 

The relative performance of the different approaches is not surprising: The 
The relative performance of the different approaches is not surprising: The 

Line 691:  Line 669:  
Curry) is about six times slower while the solution using monadic reflection is 
Curry) is about six times slower while the solution using monadic reflection is 

another four times slower (and gets slightly worse for larger values of 
another four times slower (and gets slightly worse for larger values of 

−  +  <haskell>n</haskell>), since a lot of recomputation is implied by the way <haskell>shift</haskell> and 

−  +  <haskell>reset</haskell> are implemented. Finally, the naÔve solution would probably take 

years to finish. 
years to finish. 

−  == 
+  ==Further Ideas== 
−  This section discusses some further directions in which the ideas of this 
+  This section discusses some further directions in which the ideas of this 
article might be extended. 
article might be extended. 

−  === 
+  ===Denotational Semantics=== 
The relationship between laziness and directstyle continuation effects, 
The relationship between laziness and directstyle continuation effects, 

despite often following the intuition, needs some further clarification. 
despite often following the intuition, needs some further clarification. 

Line 706:  Line 684:  
library, respectively. They can be checked for coincidence using !QuickCheck 
library, respectively. They can be checked for coincidence using !QuickCheck 

tests generating typechecking expressions for the language. The monad 
tests generating typechecking expressions for the language. The monad 

−  the interpreter is built upon is an 
+  the interpreter is built upon is an <haskell>ST</haskell> monad augmented with continuations 
−  of answer type 
+  of answer type <haskell>Int</haskell> using the <haskell>ContT</haskell> transformer. 
−  +  <haskell>#!syntax haskell 

newtype Eval s a 
newtype Eval s a 

−  +  = Eval { runEval :: ContT Int (ST s) a } 

−  +  deriving (Functor, Monad) 

−  +  </haskell> 

The interpreter maps the source language's expressions into the following 
The interpreter maps the source language's expressions into the following 

universal type. 
universal type. 

−  +  <haskell>#!syntax haskell 

type U s = Eval s (Ref s `Either` U' s) 
type U s = Eval s (Ref s `Either` U' s) 

data U' s 
data U' s 

−  +  = Int { runInt :: Int } 

−  +   Fun { runFun :: U s > U s } 

−  +   List { runList :: Maybe (U s, U s) } 

newtype Ref s = Ref { unRef :: STRef s (U' s `Either` U s) } 
newtype Ref s = Ref { unRef :: STRef s (U' s `Either` U s) } 

−  }}} 

+  </haskell> 

−  So an 
+  So an <haskell>U s</haskell> is either a reference or a value of type <haskell>U' s</haskell>; references 
−  either point to a thunk of type 
+  either point to a thunk of type <haskell>U s</haskell> or to an evaluated value of type 
−  +  <haskell>U' s</haskell>. Laziness is provided by two functions of the following types. 

−  +  <haskell>#!syntax haskell 

 Delays a computation 
 Delays a computation 

delay :: U s > U s 
delay :: U s > U s 

 Force evaluation of a reference to a normal form. 
 Force evaluation of a reference to a normal form. 

force :: U s > Eval s (U' s) 
force :: U s > Eval s (U' s) 

−  }}} 

+  </haskell> 

Details can be found in the [attachment:Reflection.tar.gz tarball] provided with this article. The 
Details can be found in the [attachment:Reflection.tar.gz tarball] provided with this article. The 

Line 742:  Line 720:  
annotations. 
annotations. 

−  === 
+  ===A Lightweight Notation for Monads=== 
Haskell's donotation is often criticized being too verbose, especially for 
Haskell's donotation is often criticized being too verbose, especially for 

commutative monads; and the process of transforming pure functions into monadic 
commutative monads; and the process of transforming pure functions into monadic 

Line 749:  Line 727:  
GHC already has special support for the (commutative) reader monad, through 
GHC already has special support for the (commutative) reader monad, through 

−  implicit parameters. 
+  implicit parameters. This special rÙle of the reader monad might be justified 
by additional properties this monad has, for example that there are 
by additional properties this monad has, for example that there are 

−  isomorphisms of type 
+  isomorphisms of type <haskell>m (a > b) > a > m b</haskell> and 
−  +  <haskell>m (a, b) > (m a, m b)</haskell> whose inverses are given by 

−  +  <haskell>\f x > f `ap` return x</haskell> and <haskell>liftM2 (,)</haskell>, respectively. 

Also, special tools [[#ref13 13]] are being developed that automatically 
Also, special tools [[#ref13 13]] are being developed that automatically 

transform a function from direct into monadic style, but this process 
transform a function from direct into monadic style, but this process 

requires arbitrary decisions where to apply effects, e.g. it is unclear if 
requires arbitrary decisions where to apply effects, e.g. it is unclear if 

−  a function of type 
+  a function of type <haskell>Int > Bool</haskell> should be monadified to a function of 
−  type 
+  type <haskell>Monad m => m Int > m Bool</haskell> or <haskell>Monad m => Int > m Bool</haskell>, as 
both make sense in different circumstances. 
both make sense in different circumstances. 

−  As we showed in this article, Haskell's type system is almost ready to 
+  As we showed in this article, Haskell's type system is almost ready to 
express these differences on the type level; the only remaining problem is 
express these differences on the type level; the only remaining problem is 

that forallhoisting [6] changes the meaning of expressions. On the other 
that forallhoisting [6] changes the meaning of expressions. On the other 

hand, because of the interaction with laziness, keeping the semantics of 
hand, because of the interaction with laziness, keeping the semantics of 

the library described in this article would result in a rather complicated 
the library described in this article would result in a rather complicated 

−  translation, as we saw in the last section. In order to get rid of this 
+  translation, as we saw in the last section. In order to get rid of this 
−  obscurity, one might imagine a typedirected translation which translates 
+  obscurity, one might imagine a typedirected translation which translates 
(pseudocode) 
(pseudocode) 

−  +  <haskell>#!syntax haskell 

reflect :: m a > (<m> => a) 
reflect :: m a > (<m> => a) 

−  reify 
+  reify :: Monad m => (<m> => a) > m a 
foo :: <[]> => Int 
foo :: <[]> => Int 

Line 779:  Line 757:  
bar :: [Int] 
bar :: [Int] 

bar = reify foo 
bar = reify foo 

−  }}} 

+  </haskell> 

−  more strictly into 
+  more strictly into 
−  +  <haskell>#!syntax haskell 

foo :: [Int] 
foo :: [Int] 

foo = (+) `fmap` [0,2] `ap` [0,1] 
foo = (+) `fmap` [0,2] `ap` [0,1] 

Line 787:  Line 765:  
bar :: [Int] 
bar :: [Int] 

bar = foo 
bar = foo 

−  }}} 

+  </haskell> 

However, this contradicts Haskell's philosophy to make invocation of effects as 
However, this contradicts Haskell's philosophy to make invocation of effects as 

explicit as possible, and would probably be considered an "underkill". Moreover, 
explicit as possible, and would probably be considered an "underkill". Moreover, 

it would require a decent solution to the monomorphism restriction problem. 
it would require a decent solution to the monomorphism restriction problem. 

−  == 
+  ==Conclusion== 
Do not take this too seriously: Our code heavily relies on unsafe and 
Do not take this too seriously: Our code heavily relies on unsafe and 

experimental features; time and space usage are increased by the suboptimal 
experimental features; time and space usage are increased by the suboptimal 

encoding of continuations and the recomputations; and the number of supported 
encoding of continuations and the recomputations; and the number of supported 

−  monads is limited by the 
+  monads is limited by the <haskell>DeepSeq</haskell> requirement. 
However, we provided a framework with strong static guarantees in which it is 
However, we provided a framework with strong static guarantees in which it is 

−  easy to experiment with the unfamiliar 
+  easy to experiment with the unfamiliar <haskell>shift</haskell> and <haskell>reset</haskell> operators, 
and we learned that GHC Haskell's type system goes well beyond 
and we learned that GHC Haskell's type system goes well beyond 

HindleyMilner and it is almost ready for an impure language where effects are 
HindleyMilner and it is almost ready for an impure language where effects are 

Line 807:  Line 785:  
of (GHC) Haskell, to create an impure sublanguage with monadic effects. 
of (GHC) Haskell, to create an impure sublanguage with monadic effects. 

−  == 
+  ==Acknowledgments== 
I would like to thank the GHC team for this great compiler with its many 
I would like to thank the GHC team for this great compiler with its many 

fascinating extensions. 
fascinating extensions. 

−  I also want to thank Peter Eriksen, Cale Gibbard and Don Stewart for 
+  I also want to thank Peter Eriksen, Cale Gibbard and Don Stewart for 
proofreading the article and their valuable suggestions, as well as 
proofreading the article and their valuable suggestions, as well as 

Brandon Moore and Autrijus Tang for their advice on the references. 
Brandon Moore and Autrijus Tang for their advice on the references. 

−  == 
+  ==References== 
[[Anchor(ref1)]] 
[[Anchor(ref1)]] 

[1] Olivier Danvy and Andrzej Filinski. 
[1] Olivier Danvy and Andrzej Filinski. 

Line 897:  Line 875:  
"Monadification as a Refactoring". 
"Monadification as a Refactoring". 

http://www.cs.kent.ac.uk/projects/refactorfp/Monadification.html 
http://www.cs.kent.ac.uk/projects/refactorfp/Monadification.html 

−   

+  
−  CategoryArticle 

+  [[Category:Article]] 
Revision as of 03:36, 10 May 2008
This article needs reformatting! Please help tidy it up WouterSwierstra 14:12, 9 May 2008 (UTC)
[attachment:Reflection.pdf PDF version of this article]
[attachment:Reflection.tar.gz Code from the article] [:IssueTwo/FeedBack/FunWithLinearImplicitParameters: Feedback]
Contents
Fun with Linear Implicit Parameters
Monadic Reflection in Haskell
by [:ThomasJ‰ger:Thomas J‰ger] for The Monad.Reader [:IssueTwo:Issue Two] BR 01.05.2005
Abstract. Haskell is widely believed to be a purely functional language. While this is certainly true for Haskell98, GHC's various extensions can interplay in unforeseen ways and make it possible to write sideeffecting code.
In this article, we take the next step of impure programming by implementing
Filinski'sreflect
reify
Introduction
The following sections provide a short introduction into the various concepts our implementation uses. You can download the implementation and the examples from the article [attachment:Reflection.tar.gz here], it has been successfully tested with ghc6.2.2 and ghc6.4. The examples of this article can be found
in the fileArticle.hs
Reflection.hs
Shift and Reset
Theshift
reflect
delimited continuations, which are similar to the undelimited continuation the
familiarcall/cc
descriptions available e.g. in Danvy & Filinski #ref1 1 and Shan #ref2 2; moreover, Dybvig, Peyton Jones, Sabry #ref3 3 give a unifying treatment of various forms of other "subcontinuations".
Instead of capturing an undelimited continuation ascall/cc
shift
reset
reifies it into a function value. The result of the evaluation of the body then
becomes the result of thereset
#!syntax haskell
reset (1 + shift (\k > k 1 + k 2)) :: Int
shift
k = \x > x + 1
k 1 + k 2 = 2 + 3 = 5
shift
reset
continuation monad.
#!syntax haskell
 An action in the continuation monad maps a continuation,
 i.e the "rest" of the computation, to a final result of type r.
newtype Cont r a = Cont { runCont :: (a > r) > r }
instance Functor (Cont r) where { ... }
instance Monad (Cont r) where { ... }
 NB. In the attached Article.hs file, these are called shiftC and resetC.
shift :: ((a > r) > Cont r r) > Cont r a
shift e = Cont $ \k > reset (e k)
reset :: Cont a a > a
reset e = e `runCont` id
 The above example written in monadic style
* Main> reset $ (1 +) `fmap` shift (\k > return $ k 1 + k 2)
5
reset e
e
shift
Cont
shift
reset
call/cc
r
shift
reset
setting, it is necessary to express the answer type of the underlying continuation monad in the types. The HindleyMilner type system cannot express this, but luckily, Haskell allows type information to be hidden in contexts, which provides our approach with full static type safety as opposed to Filinski's implementation in SML.
Monadic Reflection
Monadic reflection #ref4 4 enables us to write monadic code in direct style.
reflect
language. The side effects can then be observed by "reifing" a value back into monadic form. For example,
#!syntax haskell
> reify (reflect [0,2] + reflect [0,1]) :: [Int]
and
> liftM2 (+) [0,2] [0,1]
[0,1,2,3]
In order to understand how monadic reflection can be implemented, we combine
the observation thatshift
reset
underlying continuation monad with an arbitrary answer type with Wadler's #ref5 5 observation that every monad can be embedded in the continuation
monad. So using a directstyleshift
reset
arbitrary monadic code in direct style.
Explicitly (but hiding the wrapping necessary for the ContT monad transformer), Wadler's transformation is as follows
#!syntax haskell
embed :: Monad m => m a > (forall r. (a > m r) > m r)
embed m = \k > k =<< m
project :: Monad m => (forall r. (a > m r) > m r) > m a
project f = f return
project . embed === id
embed
project
m
forall r. ContT m r a
Translating these morphisms into direct style, we immediately arrive at
Filinski'sreflect
reify
#!syntax haskell
reflect m = shift (\k > k =<< m)
reify t = reset (return t)
Now let us have a closer look at the above example to see how it works operationally.
#!syntax haskell
e = reify (reflect [0,2] + reflect [0,1])
Substituting the definitions, this becomes
#!syntax haskell
e = reset (return (shift (\k > k =<< [0,2]) + shift (\k > k =<< [0,1])))
which simplifies to
#!syntax haskell
e = reset [shift (\k > k 0 ++ k 2) + shift (\k' > k' 0 ++ k' 1)]
Assuming left to right evaluation, the result of this expression is
k 0 ++ k 2
k
#!syntax haskell
k = \x > reset [x + shift (\k' > k' 0 ++ k' 1)]
k'
\y > reset [x + y]
k
#!syntax haskell
k = \x > [x + 0] ++ [x + 1] = \x > [x,x+1]
Therefore, as we expected, the whole expression evaluates to
#!syntax haskell
e = k 0 ++ k 2 = [0,1] ++ [2,3] = [0,1,2,3]
Implicit Parameters
Implicit parameters #ref6 6 are GHCspecific type system extension providing dynamically bound variables. They are passed in the same way as type class dictionaries, but unlike type class dictionaries, their value can be changed for a subexpression. The types of the implicit parameters a function expects appear in type contexts which now make sense at arbitrary argument positions.
#!syntax haskell
addThree :: (?foo :: Int) => Int
addThree = 3 + ?foo
withFour :: ((?foo :: Int) => a) > a
withFour x = let ?foo = 4 in x
* Main> withFour addThree
7
We see that implicit parameters act like a reader monad written in direct style. The commutativity of the reader monad ensures that the code still is referentially transparent (the monomorphic recursion issue aside that will be discussed below).
Linear implicit parameters #ref6 6 work very much like regular implicit parameters, but the type of the parameter is required to be an instance of the
classGHC.Exts.Splittable
split :: a > (a,a)
parameter gets split, so that each value is used only once. However, as we shall later see, this linearity is not enforced in all circumstances, with higher order functions and a certain class of recursive functions being the notable exceptions.
Possible uses are random number distribution, fresh name generation (if you do not mind the names becoming very long) or a directstyle !QuickCheck #ref7 7. In this article, they will be used to store a subcontinuation from
an enclosingreset
?
%
illustrating their intended use.
#!syntax haskell
import qualified System.Random as R
instance Splittable R.StdGen where split = R.split
randInts :: R.StdGen > (Int, Int, Int)
randInts gen = let %gen = gen in (rand, rand, rand) where
rand :: (%gen :: R.StdGen) => Int
rand = fst $ R.random %gen
* Main> print . randInts =<< R.getStdGen
(1305955622,1639797044,945468976)
As in the implicit case, the semantics of linear implicit parameters can be described in terms of a "monad", which, however, does not obey the monad laws in any nontrivial case.
#!syntax haskell
newtype Split r a = Split { runSplit :: r > a }
instance Functor (Split r) where
f `fmap` Split x = Split $ f . x
instance Splittable r => Monad (Split r) where
return x = Split $ const x
Split x >>= f = Split $ \s >
let (s1,s2) = split s in f (x s1) `runSplit` s2
toSplit :: ((%foo :: r) => a) > Split r a
toSplit x = Split $ \r > let %foo = r in x
fromSplit :: Split r a > ((%foo :: r) => a)
fromSplit (Split f) = f %foo
The ability to freely transform between "monadic" and "implicit" style is often very helpful, e.g. to work around GHC's limitation that signature contexts in a mutually recursive group must all be identical.
Unsafe Operations
The code below uses two unsafe operations #ref8 8. We briefly discuss which conditions must be checked in order to ensure that they are used in a "safe" way.
#!syntax haskell
unsafePerformIO :: IO a > a
unsafeCoerce# :: a > b
unsafePerformIO
IO
result as a pure value. Thus, it should only be used if the result of the action does not depend on the state of the external world. However, we do not demand that the result of the computation be independent of the evaluation order. Furthermore, we must be aware that the compiler may inline function
definitions, so that two invocations ofunsafePerformIO
{# NOINLINE foo #
be used to forbid inlining in such cases.
TheunsafeCoerce#
are known to be equal although the type system cannot proof this fact. If the types do not match, its behavior is undefined; usually, the program will crash or return a wrong result.
Dynamic Exceptions
In addition to exceptions that only print an error message, the Hierarchical
Libraries provide thethrowDyn
catchDyn
exceptions of an arbitrary instance of the class Typeable. However, there is a tricky aspect of exceptions because of Haskell's laziness. Consider
#!syntax haskell
* Main> print =<< evaluate ([1,throwDyn "escape"])
`catchDyn` \"escape" > return [2]
[1,*** Exception: (unknown)
Here the evaluation of the list only determines whether the list is empty, but the list is inspected when the expression is printed, and thus the exception
escapes thecatchDyn
When all thrown exception have to be caught, we must evaluate the expression fully before handling the exception, which can
be ensured with theDeepSeq
#!syntax haskell
infixr 0 `deepSeq`, $!!
class DeepSeq a where
deepSeq :: a > b > b
($!!) :: (DeepSeq a) => (a > b) > a > b
f $!! x = x `deepSeq` f x
DeepSeq
IO
sensible way.
Implementation
This section discusses the implementation of the monadic reflection library. It safely be skipped, especially the first two subsections are very technical.
Basic Declarations
k :> v
Position
it should have the property that different sequences of applications of
leftPos
rightPos
initPos
Cell
Prompt
position
prompt
reset
facts
promptID
be used for exception handling.
#!syntax haskell
infixr 9 :>
lookup :: Ord k => (k :> v) > k > Maybe v
insert :: Ord k => (k :> v) > k > v > k :> v
empty :: k :> v
leftPos :: Position > Position
rightPos :: Position > Position
initPos :: Position
type Facts = Position :> Cell
data Cell = forall a. Cell a deriving Typeable
data Prompt r = Prompt {
position :: Position,
prompt :: Direct r r,
facts :: Facts,
promptID :: Unique
}
newPrompt :: Facts > Direct r r > Prompt r
instance Splittable (Prompt r) where
split p = (p {position = leftPos pos},
p {position = rightPos pos}) where
pos = position p
type Direct r a = (%ans :: Prompt r) => a
Shift and Reset
shift
Prompt
shift
facts
reset
f
shift
reset
f
Prompt
facts
shift
x
prompt
reset
f
reset
Prompt
r
Cell
r
Typeable
reset
Prompt
This gets a little more complicated because we need to be able to handle the
effects of nestedresets
#!syntax haskell
shift :: ((a > r) > Direct r r) > Direct r a
shift f :: Direct r a =
let ans :: Prompt r
ans = %ans
in case lookup (facts ans) (position ans) of
Just (Cell a) > unsafeCoerce# a
Nothing > throwDyn . (,) (promptID ans) . Cell . f $ \x >
let %ans = newPrompt
(insert (facts ans) (position ans) (Cell x))
(prompt ans)
in prompt ans
reset :: DeepSeq r => Direct r r > r
reset e :: r = let %ans = newPrompt empty res in res where
res :: Direct r r
res = unsafePerformIO $ do
let catchEsc e' = evaluate (id $!! e') `catchDyn`
\err@(i, Cell result) >
if i == promptID %ans
then catchEsc $ unsafeCoerce# result
else throwDyn err
catchEsc e
It is interesting to observe that in case of the error monad, this code uses
theIO
Finally, we need to check the unsafe features are used in a safe way as
described above. TheunsafeCoerce#
r
r
i == promptID
unsafePerformIO
used for a "pure exception handling", which destroys purity, but still satisfies the weaker condition that the behavior does not depend on the outside world, which is essential here, as we rely on the property that a computation performs exactly the same steps when rerun.
Reflection and Reification
With workingshift
reset
reflection primitives. We first consider the case of the continuation monad.
Reflecting the Cont Monad
#!syntax haskell
reflectCont :: Cont r a > Direct r a
reflectCont (Cont f) = shift f
reifyCont :: DeepSeq r => Direct r a > Cont r a
reifyCont e = Cont $ \k > reset (k e)
callCC
Control.Monad.Cont
to directstyle.
#!syntax haskell
callCC' :: DeepSeq r => ((a > b) > Direct r a) > Direct r a
callCC' f = reflectCont $ callCC $ \c > reifyCont $ f $ reflectCont . c
call/cc
shift
#!syntax haskell
callCC' :: ((forall b. a > b) > Direct r a) > Direct r a
callCC' f = shift $ \k > k $ f (\x > shift $ \_ > k x)
In both versions, the expression
#!syntax haskell
reset (callCC' (\k x > k (x+)) 5) :: Int
10
continuation monad; but be warned that it is a little harder than the above directstyle version.
Reflecting Arbitrary Monads
Now, implementingreflect
reify
shift
reset
#!syntax haskell
 Type alias for more concise type signatures of directstyle code.
type Monadic m a = forall r. Direct (m r) a
reflect :: Monad m => m a > Monadic m a
reflect m = shift (\k > k =<< m)
reify :: (DeepSeq (m a), Monad m) => Monadic m a > m a
reify t = reset (return t)
Interface
For quick reference, we repeat the type signatures of the most important library functions.
#!syntax haskell
type Direct r a = (%ans :: Prompt r) => a
shift :: ((a > r) > Direct r r) > Direct r a
reset :: DeepSeq r => Direct r r > r
type Monadic m a = forall r. Direct (m r) a
reflect :: Monad m => m a > Monadic m a
reify :: (DeepSeq (m a), Monad m) => Monadic m a > m a
Resolving Ambiguities
The use of linear implicit parameters comes with a few surprises. The GHC manual #ref6 6 even writes
 quote
So the semantics of the program depends on whether or not foo has a type
signature. Yikes!
You may say that this is a good reason to dislike linear implicit parameters
and you'd be right. That is why they are an experimental feature.
However, most of the problems can be circumvented quite easily, and the property that the meaning of a program can depend on the signatures given is actually a good thing.
Recursive Functions
Indeed, omitting a type signature can sometimes result in a different behavior. Consider the following code, where
shift (\k > k n)
n
#!syntax haskell
 Without the explicit signature for k GHC does not infer a
 sufficiently general type.
down 0 = []
down (n+1) = shift (\(k::Int > [Int]) > k n): down n
* Main> reset (down 4)
[3,3,3,3]  wrong!
down
down
down
actually be polymorphically recursive. This is semantically different and ensures the linearity. We can persuade GHC to treat it correctly by giving the function an explicit signature.
#!syntax haskell
down' :: Int > Direct [Int] [Int]
{ ... }
* Main> reset (down' 4)
[3,2,1,0]  right!
Furthermore, we have to watch out for a GHC bug #ref10 10 that appears to happen when expressions with differently polymorphic linear implicit parameter constraints are unified. In the above example, this occurs when
k
down
Int > Direct r [Int]
Higher order functions
Implicit parameters are particularly tricky when functions using implicit parameters are passed to higher order functions. Consider the following example.
#!syntax haskell
 The prelude definition of the function map
map :: (a > b) > [a] > [b]
map _ [] = []
map f (x:xs) = f x : map f xs
foo :: [[Int]]
foo = reify (map f [1,2,3]) where
f :: Int > Monadic [] Int
f x = reflect [x,x]
* Main> foo
[[1,1,1],[1,1,1]]  wrong!
The first surprise is that this code type checks at all: The type of the
functionf
Int > Monadic [] Int
map
f
Monadic [] (Int > Int)
GHC pushes contexts at covariant argument positions as far to the left as possible using a technique called forallhoisting #ref6 6, which is of course sensible for type class constraints and implicit parameters, but destroys the linearity, which seems bad even in the motivating examples of random number or fresh name generation, and is only OK in the !QuickCheck example. So we always have to watch out for effectful functions that are passed as parameters, but at least we can copy the implementation of the higher order functions we want to use.
#!syntax haskell
map' :: (a > Direct r b) > [a] > Direct r [b]
{ Implementation as above }
foo = reify (map' f [1,2,3]) where { ... }
* Main> foo
[[1,2,3],[1,2,3],[1,2,3],[1,2,3],[1,2,3],[1,2,3],[1,2,3],
[1,2,3]]  right!
The Monomorphism Restriction
What should the expression
#!syntax haskell
reify (let x = reflect [0,1] in [x,x+2,x+4])
evaluate to? Two possibilities come to mind: Either we choose a value for the
variablex
[x,x+2,x+4]
x
[0,1]
x
0
1
x
immediately clear how both variants can be achieved in monadic style.
#!syntax haskell
* Main> do x < [0,1]; return [x,x+2,x+4]
[[0,2,4],[1,3,5]]
* Main> let x = [0,1] in sequence [x,(+2) `fmap` x, (+4) `fmap` x]
[[0,2,4],[0,2,5],[0,3,4],[0,3,5],[1,2,4],[1,2,5],[1,3,4],[1,3,5]]
In direct style, this is even easier, but the meaning of our code now depends on the type signature.
#!syntax haskell
* Main> reify (let x :: Int; x = reflect [0,1] in [x,x+2,x+4])
[[0,2,4],[1,3,5]]
* Main> reify (let x :: Monadic [] Int; x = reflect [0,1] in [x,x+2,x+4])
[[0,2,4],[0,2,5],[0,3,4],[0,3,5],[1,2,4],[1,2,5],[1,3,4],[1,3,5]]
It is important that we give a real type signature:
x :: Int = reflect [0,1]
This is a nice and very natural way to describe both situations, but the answer to the question which one GHC chooses when no signature is given is less satisfactory: It depends on the status of the flag
f(no)monomorphismrestriction
x
a monomorphic type, so the first situation applies, without the restriction
x
opinion, it would be nice if there were a flag that, in order to give the programmer a chance to disambiguate his code, causes a warning to be emitted whenever the monomorphism restriction kicks in; a similar warning has been proven useful to detect numeric defaulting.
Examples
We now present some examples reflecting theCont
[]
Lazy Evaluation
The use of monads in Haskell models an impure language with callbyvalue semantics. This is not surprising as one motivation for the use of monads is the need to do IO. For IO, evaluation order is important and callbyvalue
makes evaluation order easier to reason about. For theIO
unsafeInterleaveIO
IO
But such a lazy monadic behavior would be practical for other monads, too: The list monad is very susceptible to space leaks and unnecessary recomputation. The reflected list monad, however, is often closer to the desired behavior, as the following examples suggest.
#!syntax haskell
 Lazy repeat, Prelude.repeat would allow the side effect
 of the argument to take place only once
repeat' :: Direct r a > Direct r [a]
repeat' x = x:repeat' x
* Main> take 3 `fmap` sequence (repeat [1,2::Int])
<< Does not terminate. >>
* Main> reify (take 3 $ repeat' (reflect [1,2::Int]))
[[1,1,1],[1,1,2],[1,2,1],[1,2,2],[2,1,1],[2,1,2],[2,2,1],[2,2,2]]
* Main> fst `fmap` liftM2 (,) [1,2::Int] [3,4::Int]
[1,1,2,2]
* Main> reify (fst (reflect [1,2::Int], reflect [3,4::Int]))
[1,2]
* Main> reify (fst $!! (reflect [1,2::Int], reflect [3,4::Int]))
[1,1,2,2]
The last expression shows that we can easily revert to the eager version by adding appropriate strictness annotations.
Filtering Permutations
As a typical problem where the lazy behavior of our implementation is advantageous, we consider a small combinatorial example: Find all permutations of
#!latex
$(1,2,4,...,2^{n1})$
such that all the sums of the initial sequences of the permutations are primes.
#!syntax haskell
 NB. This section's example code can be found in the files Perms.*.
 _very_ simple primality test.
isPrime :: Int > Bool
isPrime n = n >= 2 && all (\k > n `mod` k /= 0)
(takeWhile (\k > k*k <= n) $ 2:[3,5..])
 check if all the initial sums are primes.
goodPerm :: [Int] > Bool
goodPerm xs = all isPrime (scanl1 (+) xs)
If we want to solve the problem in Haskell, we need to make a big compromise: Either we take the easy road and generate a list of the permutations and then
filter
permutations must be checked even if it already turns out after inspecting a few list elements that no permutation starting this way can have the property.
Alternatively, we can handoptimize the algorithm by performing the construction of the permutation stepwise and interleaving the primality checks appropriately. In our example, this is not really hard and the list monad is a great help, but it feels lowlevel, errorprone and lacks modularity. We would like the declarativity of the first approach while retaining the speed improvements the lazy checking provides.
So, should we to switch to another language? An obvious candidate is curry #ref12 12, a lazily evaluated hybrid functionallogic language with a very Haskelllike syntax and feel. Curry allows nondeterministic functions to be written by simply declaring the function multiple times; however, the nondeterminacy cannot be expressed on the type level. Using monadic reflection, we can do something very similar as follows.
#!syntax haskell
 nondeterministic choice
(?) :: DeepSeq a => Monadic [] a > Monadic [] a > Monadic [] a
x ? y = reflect (reify x `mplus` reify y)
 nondeterministically select a permutation
permute :: [Int] > Monadic [] [Int]
permute [] = []
permute xs = y: permute ys where
y::Int; ys::[Int]
(y,ys) = select xs
select :: [Int] > Monadic [] (Int,[Int])
select [] = reflect []
select (x:xs) = (x,xs) ? second (x:) (select xs) where
 a special case of Control.Arrow.second
second f (x,y) = (x,f y)
Now we only need to ensure that the computation fails when the permutation does not have the desired property.
#!syntax haskell
solve :: Int > Monadic [] [Int]
solve n = if goodPerm xs then xs else reflect [] where
xs :: [Int]
xs = permute $ map (2^) [0..n1]
* Main> reify (solve 17)
[[2,1,4,1024,512,16,8,65536,128,4096,32,16384,32768,256,8192,64,2048],
[2,1,4,1024,512,16,2048,16384,8192,65536,32768,64,32,256,128,4096,8]]
The relative performance of the different approaches is not surprising: The manual Haskell solution (GHC) is the fastest, the Curry solution (Muenster Curry) is about six times slower while the solution using monadic reflection is another four times slower (and gets slightly worse for larger values of
n
shift
reset
years to finish.
Further Ideas
This section discusses some further directions in which the ideas of this article might be extended.
Denotational Semantics
The relationship between laziness and directstyle continuation effects, despite often following the intuition, needs some further clarification. For that purpose, I wrote two interpreters of a simple untyped combinator language, which use a continuationlike monad and the monadic reflection library, respectively. They can be checked for coincidence using !QuickCheck tests generating typechecking expressions for the language. The monad
the interpreter is built upon is anST
Int
ContT
#!syntax haskell
newtype Eval s a
= Eval { runEval :: ContT Int (ST s) a }
deriving (Functor, Monad)
The interpreter maps the source language's expressions into the following universal type.
#!syntax haskell
type U s = Eval s (Ref s `Either` U' s)
data U' s
= Int { runInt :: Int }
 Fun { runFun :: U s > U s }
 List { runList :: Maybe (U s, U s) }
newtype Ref s = Ref { unRef :: STRef s (U' s `Either` U s) }
U s
U' s
U s
U' s
#!syntax haskell
 Delays a computation
delay :: U s > U s
 Force evaluation of a reference to a normal form.
force :: U s > Eval s (U' s)
Details can be found in the [attachment:Reflection.tar.gz tarball] provided with this article. The distribution also contains two interpreters for a strict version of the language, which can be more straightforwardly implemented using the plain continuation monad and, in case of the directstyle interpreter, some strictness annotations.
A Lightweight Notation for Monads
Haskell's donotation is often criticized being too verbose, especially for commutative monads; and the process of transforming pure functions into monadic style because some (possibly deeply nested) function needs some effects is tedious and errorprone.
GHC already has special support for the (commutative) reader monad, through implicit parameters. This special rÙle of the reader monad might be justified by additional properties this monad has, for example that there are
isomorphisms of typem (a > b) > a > m b
m (a, b) > (m a, m b)
\f x > f `ap` return x
liftM2 (,)
Also, special tools #ref13 13 are being developed that automatically transform a function from direct into monadic style, but this process requires arbitrary decisions where to apply effects, e.g. it is unclear if
a function of typeInt > Bool
Monad m => m Int > m Bool
Monad m => Int > m Bool
both make sense in different circumstances.
As we showed in this article, Haskell's type system is almost ready to express these differences on the type level; the only remaining problem is that forallhoisting [6] changes the meaning of expressions. On the other hand, because of the interaction with laziness, keeping the semantics of the library described in this article would result in a rather complicated translation, as we saw in the last section. In order to get rid of this obscurity, one might imagine a typedirected translation which translates (pseudocode)
#!syntax haskell
reflect :: m a > (<m> => a)
reify :: Monad m => (<m> => a) > m a
foo :: <[]> => Int
foo = reflect [0,2] + reflect [0,1]
bar :: [Int]
bar = reify foo
more strictly into
#!syntax haskell
foo :: [Int]
foo = (+) `fmap` [0,2] `ap` [0,1]
bar :: [Int]
bar = foo
However, this contradicts Haskell's philosophy to make invocation of effects as explicit as possible, and would probably be considered an "underkill". Moreover, it would require a decent solution to the monomorphism restriction problem.
Conclusion
Do not take this too seriously: Our code heavily relies on unsafe and experimental features; time and space usage are increased by the suboptimal encoding of continuations and the recomputations; and the number of supported
monads is limited by theDeepSeq
However, we provided a framework with strong static guarantees in which it is
easy to experiment with the unfamiliarshift
reset
and we learned that GHC Haskell's type system goes well beyond HindleyMilner and it is almost ready for an impure language where effects are declared explicitly on the type level.
More importantly, it is great fun to abuse just about every unsafe feature of (GHC) Haskell, to create an impure sublanguage with monadic effects.
Acknowledgments
I would like to thank the GHC team for this great compiler with its many fascinating extensions.
I also want to thank Peter Eriksen, Cale Gibbard and Don Stewart for proofreading the article and their valuable suggestions, as well as Brandon Moore and Autrijus Tang for their advice on the references.
References
Anchor(ref1) [1] Olivier Danvy and Andrzej Filinski. "A Functional Abstraction of Typed Contexts". DIKU. DIKU Rapport 89/12. July 1989. Available online: http://www.daimi.au.dk/~danvy/Papers/fatc.ps.gz
Anchor(ref2) [2] Chungchieh Shan. "Shift to Control". 2004 Scheme Workshop. September 2004. Available online: http://repository.readscheme.org/ftp/papers/sw2004/shan.pdf
Anchor(ref3) [3] R. Kent Dybvig, Simon PeytonJones, and Amr Sabry. "A Monadic Framework for Subcontinuations". February 2005. Available online: http://www.cs.indiana.edu/~sabry/papers/monadicSubcont.ps
Anchor(ref4) [4] Andrzej Filinski. Representing monads. In Conference Record of POPL '94: 21st ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, Portland, Oregon, pages 446457. Available online: http://citeseer.ist.psu.edu/filinski94representing.html
Anchor(ref5) [5] Philip Wadler. "The essence of functional programming". Invited talk, 19'th Symposium on Principles of Programming Languages, ACM Press. January 1992. Available online: http://homepages.inf.ed.ac.uk/wadler/papers/essence/essence.ps
Anchor(ref6) [6] The GHC Team. "The Glorious Glasgow Haskell Compilation System User's Guide, Version 6.4". BR Linear Implicit Parameters: http://haskell.org/ghc/docs/6.4/html/users_guide/typeextensions.html#implicitparameters BR Implicit Parameters: http://haskell.org/ghc/docs/6.4/html/users_guide/typeextensions.html#linearimplicitparameters BR ForallHoisting: http://haskell.org/ghc/docs/latest/html/users_guide/typeextensions.html#hoist
Anchor(ref7) [7] Koen Claessen and John Hughes. "!QuickCheck: An Automatic Testing Tool for Haskell". http://www.cs.chalmers.se/~rjmh/QuickCheck/
Anchor(ref8) [8] Simon Peyton Jones. "Tackling the awkward squad: monadic input/output, concurrency, exceptions, and foreignlanguage calls in Haskell". In "Engineering theories of software construction, ed Tony Hoare, Manfred Broy, Ralf Steinbruggen, IOS Press, ISBN 1 58603 1724, 2001, pp4796. Available online: http://research.microsoft.com/Users/simonpj/papers/marktoberdorf/mark.pdf
Anchor(ref9) [9] Dean Herington. "Enforcing Strict Evaluation". Mailing list post. http://www.haskell.org/pipermail/haskell/2001August/007712.html
Anchor(ref10) [10] Thomas J‰ger "Linear implicit parameters: linearity not enforced". Mailing list post. http://www.haskell.org/pipermail/glasgowhaskellbugs/2005March/004838.html
Anchor(ref11) [11] Simon Peyton Jones [editor] "The Revised Haskell Report". 2002. Section, 4.5.5, "The Monomorphism Restriction". http://www.haskell.org/onlinereport/decls.html#sect4.5.5
Anchor(ref12) [12] Michael Hanus [editor] "Curry. An Integrated Functional Logic Language". Available online: http://www.informatik.unikiel.de/~mh/curry/papers/report.pdf
Anchor(ref13) [13] "Monadification as a Refactoring". http://www.cs.kent.ac.uk/projects/refactorfp/Monadification.html