October 2007 - Haskell-Cafe

Re: [Haskell] Announce: generating free theorems, online and offline
by ajb＠spamcop.net 19 Oct '07

19 Oct '07

[Ccing to haskell-cafe; please direct any replies there instead of haskell] G'day all. First of all, once again well done to Sascha on a great tool. Just a few comments. Quoting Janis Voigtlaender <voigt(a)tcs.inf.tu-dresden.de>: > - support for type classes > (e.g., enter "elem" and note the generated respects-restrictions) This is a great feature, and it'll be even better when constructor classes are done. Some of these respects-restrictions arent as useful as they might be, because they don't take into account easily-predictable invariants. For example, the type: (Eq a) => [a] -> [a] generates the following restriction: g respects Eq if forall x :: t1. forall y :: t1. (==) x y = (==) (g x) (g y) forall x :: t1. forall y :: t1. (/=) x y = (/=) (g x) (g y) Thats correct, but redundant, because (x == y) = (g x == g y) if and only if (x /= y) = (g x /= g y). Crucially, you can work this out from the definition of Eq, because (/=) has a default implementation defined in terms of (==) alone. The type (Monoid a) => [a] -> a gives: forall t1,t2 in TYPES(Monoid), g :: t1 -> t2, g respects Monoid. forall x :: [t1]. g (f x) = f (map g x) The class restriction occurring therein is defined as follows: g respects Monoid if g mempty = mempty forall x :: t1. forall y :: t1. g (mappend x y) = mappend (g x) (g y) forall (x, y) in lift{[]}(g). g (mconcat x) = mconcat y Again, mconcat is redundant. Even more curiously, though, map appears in the theorem, but lift{[]} appears in the class restriction. Cheers, Andrew Bromage

8 21

Re: [Haskell] ANNOUNCE: Lazy SmallCheck 0.1
by Janis Voigtlaender 19 Oct '07

19 Oct '07

That's pretty cool. If you are not yet aware of it, you might want to compare this with the EasyCheck library for Curry. They directly use functional logic programming for test generation, where you use exceptions for simulating logical variables. Here are some slides of a talk I heard recently: http://www.informatik.uni-kiel.de/~jac/data/DarkSecret.pdf (in German, unfortunately) Matthew Naylor wrote: > Announcing Lazy SmallCheck 0.1, a library for exhaustive, > demand-driven testing of Haskell programs. > > Lazy SmallCheck is based on the idea that if a property holds for a > partially-defined input then it must also hold for all fully-defined > instantiations of that input. Compared to `eager' input generation > in SmallCheck, Lazy SmallCheck may require significantly fewer > test-cases to verify a property for all inputs up to a given depth. > > There is a webpage for Lazy SmallCheck: > > http://www-users.cs.york.ac.uk/~mfn/lazysmallcheck/ > > There you'll find a more detailed description, a worked example, a > comparison with SmallCheck on a number of benchmarks, and link to > download the library. > > The library was developed together with Fredrik Lindblad during his > recent visits to York. > > Suggestions, experiences and bug reports are welcome! > > Matthew. > _______________________________________________ > Haskell mailing list > Haskell(a)haskell.org > http://www.haskell.org/mailman/listinfo/haskell > -- Dr. Janis Voigtlaender http://wwwtcs.inf.tu-dresden.de/~voigt/ mailto:voigt@tcs.inf.tu-dresden.de

1 0

data Bin = Zero | One
by PR Stanley 19 Oct '07

19 Oct '07

>Hi >data Bin = Zero | One As suggested by someone on this list. It's a really neat idea although I'm wondering how I can apply this to my int to binary function. The Zero or One declaration is saying that Bin is a data type that can hold either a one or a zero. I tried testing this with a very simple Bin -> Bin function and the Integral values 0 and 1 but ran into difficulties. Any ideas what I'm doing wrong here? Incidentally, does the general syntax above come from the old BNF notation? Cheers, Paul

2 1

Functional specification of DFS
by Vimal 18 Oct '07

