October 2010 - Haskell-Cafe

Re: [Haskell] Specification and prover for Haskell
by Dominique Devriese 25 Oct '10

25 Oct '10

Romain, 2010/10/25 Romain Demeyer <rde(a)info.fundp.ac.be>: > I'm working on static verification in Haskell, and I search for existing > works on specification of Haskell programs (such as pre/post conditions, for > example) or any other functional language. It would be great if there exists > a prover based on this kind of specifications. I already found the > ESC/Haskell. Do you know some other works which could be interesting? I found the paper "Verifying Haskell using constructive type theory" [1] interesting... Dominique Footnotes: [1] http://www.mimuw.edu.pl/~ben/Papers/monadic.pdf

1 0

Converting Values Between Lua And Haskell
by aditya siram 25 Oct '10

25 Oct '10

Hi all, The HsLua page [1] says that Int,Double,String,Bool,[a] and [(a,b)] types can be converted to and from Lua values. However the on hslua API page I don't see a StackValue instance [2] for [a] or [(a,b)]. Am I missing something? -deech [1] http://www.haskell.org/haskellwiki/HsLua#Exchanging_data_between_Haskell_an… [2] http://hackage.haskell.org/packages/archive/hslua/latest/doc/html/Scripting…

3 3

ANNOUNCE: iteratee-compress 0.1.1
by Maciej Piechotka 24 Oct '10

24 Oct '10

Iteratee-compress provides compressing and decompressing enumerators including flushing. Currently only gzip is provided but at least bzip is planned. Changes from previous version: - Independent from zlib library (Haskell one, not C) - Allow hand-flushing the contents (from outside). - Fix potential memory-leak Next goals: - BZip support - Generic interface for flushing To think about: - Should inner iteratee be able to request flushing? Regards PS. It did change API by removing dependency on zlib but I home such breakage in 0.1.x will be allowed

4 5

Eta-expansion and existentials (or: types destroy my laziness)
by Max Bolingbroke 24 Oct '10

24 Oct '10

