- Haskell-Cafe - Haskell.org

Proof in Haskell
by pat browne 25 Sep '09

25 Sep '09

Hi, Below is a function that returns a mirror of a tree, originally from: http://www.nijoruj.org/~as/2009/04/20/A-little-fun.html where it was used to demonstrate the use of Haskabelle(1) which converts Haskell programs to the Isabelle theorem prover. Isabelle was used to show that the Haskell implementation of mirror is a model for the axiom: mirror (mirror x) = x My question is this: Is there any way to achieve such a proof in Haskell itself? GHC appears to reject equations such has mirror (mirror x) = x mirror (mirror(Node x y z)) = Node x y z Regards, Pat =================CODE===================== module BTree where data Tree a = Tip | Node (Tree a) a (Tree a) mirror :: Tree a -> Tree a mirror (Node x y z) = Node (mirror z) y (mirror x) mirror Tip = Tip (1)Thanks to John Ramsdell for the link to Haskabelle: http://www.cl.cam.ac.uk/research/hvg/Isabelle/haskabelle.html)

3 2

ANN: epoll bindings 0.2
by Toralf Wittner 25 Sep '09

25 Sep '09

Hi, I am pleased to announce the release of epoll bindings 0.2 available from: http://hackage.haskell.org/package/epoll Epoll is an I/O event notification facility for Linux similar to poll but with good scaling characteristics. This release adds a buffer abstraction on top of the existing low-level bindings, so client code can write and read to buffers without having to deal directly with the underlying epoll event handling. -Toralf

1 0

How does one delare a 2D STUArray in Haskell?
by Casey Hawthorne 25 Sep '09

25 Sep '09

How does one delare a 2D STUArray in Haskell? I see the following from a diffusion program segment: module Diffusion where import Data.Array import Data.List (sortBy) type VFieldElem = Float type VField = Array (Int,Int) VFieldElem <snip> zeros = listArray ((1,1),(imax,jmax)) (repeat 0) From Real World Haskell to declare a 1D array (I changed some of the value names) there is the following: import Data.Array.ST (STUArray) import Data.Array.Unboxed (UArray) import Data.Word (Word32) data PlayingField1D a = PF1D { pf1DState :: (a -> [Word32]) , pf1DArray :: UArray Word32 Bool } data MutPlayingField1D s a = MPF1D { mpf1DState :: (a -> [Word32]) , mutpf1DArray :: STUArray s Word32 Bool } But I cannot see how to declare a 2D array. Although, it is not "strictly" necessary, pun intended, since one can reframe the 1D array as 2D array by using row/column mapping functions. -- Regards, Casey

4 6

Haddock and literate Haskell: annotations must be marked as source?
by Andy Gimblett 25 Sep '09

25 Sep '09

Hi all, I've developed a bit of a taste for literate Haskell lately, being a verbose sort of guy. Unfortunately, it doesn't seem to interact with Haddock in the way I'd like/expect. I just wanted to check that my understanding of the situation is correct before I (regretfully) give up on LHS. It seems to me that Haddock only picks up annotation comments (ie those that should be included in the produced documentation) from literate Haskell source when those annotations are themselves marked up as source - it seems not to recognise them in the general text. For example, I was expecting/hoping that from the point of view of Haddock, the following literate Haskell code with an annotation-marked paragraph (starts with a vertical bar) in the non-source text. | Turn a foo into a bar. > foo :: Foo -> Bar > foo b = ... ought to be equivalent to the following "illiterate" Haskell: -- | Turn a foo into a bar. foo :: Foo -> Bar foo b = ... ie, it should produce Haddock docs where the definition of foo is annotated with that comment. Sadly, that appears not to be the case. It appears the literate version needs to look like this: > -- | Turn a foo into a bar > foo :: Foo -> Bar > foo b = ... which to my mind rather defeats the purpose of being literate. So: am I right that this is the intended/expected behaviour? If not, how does one get round it? If so, could someone perhaps comment on the prospects/complexity of implementing this - or the reasons why it is in fact a bad idea? Many thanks! -Andy

3 6

Monad Tutorial in C++
by AdrianMay 25 Sep '09

25 Sep '09

Just wrote yet another of the above if anybody wants one: http://nuerd.blogspot.com/2009/09/monad-tutorial-in-c.html Adrian. -- View this message in context: http://www.nabble.com/Monad-Tutorial-in-C%2B%2B-tp25606090p25606090.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.

1 1

Referring to Prelude.(++)
by Terry Hayes 25 Sep '09

25 Sep '09

I'd like to redefine (++) so that it works on a more general class of "lists" (ListOf a). To do this, I found that I can import the Prelude hiding the definition of (++). Then I want to make [] an instance of ListOf, and have the (++) function call the built-in Prelude.(++). My problem is that I can't figure out how to call the built-in function. Just using "Prelude.(++)" doesn't seem to work in the way that "Prelude.foldl" would (for example). Any ideas? Terry

2 2

ANN: diagrams 0.2.1, and planned major improvements
by Brent Yorgey 24 Sep '09

24 Sep '09