18 Oct '07

Hello Haskellers, Yesterday, my professor had asked this question in a quiz: "Give a functional description of Depth First Search on a graph G. Use lisp." The first thing I wrote was: Let DFS(G, root) return the list of edges in the dfs spanning tree of G, rooted at root. Let n = |V| in: :) The naive algorithm of keeping a visited 'array' and recursive solution is what came to my mind. But, if we look at DFS as a mapping from G -> List of Spanning trees of G rooted at root, then we have an exponential (n**(n-2) ?) number of them, so, finding the one that satistifies the properties of a DFS spanning tree, might not be tractable. So, if we modify the specification of DFS(G, root) as DFS(G, root, intermediate_path), we get: DFS(G, root, path) = Union ( {(root, v)} U DFS(G, v, path U {root})) ) for all v not in path, and (root, v) exists in G. DFS is invoked as: DFS(G, root, {root}) The problem with this is that changes to "path" must be persistant across calls. i.e., {(root, v)} U DFS(G, v, {v, root} + recursive calls} U {(root, w)} U DFS(G, v, {v, root}, + nodes added in recursive calls}) etc. So, the question is: Is it possible to have a purely functional and tractable description of DFS? I did a Google on "Haskell DFS", and landed up with a paper [1], that also says that Graph Algorithms have been difficult to implement in a purely functional style. They use mutable arrays to achieve the same. I am getting a small idea using foldls and Monads to achieve this. Since, we have to take the return value of the previous instance of the function call, and then pass it on to the next. dfs initial_visited_list >>= \spanning_tree -> dfs (merge spanning_tree initial_visited) >>= \spanning_tree -> etc... I will try to write it down on paper and see if it works out. References: [1]: www.cse.ogi.edu/~jl/Papers/dfs.ps Do you have any thoughts on this? Thanks, -- ~Vimal RLE :) encode = map (length &&& head) . group decode = concatMap (uncurry replicate)

2 3

Tutorial: Curry-Howard Correspondence
by Tim Newsham 18 Oct '07

18 Oct '07

A tutorial on the Curry-Howard Correspondence in Haskell: http://www.thenewsh.com/%7Enewsham/formal/curryhoward/ Feedback appreciated. Tim Newsham http://www.thenewsh.com/~newsham/

14 27

Re: [Haskell-cafe] On the verge of ... giving up!
by Andrew Coppin 18 Oct '07

18 Oct '07

Steven Fodstad wrote: > > FWIW, other people feel about Haskell the way you feel about calculus > and the continuation monad, and your opinions of these other powerful, > but difficult, tools is what got you into this mess. On the contrary, other people's misinterpretation of my opinions on these matters is what got me into this mess. I could go into a lengthy explanation, but I'll probably just be misunderstood again. So let's leave it here. > academics don't like hearing that their life's work is useless. > Being positively surrounded by people who think Haskell is pointless, I certainly have I fair idea how that feels...

1 0

Bug in runInteractiveProcess?
by John Goerzen 18 Oct '07

18 Oct '07

Hi everyone, I have been trying to implement a Haskell-like version of shell pipelines using runInteractiveProcess. I am essentially using hGetContents to grab the output from one command, and passing that to (forkIO $ hPutStr) to write to the next. Slow, but this is just an experiment. This works OK to link together two external commands, but deadlocks when linking together three processes. After staring at straces all afternoon, I think I have found the culprit. I observed that when I have three commands linked together, the second never sees EOF on its input. This even though I saw an explicit close on the other end of the pipe from the Haskell side. Why is this, I wondered? I stared at the source for the C runInteractiveProcess function for a bit, but then the answer was right there: this function does not sanitize FDs. What that means is that the write end of the stdin pipe for command 2 was open in the Haskell process. The Haskell process then forked off for command 3 later on. This write end of the stdin pipe for command 2 was never closed in the command 3 child environment. Therefore, closing it in the Haskell thread did not cause command 2 to get an EOF. Does that make sense? Many systems will just try to close *all* FDs except the ones they need after a fork(). Another approach would be to maintain a global list of FDs that the Haskell thread is using, and close all of them except the pipe ends in the child. Without something like this, it is not possible to use runInteractiveProcess more than twice simultaneously in a single program. That renders it almost useless for some tasks. Does this make sense to everyone? If so, I'll submit the bug on GHC. -- John