Hi Cafe, I've run across a problem with my use of existential data types, whereby programs using them are forced to become too strict, and I'm looking for possible solutions to the problem. I'm going to explain what I mean by using a literate Haskell program. First, the preliminaries: > {-# LANGUAGE ExistentialQuantification #-} > import Control.Arrow (second) > import Unsafe.Coerce Let's start with a simple example of an existential data type: > data Stream a = forall s. Stream s (s -> Maybe (a, s)) This is a simplified version of the type of streams from the stream fusion paper by Coutts et al. The idea is that if you have a stream, you have some initial state s, which you can feed to a step function. The step function either says "Stop! The stream has ended!", or yields an element of the stream and an updated state. The use of an existential quantifier is essential to this code, because it means that we can write most functions on Streams in a non-recursive fashion. This in turn makes them amenable to inlining and simplification by GHC, which gives the us the loop fusion we need. An example stream is that of natural numbers: > nats :: Stream Int > nats = Stream 0 (\n -> Just (n, n + 1)) Here, the state is just the next natural number to output. We can also build the list constructors as functions on streams: > nil :: Stream a > nil = Stream () (const Nothing) > cons :: a -> Stream a -> Stream a > cons a (Stream s step) = Stream Nothing (maybe (Just (a, Just s)) (fmap (second Just) . step)) List functions can also easily be expressed: > taken :: Int -> Stream a -> Stream a > taken n (Stream s step) = Stream (n, s) (\(n, s) -> if n <= 0 then Nothing else maybe Nothing (\(a, s) -> Just (a, (n - 1, s))) (step s)) To see this all in action, we will need a Show instance for streams. Note how this code implements a loop where it repeatedly steps the stream (starting from the initial state): > instance Show a => Show (Stream a) where > showsPrec _ (Stream s step) k = '[' : go s > where go s = maybe (']' : k) (\(a, s) -> shows a . showString ", " $ go s) (step s) We can now run code like this: > test1 = do > print $ (nil :: Stream Int) -- [] > print $ cons 1 nil -- [1, ] > print $ taken 1 $ cons 1 $ cons 2 nil -- [1, ] Now we may wish to define infinite streams using value recursion: > ones :: Stream Int > ones = cons 1 ones Unfortunately, 'ones' is just _|_! The reason is that cons is strict in its second argument. The problem I have is that there is no way to define cons which is simultaneously: 1. Lazy in the tail of the list 2. Type safe 3. Non-recursive If you relax any of these constraints it becomes possible. For example, if we don't care about using only non-recursive functions we can get the cons we want by taking a roundtrip through the skolemized (existiental-eliminated - see http://okmij.org/ftp/Computation/Existentials.html) version of streams: > data StreamSK a = StreamSK (Maybe (a, StreamSK a)) > > skolemize :: Stream a -> StreamSK a > skolemize (Stream s step) = StreamSK (fmap (\(a, s') -> (a, skolemize (Stream s' step))) $ step s) > > unskolemize :: StreamSK a -> Stream a > unskolemize streamsk = Stream streamsk (\(StreamSK next) -> next) > > instance Show a => Show (StreamSK a) where > showsPrec _ (StreamSK mb_next) k = maybe (']' : k) (\(a, ssk) -> shows a . showString ", " $ shows ssk k) mb_next Now we can define: > cons_internally_recursive x stream = cons x (unskolemize (skolemize stream)) This works because unskolemize (skolemize stream) != _|_ even if stream is bottom. However, this is a non-starter because GHC isn't able to fuse together the (recursive) skolemize function with any consumer of it (e.g. unskolemize). In fact, to define a correct cons it would be sufficient to have some function (eta :: Stream a -> Stream a) such that (eta s) has the same semantics as s, except that eta s /= _|_ for any s. I call this function eta because it corresponds to classical eta expansion. We can define a type class for such operations with a number of interesting instances: > class Eta a where > -- eta a /= _|_ > eta :: a -> a > > instance Eta (a, b) where > eta ~(a, b) = (a, b) > > instance Eta (a -> b) where > eta f = \x -> f x > > instance Eta (StreamSK a) where > eta ~(StreamSK a) = StreamSK a If we had an instance for Eta (Stream a) we could define a lazy cons function: > cons_lazy :: a -> Stream a -> Stream a > cons_lazy x stream = cons x (eta stream) As we have already seen, one candidate instance is that where eta = unskolemize . skolemize, but I've already ruled that possibility out. Given that constraint, the only option that I see is this: > instance Eta (Stream a) where > -- Doesn't type check, even though it "can't go wrong": > --eta stream = Stream (case stream of Stream s _ -> s) (case stream of Stream _ step -> step) > eta stream = Stream (case stream of Stream s _ -> unsafeCoerce s :: ()) (case stream of Stream _ step -> unsafeCoerce step) I've had to use unsafeCoerce to make this go through, because I can't see any type-correct way of defining eta-expansion of existential data types - and indeed GHC complains if you try to use the ~pattern notation to define it. Nonetheless, it is "obvious" that 'eta' can't actually go wrong (in Milners's sense of the term). Now we can define the infinite stream we originally wanted: > lazy_ones :: Stream Int > lazy_ones = cons_lazy 1 lazy_ones > > test2 = print $ taken 2 $ lazy_ones -- [1, 1, ] Finally, here is some code to actually run the tests: > main = do > test1 > test2 So, cafe: is there any way to define a cons that satisfies my three earlier conditions: 1. Lazy in the tail of the list 2. Type safe 3. Non-recursive Or am I going to have to stick with my slightly unsafe eta that uses unsafeCoerce? Cheers, Max

3 4

"back doors" into the IO monad
by Manlio Perillo 24 Oct '10

24 Oct '10

Hi. What are the available methods to execute IO actions from pure code? I know only unsafePerformIO and foreign import (to call a non pure foreign function). Assuming I want to execute external untrusted code using plugins (via the `plugins` package), is it possible to completely forbid execution of IO actions from user code? Thanks Manlio

4 3

Haddock: patch to generate single-index page in addition to perl-letter indexes indices.
by Ryan Newton 24 Oct '10

24 Oct '10

When I encounter a split-index (A-Z) page it can be quite frustrating if I don't know the first letter of what I'm searching for. I want to use my browser find! For example, tonight I wanted to look at all the functions that END in "Window" in the Chart package -- no luck: * http://hackage.haskell.org/packages/archive/Chart/0.13.1/doc/html/doc-index… * * * *Therefore I propose that even when generating the "A-Z" individual pages that there also be an "All" option for the single-page version. Attached is a patch against haddock's HEAD (darcs get http://code.haskell.org/haddock/right?) that implements this behavior. As an example, here is FGL's documentation built with the patched haddock:* * * * http://people.csail.mit.edu/newton/fgl_example_doc/doc-index.html* The great thing about hackage being centralized is that if people are happy with this fix it can be widely deployed where it counts, and quickly! *Cheers,* * -Ryan* * * P.S. At the other end of the spectrum, when considering a central index for all of hackage (as in the below ticket) maybe it would be necessary to have more than 26 pages, I.e. Aa-Am | An-Az or whatever. http://hackage.haskell.org/trac/hackage/ticket/516#comment:6

3 3

Re: [Haskell-cafe] concurrency vs. I/O in GHC
by John Lato 24 Oct '10

24 Oct '10

