# The Monad.Reader/Issue2/FunWithLinearImplicitParameters

### From HaskellWiki

**Fun with Linear Implicit Parameters**

*by Thomas Jäger*

**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 side-effecting code. In this article, we take the next step of impure programming by implementing Filinski's

## Contents |

## 1 Introduction

The following sections provide a short introduction into the various concepts our implementation uses. The code presented here is no longer available as an attachment. It has however been successfully tested with ghc-6.2.2 and ghc-6.4.

### 1.1 Shift and Reset

Thereset (1 + shift (\k -> k 1 + k 2)) :: Int

-- 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

### 1.2 Monadic Reflection

Monadic reflection [4] enables us to write monadic code in direct style.> reify (reflect [0,2] + reflect [0,1]) :: [Int]

and

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

Explicitly (but hiding the wrapping necessary for the ContT monad transformer), Wadler's transformation is as follows

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

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.

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

Substituting the definitions, this becomes

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

which simplifies to

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

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

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

Therefore, as we expected, the whole expression evaluates to

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

### 1.3 Implicit Parameters

Implicit parameters [7] are GHC-specific 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.

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 [6] work very much like regular implicit parameters, but the type of the parameter is required to be an instance of the classimport 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.

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.

### 1.4 Unsafe Operations

The code below uses two unsafe operations [7]. We briefly discuss which conditions must be checked in order to ensure that they are used in a "safe" way.

unsafePerformIO :: IO a -> a unsafeCoerce# :: a -> b

### 1.5 Dynamic Exceptions

In addition to exceptions that only print an error message, the Hierarchical Libraries provide the* Main> print =<< evaluate ([1,throwDyn "escape"]) `catchDyn` \"escape" -> return [2] [1,*** Exception: (unknown)

infixr 0 `deepSeq`, $!! class DeepSeq a where deepSeq :: a -> b -> b ($!!) :: (DeepSeq a) => (a -> b) -> a -> b f $!! x = x `deepSeq` f x

## 2 Implementation

This section discusses the implementation of the monadic reflection library. It safely be skipped, especially the first two subsections are very technical.

### 2.1 Basic Declarations

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

### 2.2 Shift and Reset

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

### 2.3 Reflection and Reification

With working#### 2.3.1 Reflecting the Cont Monad

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' :: DeepSeq r => ((a -> b) -> Direct r a) -> Direct r a callCC' f = reflectCont $ callCC $ \c -> reifyCont $ f $ reflectCont . c

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

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

#### 2.3.2 Reflecting Arbitrary Monads

Now, implementing-- Type alias for more concise type signatures of direct-style 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)

## 3 Interface

For quick reference, we repeat the type signatures of the most important library functions.

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

## 4 Resolving Ambiguities

The use of linear implicit parameters comes with a few surprises. The GHC manual [6] even writes

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.

### 4.1 Recursive Functions

Indeed, omitting a type signature can sometimes result in a different behavior. Consider the following code, where-- 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' :: Int -> Direct [Int] [Int] {- ... -} * Main> reset (down' 4) [3,2,1,0] -- right!

### 4.2 Higher order functions

Implicit parameters are particularly tricky when functions using implicit parameters are passed to higher order functions. Consider the following example.

-- 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!

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!

### 4.3 The Monomorphism Restriction

What should the expression

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

* 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.

* 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:

## 5 Examples

We now present some examples reflecting the### 5.1 Lazy Evaluation

The use of monads in Haskell models an impure language with call-by-value 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 call-by-value makes evaluation order easier to reason about. For theBut 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.

-- 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.

### 5.2 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

$(1,2,4,...,2^{n-1})$

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

-- 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)

*all*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 hand-optimize the algorithm by performing the construction of the permutation step-wise 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 low-level, error-prone 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 [12], a lazily evaluated hybrid functional-logic language with a very Haskell-like 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.

-- 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.

solve :: Int -> Monadic [] [Int] solve n = if goodPerm xs then xs else reflect [] where xs :: [Int] xs = permute $ map (2^) [0..n-1] * 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]]

## 6 Further Ideas

This section discusses some further directions in which the ideas of this article might be extended.

### 6.1 Denotational Semantics

The relationship between laziness and direct-style 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 continuation-like monad and the monadic reflection library, respectively. They can be checked for coincidence using !QuickCheck tests generating type-checking expressions for the language. The monad the interpreter is built upon is annewtype 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.

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) }

-- 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 direct-style interpreter, some strictness annotations.

### 6.2 A Lightweight Notation for Monads

Haskell's do-notation 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 error-prone.

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 typeAs 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 forall-hoisting [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 type-directed translation which translates (pseudo-code)

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

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.

## 7 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 the## 8 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 proof-reading the article and their valuable suggestions, as well as Brandon Moore and Autrijus Tang for their advice on the references.

## 9 References

[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

[2] Chung-chieh Shan. "Shift to Control". *2004 Scheme Workshop*.
September 2004. Available online:
http://repository.readscheme.org/ftp/papers/sw2004/shan.pdf

[3] R. Kent Dybvig, Simon Peyton-Jones, and Amr Sabry. "A Monadic Framework for Subcontinuations". February 2005. Available online: http://www.cs.indiana.edu/~sabry/papers/monadicSubcont.ps

[4] Andrzej Filinski. Representing monads.
*In Conference Record of POPL '94: 21st ACM SIGPLAN-SIGACT Symposium on*
Principles of Programming Languages, Portland, Oregon, pages 446--457.
Available online:
http://citeseer.ist.psu.edu/filinski94representing.html

[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

[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/type-extensions.html#implicit-parameters BR Implicit Parameters: http://haskell.org/ghc/docs/6.4/html/users_guide/type-extensions.html#linear-implicit-parameters BR Forall-Hoisting: http://haskell.org/ghc/docs/latest/html/users_guide/type-extensions.html#hoist

[7] Koen Claessen and John Hughes. "!QuickCheck: An Automatic Testing Tool for Haskell". http://www.cs.chalmers.se/~rjmh/QuickCheck/

[8] Simon Peyton Jones.
"Tackling the awkward squad: monadic input/output, concurrency, exceptions, and
foreign-language calls in Haskell".
*In "Engineering theories of software construction, ed Tony Hoare, Manfred*
Broy, Ralf Steinbruggen, IOS Press, ISBN 1 58603 1724, 2001, pp47-96*.*
Available online:
http://research.microsoft.com/Users/simonpj/papers/marktoberdorf/mark.pdf

[9] Dean Herington. "Enforcing Strict Evaluation". Mailing list post. http://www.haskell.org/pipermail/haskell/2001-August/007712.html

[10] Thomas J‰ger "Linear implicit parameters: linearity not enforced". Mailing list post. http://www.haskell.org/pipermail/glasgow-haskell-bugs/2005-March/004838.html

[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

[12] Michael Hanus [editor] "Curry. An Integrated Functional Logic Language". Available online: http://www.informatik.uni-kiel.de/~mh/curry/papers/report.pdf

[13] "Monadification as a Refactoring". http://www.cs.kent.ac.uk/projects/refactor-fp/Monadification.html