7 18

Re: [Haskell-cafe] Tutorial: Curry-Howard Correspondence
by Dan Weston 17 Oct '07

17 Oct '07

_|_ does not provide a witness to a theorem in any consistent logic (otherwise everything could be proved from it), yet it inhabits every type in Haskell. If the only invalid type instance is _|_, then a necessary and sufficient test for the C-H correspondence be the existence of a type instance that halts. Non-strict constructors would seem to mess that up. From http://en.wikipedia.org/wiki/Curry%E2%80%93Howard#Types "The problem of finding a ?-expression with a particular type is called the type inhabitation problem. The answer turns out to be remarkable: There is a closed ?-expression with a particular type only if the type corresponds to a theorem of logic, when the ? symbols are re-interpreted as meaning logical implication." By inhabit, they clearly mean no occurrence (recursively) in the type instance of _|_. I think the extra wrinkle you are introducing with constructors like Prop to wrap types is justified only insofar as the boxed and unboxed types are isomorphic, but they are not unless the constructor is strict in all its arguments. Just as _|_ :: a does not qualify as justifying theorem a, so in isomorphism Prop _|_ :: Prop a should also not qualify. If all constructors were strict, Prop _|_ = _|_ and all is fine. I am posting this to the haskell-cafe list because I am not at all sure that my understanding is right, and I don't want you to change your tutorial if it's not. Dan Weston Tim Newsham wrote: >> Also, I was wondering if the constructor and/or function arguments >> should be marked strict. >> >> Otherwise, types can be inhabited by defined arguments. Since Prop is >> not strict in its argument, we could have the (false) theorem >> >> andAlwaysTrue :: forall p q . p :/\ q >> andAlwaysTrue p q = And (Prop undefined) (Prop undefined) >> >> This halts for all p and q since Prop and And are not strict. > > Hmm.. I'm wondering to what degree this would make a difference. > I'm not actually running any of these programs. I'm just compiling > them and relying on the type checker to validate the types (and > check the proofs). If I understand this correctly, adding "!" > wont affect the behavior of the type checking phase. > >> Dan Weston wrote: >>> That is a great tutorial. Thanks! But in the last two sentences of >>> the introduction you say: >>> >>> > We just need to find any program with the given type. >>> > The existence of a program for the type will be a proof >>> > of the corresponding proposition! >>> >>> Maybe you should make explicit that >>> >>> 1) the type is inhabited >>> >>> undefined :: forall p . p >>> >>> does not prove that all propositions are true >>> >>> 2) the function must halt for all defined arguments >>> >>> fix :: forall p . (p -> p) -> p >>> fix f = let x = f x in x >>> >>> does not prove the (false) theorem >>> >>> (p => p) => p >>> >>> even though (fix id) is well-typed and id is certainly not undefined >>> (though fix id is). >>> >>> Tim Newsham wrote: >>>> A tutorial on the Curry-Howard Correspondence in Haskell: >>>> http://www.thenewsh.com/%7Enewsham/formal/curryhoward/ >>>> >>>> Feedback appreciated. >>>> >>>> Tim Newsham >>>> http://www.thenewsh.com/~newsham/ >>>> _______________________________________________ >>>> Haskell-Cafe mailing list >>>> Haskell-Cafe(a)haskell.org >>>> http://www.haskell.org/mailman/listinfo/haskell-cafe >>>> >>>> >>> >>> >> >> > > Tim Newsham > http://www.thenewsh.com/~newsham/ > >

2 1

ANNOUNCE: xmonad 0.4
by Don Stewart 17 Oct '07

17 Oct '07