Hi all, I'm pleased to announce version 0.2.1 of the diagrams library, available now on Hackage [1]. This is a minor release which fixes a few bugs and adds a few new combinators, most notably a grid layout combinator contributed by Ganesh Sittampalam. For a full list of the features new to 0.2.1, see the CHANGES file [2]. The real reason for the release is to get existing new features out the door before gearing up for a planned major rewrite of the backend to use a constraint-solving layout engine. This will allow for much greater elegance and flexibility, as well as a number of features (such as arrows connecting different parts of the diagram) which would be difficult or impossible to implement in the current framework. My ultimate vision is for the diagrams library to become a viable alternative to declarative drawing systems such as MetaPost [3] and Asymptote [4], with the distinct advantages that it will be (1) *purely* declarative, and (2) an *embedded* DSL, providing the full power of Haskell and its ecosystem, as opposed to the ad-hoc specialized languages used by MetaPost and Asymptote. If this sounds exciting to you, I hope you'll join me, either by trying out diagrams for your projects and providing feedback, or by contributing some code. If you're interested in helping with the rewrite itself, let me know; I also plan to set up a core/contrib model like that of xmonad, so there should also be plenty of opportunities for contributing independent add-on modules which enhance the core functionality. -Brent [1] http://hackage.haskell.org/package/diagrams [2] http://code.haskell.org/diagrams/CHANGES [3] http://www.tug.org/metapost.html [4] http://asymptote.sourceforge.net/

2 1

source locations (was: best practices for monad transformers and exceptions?)
by Evan Laforge 24 Sep '09

24 Sep '09

I forgot to mention this, but control-monad-exception reminded me: Is there any interest in a way for ghc to report source locations? I have a preprocessor that basically works and is really useful but also awkward and not scalable. control-monad-exception has TH which is more scalable but requires manual annotation at every call site. The loch package also requires annotation at call sites. I searched on trac, but it's hard to know what to search for and I only found a feature request to make 'undefined' report line numbers. Some way to have the callee get the caller's location would be quite handy. Perhaps something like: -- | (calling_function, calling_filename, line_number) type SrcPos = Maybe (String, String, Int) {-# SRCPOS_ANNOTATE foo, foo_srcpos #-} foo :: Arg -> Result foo = foo_srcpos Nothing foo_srcpos :: SrcPos -> Arg -> Result foo_srcpos srcpos arg = do State.modify $ \st -> st { state_stack = srcpos : state_stack st } -- or whatever Then ghc will rewrite calls to 'foo' as calls to 'foo_srcpos' and add a SrcPos arg. If the extension isn't present, plain 'foo' will be called which will pass Nothing. This is basically what my preprocessor does, only it doesn't understand modules and importing, so it relies on me having a consistent import convention. I suppose the preprocessor could be extended with the ability to understand import lines... but ghc could put the annotation in .hi and wouldn't have to scan all the source files. My preprocessor wouldn't work with libraries. Getting a complete call stack would be even nicer, and I remember seeing something a while ago about how it would require keeping track of the calls separately from the real (possibly heavily inlined or tail recursive) call stack but would be technically possible especially with some more detailed source code information which I suppose may be in by now...

1 1

Parallel graphics
by Andrew Coppin 24 Sep '09

24 Sep '09

I have a number of compute-bound graphics programs written in Haskell. (Fractal generators, ray tracers, that kind of thing.) GHC offers several concurrency and parallelism abstractions, but what's the best way to use these to get images rendered as fast as possible, using the available compute power? (OK, well the *best* way is to use the GPU. But AFAIK that's still a theoretical research project, so we'll leave that for now.) I've identified a couple of common cases. You have a 2D grid of points, and you want to compute the value at each point. Eventually you will have a grid of /pixels/ where each value is a /colour/, but there may be intermediate steps before that. So, what cases exist? 1. A point's value is a function of its coordinates. 2. A point's value is a function of its previous value from the last frame. 3. A point's value is a function of /several/ points from the last frame. How can we accelerate this? I see a few options: - Create a spark for every point in the grid. - Create several explicit threads to populate non-overlapping regions of the grid. - Use parallel arrays. (Does this actually works yet??) I'm presuming that sparking every individual point is going to create billions of absolutely tiny sparks, which probably won't give great performance. We could spark every line rather than every point? Using explicit threads has the nice side-effect that we can produce progress information. Few things are more frustrating than staring at a blank screen with no idea how long it's going to take. I'm thinking this method might also allow you to avoid two cores tripping over each other's caches. And then there's parallel arrays, which presumably are designed from the ground up for exactly this type of task. But are they usable yet? Any further options?

9 8

Re: [Haskell-cafe] best practices for monad transformers and exceptions?
by Evan Laforge 24 Sep '09

24 Sep '09

On Thu, Sep 24, 2009 at 8:11 AM, pepe <pepeiborra(a)gmail.com> wrote: > Exceptions in the ErrorT monad are not compositional. > It's the first time I see the approach of stacking > several ErrorT monads. It seems slightly better than > having a 'global' exception type, although the explicit > lifting looks quite painful. > > I really don't know whether there is a way to write > catch_abort, sorry! Even if there is, I don't think you > want to use it. A much better option is to use an extensible > exception type. Yeah, I had forgotten about Tyeable implementations, which is silly since that's how the IO exceptions now work. Your extensible error framework looks pretty nice! I just made the exceptions global (i.e. put them all in the lowest level type) since I only have two at this point, but if I had more I would definitely check out Control.Monad.Exception. Ideally I would like to be able to package up a set of "services" as a transformer and plug it in compositionally without worrying about its implementation, but it seems monad transformers are only part of the way there. You can get some hiding with a newtype, and then you can get unlifted access with classes as mtl does (but then you need a bunch of instance boilerplate), but then if the one of the services the transformer needs is "early return", then you have to pull the ErrorT out and put it into the "final" monad, and handle all the exceptions in the final monad's "run". It would be nice someday to have more satisfactory way of combining effects. I dream of a way to effortlessly create encapsulated transformers that easily compose with other transformers...

1 0