> > From: Donn Cave <donn(a)avvanta.com> > > [I wrote initially, ...] > > > As I have migrated more of my application into Haskell, I find that > > I/O in one thread effectively blocks other threads. > > Resolved - the SSL_read external I/O function needs to be "safe". If anyone is listening, I would very much like for there to be a mechanism by which external functions can be called "unsafe"-ly, but without blocking all other Haskell threads. I have code that does this: calcUpdate a b c = do expensiveComputation a b expensiveComputation a c "expensiveComputation" mutates the second argument (b or c here), but does not call back into Haskell or update "a" and I would very much like to run these two in parallel, however it's not possible if "expensiveComputation" is unsafe. If I make "expensiveComputation" safe, the extra time necessary for safe-ness outweighs the gains from parallelization for even reasonably-sized inputs (the expensiveComputation is called 100k's of times or more). My current plan is to handle the parallelization in C, but I'd prefer to do it in Haskell if possible. John

7 10

Splay tree in a pattern matching way
by Xinyu LIU 24 Oct '10

24 Oct '10

Hi, I checked the Hackage Splay Tree implementation from. http://hackage.haskell.org/packages/archive/TreeStructures/0.0.1/doc/html/s… Basically it's based on the strategy mentioned in Okasaki's ``Purely Functional Programming'', Chapter 5.4. That in case we traverse twice in left (or right), we rotate the tree, so in long term of view, the tree turns more and more balanced. There are 3 cases for splay: zig-zig case, zig-zag case and zig case according to http://en.wikipedia.org/wiki/Splay_tree So I wonder if Splay tree can also be implemented by using pattern matching in a similar way as red black tree. Here is a draft source code: >>> data STree a = E -- Empty | Node (STree a) a (STree a) -- left, element, right deriving (Eq, Show) -- splay by pattern matching splay :: (Eq a) => STree a -> a ->STree a -- zig-zig splay t@(Node (Node (Node a x b) p c) g d) y = if x == y then Node a x (Node b p (Node c g d)) else t splay t@(Node a g (Node b p (Node c x d))) y = if x == y then Node (Node (Node a g b) p c) x d else t -- zig-zag splay t@(Node (Node a p (Node b x c)) g d) y = if x == y then Node (Node a p b) x (Node c g d) else t splay t@(Node a g (Node (Node b x c) p d)) y = if x == y then Node (Node a g b) x (Node c p d) else t -- zig splay t@(Node (Node a x b) p c) y = if x == y then Node a x (Node b p c) else t splay t@(Node a p (Node b x c)) y = if x == y then Node (Node a p b) x c else t -- otherwise splay t _ = t -- insert by using pattern matching insert :: (Ord a) => STree a -> a -> STree a insert E y = Node E y E insert (Node l x r) y | x < y = splay (Node (insert l y) x r) y | otherwise = splay (Node l x (insert r y)) y <<< I am not quite sure if the solution is correct and what about the efficiency of this code. Regards. -- Larry. LIU Xinyu http://sites.google.com/site/algoxy<http://sites.google.com/site/algoxy/home>

2 1

Haskellers design
by Michael Snoyman 23 Oct '10

23 Oct '10

I've gotten two offers for designs for Haskellers. The one uses the Haskell color theme choices we seem to be standardizing on as a community, the other uses a more custom theme. There is a screenshot of the former[1] and a demo page for the latter[2]. So the questions are: * How important is adhering to a "standard" look? * Which theme is overall more visually appealing? * Which theme gives a more professional feel? Please note that questions 1 and 2 may have different answers. Keep in mind when evaluating these themes, especially the first, that it is *not* in finalized form, just an basic idea of what could be. A third option that I have not pursued yet due to time constraints would be to leave the layout as-is currently but replace it with the Haskell color scheme. Yet another option would be to take the second theme mentioned above and try to force the Haskell color theme on it; I don't find that a good idea. Options 5 and 6 are leaving the site as it is (both layout and design), or proposing a totally different layout. Michael [1] http://imgur.com/lnkE7.png [2] http://previasports.com/haskellers_website/

7 9

Error Calling Lua Function
by aditya siram 23 Oct '10

23 Oct '10

Hi all, I'm having some issues calling Lua functions from Haskell. I have the following in "Haskell2Lua.lua": function hello () return "hello world" end And my Haskell file "Haskell2Lua.hs" looks like this: import qualified Scripting.Lua as Lua main = do l <- Lua.newstate Lua.openlibs l succ <- Lua.loadfile l "/Haskell2Lua.lua" print succ Lua.callproc l "hello" "" Lua.close l When I compile and run this file I get: 0 Haskell2Lua: user error (attempt to call a nil value) I have tried some variations on calling the function including: Lua.callproc l "hello" Lua.callfunc l "hello" Lua.callfunc l "hello" "" I know the Lua bridge is working because the following works: Lua.callproc l "print" "Hello from Lua" Any help is appreciated! -deech

3 4