The xmonad dev team is pleased to announce the 0.4 release of xmonad! http://xmonad.org xmonad is a tiling window manager for X. Windows are arranged automatically to tile the screen without gaps or overlap, maximising screen use. Window manager features are accessible from the keyboard: a mouse is optional. xmonad is written, configured and extensible in Haskell. Custom layout algorithms, key bindings and other extensions may be written by the user in Haskell, in config files. Window layouts are applied dynamically, and different layouts may be used on each workspace. Xinerama is fully supported, allowing windows to be tiled across several physical screens. Features: * Simple, intuitive user interface * Stable, fast and small memory footprint * Automatic window tiling and management * First class keyboard support: a mouse is unnecessary * Full support for tiling windows on multi-head displays * Full support for floating windows * XRandR support to rotate, add or remove monitors dynamically * Per-workspace layout algorithms * Per-screens custom status bars * Easy, powerful customisation and reconfiguration * Large extension library * Extensive documentation and support for hacking This is a big release, with every feature we originally proposed for xmonad implemented. Since xmonad 0.3, the following notable improvments have appeared: * Powerful "rules" system: config files may specify rules about how particular applications are handled. For example, gimp might always be placed in the floating layer, or firefox always placed on workspace 2. Gnome dock apps (such as kicker or gnome-panel) might always be placed in a status bar gap and unmanaged. * User-specified workspace tag types (not restricted to numeric keys). E.g. "web" or "www" are valid workspace tags now. * Layouts algorithms serialisable. Current workspace state preserved across restarts/reconfiguration, including user-written modules' state * User written code sandboxed from the core applicuation further, making it safer to experiment with new extensions * 100% code coverage of logic core of xmonad by its testsuite, thanks to QuickCheck and HPC. * More hooks to make writing expressive extensions easier * mod-m to shift focus to the `master' window * many new binary distributions, for various flavours of Linux and BSD, OSX is also well supported. * extensions: xmonad comes with a huge library of extensions (3 times the size of xmonad itself), contributed by viewers like you. Extensions enable pretty much arbitrary window manager behaviour to be implemented by users, in Haskell, in the config files. For more information on using and writing extensions, see the webpage. Get it! More information, screenshots, documentation, tutorials and community resources are available from the xmonad home page: http://xmonad.org The 0.4 release, and its dependencies, are available from hackage.haskell.org, here: http://hackage.haskell.org/cgi-bin/hackage-scripts/package/xmonad Brought to you by the xmonad team: Spencer Janssen Don Stewart Jason Creighton Andrea Rossato David Roundy with code contributions from: Brandon Allbery Chris Mears Shachaf Ben-Kiki Eric Mertens Alec Berryman Neil Mitchell Gwern Branwen Devin Mullins Joachim Breitner Daniel Neri Alexandre Buisse Stefan O'Rear Nick Burlett Simon Peyton Jones Peter De Wachter Hans Philipp Annen Aaron Denney Karsten Schoelzel Nelson Elhage Michael Sloan Shae Erisson Ivan Tarasov Joachim Fasting Alex Tarkovsky Michael Fellinger Christian Thiemann David Glasser Joe Thornber Kai Grossjohann Matsuyama Tomohiro Dave Harrison Daniel Wagner Juraj Hercek Ferenc Wagner Sam Hughes Jamie Webb Miikka Koskinen Brent Yorgey David Lazar nornagon Lucas Mai timthelion Robert Marlow Klaus Weidner As well as the support of a cast of hundreds on the #xmonad and #haskell IRC channels, and the wider Haskell, FP and window manager communities. Thanks to everyone for their support!

2 2

Stack overflow in ghci
by Maurício 17 Oct '07

17 Oct '07

Hi, I get this error message when testing a function in ghci: *** Exception: stack overflow I admit I didn't care about efficiency when I wrote that function, but I'm almost sure it is not supposed to eat all my memory. Do I need to say something to ghci if I want it to use all available memory? Thanks, Maurício

3 2