News aggregator

[ANN] codex

haskell-cafe - Sat, 08/30/2014 - 4:23pm
Hi Cafe, I just wanted to let you know that I have just released a new version of `codex` on hackage. There is *no new features* in this version, but thanks for the help from Hubert Behaghel I was able to investigate issues with MacOS. So basically this version now work with MacOS, if you had give a try before please delete your "~/.codex" configuration file before installing the new version. Cheers
Categories: Offsite Discussion

Is there a neat & efficient function for modifying an element at a specific index in a data structure?

Haskell on Reddit - Sat, 08/30/2014 - 4:06pm

For example, say I have an array of 1000 an integers and I want an Index -> Array -> Array function which adds 1 to the element at the given index, returning a new array in which this change has been made. I see how the function could by implemented using some counter value which descends from the input value and applies the (+1) function to the current element when the counter hits 0. Could it be done with a fold? Or a monadic bind function? I'm fairly new to Haskell so any relevant comments or links would be extremely helpful.

submitted by Rogerthesiamesefish
[link] [18 comments]
Categories: Incoming News

IO Monad and Purity

Haskell on Reddit - Sat, 08/30/2014 - 3:16pm
Categories: Incoming News

Introducing /r/haskellgamedev

Haskell on Reddit - Sat, 08/30/2014 - 1:06pm

Based on discussion here, it seems that there's a need for a public and easily-found venue for discussion of game development in Haskell. Well, here you go: /r/haskellgamedev

I'm a total newbie myself and so expect myself to be a fairly useless founder. Anyone interested in moderator status is encouraged to ask. On a related note, I have activated the subreddit wiki and right now access is virtually unrestricted (accounts must be 1 day old). Let's get some info in there!

submitted by tejon
[link] [20 comments]
Categories: Incoming News

Philip Wadler: Howard on Curry-Howard

Planet Haskell - Sat, 08/30/2014 - 12:04pm

When writing Propositions as Types, I realised I was unclear on parts of the history. Below is a letter I wrote to William Howard and his response (with corrections he provided after I asked to publish it). I believe it is a useful historical document, and am grateful to Howard for his permission to publish.

Update. References to Figures 5 and 6 in the following are to Propositions as Types. Thanks to Ezra Cooper for pointing out this was unclear.

Here is my original request.
Subject: The Formulae-as-Types Notion of Construction
Dear Prof Howard,
My research has been greatly influenced by your own, particularly the paper cited in my subject. I am now writing a paper on the field of work that grew out of that paper, which was solicited for publications by the Communications of the ACM (the flagship of the professional organisation for computer scientists). A draft of the paper is attached.
I would like to portray the history of the subject accurately. I have read your interview with Shell-Gallasch, but a few questions remain, which I hope you will be kind enough to answer.
Your paper breaks into two halves. The first describes the correspondence between propositional logic and simple types, the second introduces the correspondence between predicate logic and dependent types. Did you consider the first half to be new material or merely a reprise of what was known? To what extent do you consider your work draws on or was anticipated by the work of Heyting and Kolmogorov, and Kleene's realisability? To what extent did your work influence the subsequent work of de Bruijn and Martin Lof? What was the history of your mimeograph on the subject, and why was it not published until the Curry Festschrift in 1980?
Many thanks for your consideration, not to mention for founding my field! Yours, -- P

And here is his response: 
Dear Prof. Wadler,
As mentioned in the interview with Shell-Gellasch, my work on propositions as types (p-a-t) originated from my correspondence with Kreisel, who was very interested in getting a mathematical notion (i.e., in ordinary mathematics) for Brouwer's idea of a construction (as explained by Heyting). I was not familiar with the work of Brouwer or Heyting, let alone Kolmogorov, but, from what Kreisel had to say, the idea was clear enough: a construction of  alpha - > beta was to be a construction F which, acting on a construction A of alpha, gives a construction B of beta. So we have constructions acting on constructions, rather like functionals acting on functionals. So, as an approximation,
(1)   let's take "construction" to mean "functional".
But what kind of functionals? In constructive mathematics, a functional is not given as a set of ordered pairs. Rather,
(2)   to give a functional is to give not only the action or process it performs but also to give its type (domain and counterdomain).
Clearly, the type structure is going to be complicated. I set myself the project of finding a suitable notation for the type symbols. So one needs a suitable type symbol for the functional F, above. Well, just take it to be alpha itself (at this point, I was thinking of propositional logic). Suddenly I remembered something that Curry had talked about in the logic seminar during my time at Penn State. If we consider typed combinators, and look at the structure of the type symbols of the basic combinators (e.g., S, K, I), we see that each of the type symbols corresponds to (is isomorphic to) one of the axioms of pure implicative logic. Well! This was just what I needed!
How do we formulate the following notion?
(3)   F is a construction of phi.
Consider the case in which phi has the form alpha - > beta. The temptation is to define "F is a construction of alpha - > beta" to mean "for all A: if A is a construction of alpha, then FA is a construction of beta". Well, that is circular, because we have used if ... then ... to define implication. This is what you call "Zeno’s paradox of logic". I avoided this circularity by taking (3) to mean:
(4)   F is assigned the type phi according to the way F is built up; i.e., the way in which F is constructed.
Thus F is a construction of phi {\em by construction}. Your figure 6 illustrates precisely what I meant by this. (I did not have that beautiful notation at the time but it conveys what I meant.)
To summarize: My basic insight consisted simultaneously of the thoughts (2) and (4) plus the thought that Curry's observation provided the means to implement (2), (4). Let me say this in a different way. The thought (2) was not new. I had had the thought (2) for many years, ever since I had begun to study primitive recursive functionals of finite type. What was new was the thought (4) plus the recognition that Curry's idea provided the way to implement (4). I got this basic insight in the summer of 1966. Once I saw how to do it with combinators, I wondered what it would look like from the vewpoint of the lambda calculus, and saw, to my delight, that this corresponded to the intuitionistic version of Gentzen's sequent calculus.
Incidentally, Curry's observation concerning the types of the basic combinators is presented in his book with Feys (Curry-Feys), but I was unaware of this, though I had owned a copy for several years (since 1959, when I was hired at Penn State). After working out the details of p-a-t over a period of several months, I began to think about writing it up, so I thought I had better see if it is in the book. Well, it is easy enough to find if you know what you are looking for. On looking at it, I got a shock: not only had they extended the ideas to Gentzen's sequent calculus, but they had the connection between elimination of cuts from a derivation and normalization of the corresponding lambda term. But, on a closer look, I concluded that they had {\em a} connection but not {\em the} connection. It turns out that I was not quite right about that either. See my remark about their Theorem 5, below. Not that it would have mattered much for anything I might have published: even if they had the connection between Gentzen's sequent calculus and the lambda calculus, I had a far-reaching generalization (i.e., to Heyting arithmetic).
The above is more detailed than would be required to answer your questions, but I needed to write this out to clarify my thoughts about the matter; so I may as well include the above, since I think it will interest you. It answers one of your questions, "To what extent do you consider your work draws on or was anticipated by the work of Heyting and Kolmogorov, and Kleene's realisability?" Namely, my work draws on the work of Heyting and Brouwer, via Kreisel's explanation of that work to me. None of it was anticipated by the work of Heyting, Kolmogorov or Kleene: they were not thinking of functionals of finite type. Though I was familiar with Kleene's recursive realizability, I was not thinking about it at the time. Admittedly, it touches on ideas about Brouwer's constructions but is far from capturing the notion of a construction (actually, Kleene once made remarks to this effect, I forget where). Because of the relation between constructions and Kleene's recursive realizability, there could have been some unconscious influence; but, in any case, not a significant influence.
"did your work influence the subsequent work of de Bruijn and Martin Lof? " As far as I know, my work had no influence on the work of de Bruijn. His work appears to be completely independent of mine. I do recall that he once sent me a package of Automath material. The project of a computer program for checking existing proofs did not appear very interesting and I did not reply. What I would have been interested in is a program for finding proofs of results that had not yet been proved! Even a proof-assistant would have been fine. Why did he send me the Automath material? I don't recall what year it was. Sometime in the 1970s. Whatever the accompanying letter, it was not informative; merely something like: "Dear Professor Howard, you may be interested in the following material ...". Since that time, I have seen two or three articles by him, and I have a more favorable impression. It is good, solid work. Obviously original. He discovered the idea of derivations as terms, and the accompanying idea of formulae-as-types, on his own. He uses lambda terms but, I think, only for purposes of description. In other words, I don't think that he has the connection between normalization and cut-elimination, but I have not made an extensive examination of his work. In fact, does he use a Gentzen system at all? I just don't know. The latter two questions would easily be answered by anyone familiar with his work. In any case, give him credit where credit is due. There are enough goodies for everyone!
My influence on Martin-Löf? No problem there. I met him at the Buffalo 1968 conference and I told him my ideas. His instant reaction was: "Now, why didn't I think of that?" He had a visiting appointment at UIC for the academic year 1968-1969, so we had lot's of opportunity to talk, and he started developing his own approach to the ideas. In Jan. 1969, mainly to make sure that we were both clear on who had discovered what, I wrote up my own ideas in the form of handwritten notes. By then, Xerox machines were prevalent, so I sent a copy to Kreisel, and he gave copies to various people, including Girard. At least, I think that is how Girard got a copy, or maybe Martin-Löf gave him one. I like Martin-Löf's work. I could say more about this, but the short answer to your question is: Martin-Löf's work originated from mine. He has always given me credit and we are good friends.
On further thought, I need to mention that, in that first conversation, Martin-Löf suggested that the derivations-as-terms idea would work particularly well in connection with Prawitz's theory of natural deduction. I thought: okay, but no big deal. Actually, at that time, I was not familiar with Prawitz's results (or, if at all, then only vaguely). But it was a bigger deal than I had thought, because Prawitz's reductions steps for a deduction correspond direcly to reduction steps for the associated lambda term! Actually, for most purposes, I like the sequent formulation of natural deduction as given in pages 33 and 88 of Sorensen and Urzyczyn (2006). In fact, if we add left-implication-introduction to this (let's confine ourselves to pure implicative logic), the resulting system P# is pretty interesting. All occurrences of modus ponens can be eliminated, not just those which are preceded by left-implication-introduction. This is what I am up to in my JSL 1980 paper, "Ordinal analysis of terms of finite type." Also, the cut rule is easy to derive in P# (just consider, for typed lambda terms: a well-formed term substituted into a well-formed term results in a well-formed term); hence P# is is a conservative extension of the system P* in Part I of my little paper in the Curry Festschrift.
The phrase formulae-as-types was coined by Kreisel in order that we would have a name for the subject matter in our correspondence back and forth. I would assume that the phrase "propositions as types" was coined by Martin-Löf; at least, during our first conversation at the Buffalo 1968 meeting, he suggested that one could think of a type as a proposition, according to the idea that, in intuitionistic mathematics, the meaning of a proposition phi is given by the species of "all" proofs of phi. I use quotes here because we are not talking about a set-theoretic, completed infinity.
"the second [part] intrudes the correspondence between predicate logic and dependent types." I was not thinking about it in that way at all. I wanted to provided an interpretation of the notion of construction to some nontrivial part of intuitionistic mathematics (Heyting arithmetic). Part I of the paper was just the preliminaries for this. Actually, what you say in the pdf is consistent with this. No need for change here.
"Did you consider the first half to be new material or merely a reprise of what was known?" New. But in January of last year I had occasion to take a really hard look at the material in Curry-Feys, pp. 313-314; and I now see that there is a much closer relationship between my Theorem 2 in Part I and their Theorem 5, page 326, than I had thought. The issues here are quite interesting. I can provide a discussion if you want.
In the introduction to my little paper, I mention that Tait had influenced me. Let me say a few words about that. In the summer of 1963 we had conversations in which he explained to me that he had developed a theory of infinite terms in analogy to Schütte's theory of infinite proofs, where normalization (via lambda reductions) of an infinite terms corresponds to cut elimination of the corresponding proof. He did not know what to make of it. He thought of his theory of infinite terms as a sort of pun on Schütte's theory of infinite proofs. But we both agreed that  there must be a deep connection between normalization of lambda terms and Gentzen's cut elimination. We puzzled over this during two or three of our conversations but could not come up with an answer.
As explained in the first paragraph of this e-mail, my work originated with a problem posed by Kreisel; so, at the start of this work, certainly I was not thinking of those conversations with Tait. But, as mentioned above, as soon as I got the basic insight about the relevance of Curry's combinators, I considered how it would work for lambda terms. At that point, I remembered my conversations with Tait. In other words, when I verified that
(5)   cut elimination for a derivation corresponds to normalization for the term,
the conversations with Tait were very much on my mind. Most likely I would have noticed (5) without having had the conversations with Tait. But who knows? In any case, he deserves credit for having noticed the correspondence between derivations and terms. What he did not have was the associated correspondence between propositions and types. In fact, he was not using a general enough notion of type for this. By hindsight we can see that in his system there is a homomorphism, not an isomorphism, from propositions to types.
I need to say a bit more about Tait and types. Since Schütte had extended his system of proofs to transfinite orders, Tait extended his system of terms to transfinite type levels. I already had my own system of primitive recursive functionals of transfinite type. In our very first conversation, we compared out ideas on this topic. This topic requires that one think very hard about the notion of type. Certainly, I had already thought extensively about the notion of type (because of (2), above) before I ever met Tait, but my conversations with him reinforced this tendency. Thoughts about types were very much on my mind when I began to consider (1), (2), above.
As already mentioned, the notes were handwritten and xeroxed; no mimeographs. "why [were they] not published until the Curry Festschrift in 1980?" First let me mention why they got published in the Curry Festschrift. Selden was bringing out the Festschrift for Curry's 80th birthday. He asked me to contribute the notes. I said: "Sure. I'll write up an improved version. I can now do much better." He replied: "No, I want the original notes. It is a historical document." In other words, by that time various copies had been passed around and there were a number of references to them in the literature. So I had them typed up and I sent them in.
Why didn't I publish them before that? Simply because they did not solve the original problem. That was Kreisel's and Gödel’s verdict (Kreisel had shown or described the work to Gödel). In fact, even before communicating the work to Kreisel, I knew that I had gotten only an approximation to the notion of construction, and that more work had to be done. Essentially, the criticism is as follows. In my little paper, I do not provide axioms and rules of inference for proving statements of the form
(3)   F is a construction of phi.
Remember, we have to avoid "Zeno’s paradox of logic"! The answer is that the proofs will look like what you have in Figure 6. In other words, Figure 6 is not only a program; it is also a proof (or: it can be reinterpreted as a proof). But Figure 6 can also be interpreted as an explanation of how a construction (blue) is to be built up in order to have a given type (red). In other words, figures such as Figure 6 implements the idea (4) mentioned near the beginning of this e-mail; i.e., F is assigned the type phi according to the way F is built up.
I hope this tickles you; it certainly tickles me. Of course, the rules of inference are as in Figure 5. So these simple ideas provide the missing theory of constructions; or, at the very least, provide a significant step in that direction.
In Jan. 2013, I exchanged a few e-mails with Tait and Constable on the history of p-a-t. This caused me to take a really careful look at the Curry-Feys book. Here is something I found that really made me laugh: the required theory, whose inferences are of the form given in Figure 5 is already in Curry-Feys. Admittedly, to see this you first have to erase all the turnstyles ( |-- ); Curry seems to have some kind of obsession with them. In particular, erase the turnstiles from the proof tree on page 281. The result is exactly a proof tree of the general form given in your Figure 6. (Hint: (...)X is to be read "X has type (...)". In other words, rewrite (...)X as X : (...).) What does Fbc mean, where F is boldface? Just rewrite Fbc as b -> c. You see? I am an expert. I could probably make money writing a translation manual. In summary, the required theory is essentially just Curry's theory of functionality (more precisely, the appropriate variant of Curry's theory). So, did I miss the boat here? Might I have seen all this in 1969 if only I had had the determination to take a hard look at Curry-Feys? I don't know. It may require the clarity of mind represented by the notation of Figure 5. Do you have any idea when and where this notation came into use?
One more remark concerning my reason for not publishing. Didn't I feel that I had made an important breakthrough, in spite of Kreisel's and Gödel’s criticisms? On the one hand, yes. On the other hand, I had reservations. Except for Martin-Löf, Prawitz, Tait and Girard, very few people showed an interest in the ideas. But maybe Martin-Löf, Prawitz, Tait and Girard should have been enough. You say: "Certainly Howard was proud of the connection he drew, citing it as one of the two great achievements of his career [43]." Should we let that passage stand? Sure. The interview occurred in the spring of 2000. By that time, I was getting lots of praise from the computer science community. So, pride is a peculiar thing. Let me end this on a positive note. In 1969 Prawitz was in the US and came to UIC to give a talk. When he entered the room, he made a beeline for me, looked me in the eye and shook my hand. The message was: Well done! THAT made me proud.
There is more to say; but this answers your questions, I think; so I'll send it to avoid further delay. 
Your pdf, Propositions as Types, is very readable.

Categories: Offsite Blogs

ICFP pre-party

haskell-cafe - Sat, 08/30/2014 - 11:24am
We're having a small unofficial ICFP pre-party today in Gothenburg. All haskell-cafe readers that happen to be in Gothenburg are welcome :-) The plan is to meet at The Bishop's Arms (Kungsportsavenyen 36) at 19.00. NOTE: there are three Bishop's Arms in Gothenburg, so mind the address. Feel free to text me at +380662285780. Roman _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe< at >
Categories: Offsite Discussion

Howard on Curry-Howard

Lambda the Ultimate - Sat, 08/30/2014 - 10:07am

Philip Wadler posts his exchange with William Howard on history of the Curry-Howard correspondence. Howard on Curry-Howard.

Categories: Offsite Discussion

Joachim Breitner: DebConf 14

Planet Haskell - Sat, 08/30/2014 - 9:10am

I’m writing this blog post on the plane from Portland towards Europe (which I now can!), using the remaining battery live after having watched one of the DebConf talks that I missed. (It was the systemd talk, which was good and interesting, but maybe I should have watched one of the power management talks, as my battery is running down faster than it should be, I believe.)

I mostly enjoyed this year’s DebConf. I must admit that I did not come very prepared: I had neither something urgent to hack on, nor important things to discuss with the other attendees, so in a way I had a slow start. I also felt a bit out of touch with the project, both personally and technically: In previous DebConfs, I had more interest in many different corners of the project, and also came with more naive enthusiasm. After more than 10 years in the project, I see a few things more realistic and also more relaxed, and don’t react on “Wouldn’t it be cool to have <emph>crazy idea</emph>” very easily any more. And then I mostly focus on Haskell packaging (and related tooling, which sometimes is also relevant and useful to others) these days, which is not very interesting to most others.

But in the end I did get to do some useful hacking, heard a few interesting talks and even got a bit excited: I created a new tool to schedule binNMUs for Haskell packages which is quite generic (configured by just a regular expression), so that it can and will be used by the OCaml team as well, and who knows who else will start using hash-based virtual ABI packages in the future... It runs via a cron job on to produce output for Haskell and for OCaml, based on data pulled via HTTP. If you are a Debian developer and want up-to-date results, log into and run ~nomeata/binNMUs --sql; it then uses the projectb and wanna-build databases directly. Thanks to the ftp team for opening up, by the way!

Unsurprisingly, I also held a talk on Haskell and Debian (slides available). I talked a bit too long and we had too little time for discussion, but in any case not all discussion would have fitted in 45 minutes. The question of which packages from Hackage should be added to Debian and which not is still undecided (which means we carry on packaging what we happen to want in Debian for whatever reason). I guess the better our tooling gets (see the next section), the more easily we can support more and more packages.

I am quite excited by and supportive of Enrico’s agenda to remove boilerplate data from the debian/ directories and relying on autodebianization tools. We have such a tool for Haskell package, cabal-debian, but it is unofficial, i.e. neither created by us nor fully endorsed. I want to change that, so I got in touch with the upstream maintainer and we want to get it into shape for producing perfect Debian packages, if the upstream provided meta data is perfect. I’d like to see the Debian Haskell Group to follows Enrico’s plan to its extreme conclusion, and this way drive innovation in Debian in general. We’ll see how that goes.

Besides all the technical program I enjoyed the obligatory games of Mao and Werewolves. I also got to dance! On Saturday night, I found a small but welcoming Swing-In-The-Park event where I could dance a few steps of Lindy Hop. And on Tuesday night, Vagrant Cascadian took us (well, three of us) to a blues dancing night, which I greatly enjoyed: The style was so improvisation-friendly that despite having missed the introduction and never having danced Blues before I could jump right in. And in contrast to social dances in Germany, where it is often announced that the girls are also invited to ask the boys, but then it is still mostly the boys who have to ask, here I took only half a minute of standing at the side until I got asked to dance. In retrospect I should have skipped the HP reception and went there directly...

I’m not heading home at the moment, but will travel directly to Göteborg to attend ICFP 2014. I hope the (usually worse) west-to-east jet lag will not prevent me from enjoying that as much as I could.

Categories: Offsite Blogs

Using 'lens' for "over"-like computation in Monad

haskell-cafe - Sat, 08/30/2014 - 8:44am
Hello Cafe, I'm trying to wrap my head around 'lens' library. My current exercise is to modify something using Lens in monad. Say, ("Hello", "World") & _1 `myOp` (\a -> putStrLn a >> return a) in IO, where myOp would be of type: myOp :: Monad m => Lens s t a b -> (a -> m b) -> s -> m t Of course I can write it myself, using combination of "view" and "set": myOp lens f v = f (view lens v) >>= flip (set lens) v (have not checked this, but something like that should do), but is there a more elegant way? Nikolay. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe< at >
Categories: Offsite Discussion


Haskell on Reddit - Sat, 08/30/2014 - 6:32am
Categories: Incoming News

Philip Wadler: Independent information on independence

Planet Haskell - Sat, 08/30/2014 - 5:59am
A few sources of information that those interested may find helpful.
Thanks to my colleague James Cheney for spotting these. (I previously circulated a pointer to the second but not to the first or third.) The sources appear reputable, but---as with everything on the net---caveat emptor.
Categories: Offsite Blogs

ANN: Agda 2.4.2

General haskell list - Fri, 08/29/2014 - 11:56pm
Agda 2.4.2 has been released! It comes with an experimental implementation of "type" classes (see "instance search" below). Download with cabal install Agda-2.4.2 (might need cabal update first) or go to Highlights: - Recursive instance search. Instance arguments are much faster than before and now work like a proper class system. - Major improvements to reflection - Quoting and unquoting of declarations and pattern matching lambdas. - New syntax to simplify using reflection: tactic f is sugar for quoteGoal g in unquote (f g) More details here:
Categories: Incoming News

Postdoctoral Researcher at Stevens Institute of Technology in domain-specific languages, security and privacy

General haskell list - Fri, 08/29/2014 - 9:27pm
Stevens Institute of Technology Department of Computer Science has an open position for a Postdoctoral Researcher in the fields of domain-specific languages, security and privacy, and mobile technologies for health information systems in Low and Middle Income Countries (LMIC). The MEDDC project (Mobile eHealthcare Delivery for Developing Countries) is a NIH and NSF-funded project that is developing and deploying tools for data collection and healthcare management in LMIC. It is affiliated with Central Africa IEDEA (International Epidemiological Databases to Evaluate AIDS), one of several NIH-funded projects that are engaged in data collection and analysis as part of the fight against the HIV/AIDS pandemic. The project has developed tools for producing data collection systems from declarative specifications. Some of the work to be done will involve adapting ideas from statistical and functional programming languages, to pursue a domain-specific language approach to developing local capacity for data analys
Categories: Incoming News

Has anyone had success using PhoneGap and Haste to build mobile apps in Haskell?

Haskell on Reddit - Fri, 08/29/2014 - 8:54pm

Given the plethora of Haskell to JS compilers (UHC, Fay, Haste) as well as HTML combinator libraries (i.e. Blaze) I was curious if anyone's had success using them in conjunction with the PhoneGap platform to build native apps in Haskell, or if there were particular interoperability problems or any other gotchas that make this an infeasible approach.

submitted by kunwoo32
[link] [7 comments]
Categories: Incoming News

Is there any way to get the nth element of a balanced tree using only fold and no direct recursion?

Haskell on Reddit - Fri, 08/29/2014 - 8:22pm

Is it possible to implement the "get" function bellow without using any form of recursion other than the provided fold?

data Tree a = Nil | Box a | Pair (Tree a) (Tree a) fold f g h Nil = h fold f g h (Box a) = g a fold f g h (Pair a b) = f (fold f g h a) (fold f g h b) summation :: (Num a) => Tree a -> a summation = fold (+) id 0 get :: Int -> Tree a -> a get n t = undefined term = Pair (Pair (Box 0) (Box 10)) (Pair (Box 20) (Box 30)) main = do print $ summation term {-print $ get 2 term -- should print 20-} submitted by SrPeixinho
[link] [7 comments]
Categories: Incoming News

Chris Wong: Hackage update, part 4

Planet Haskell - Fri, 08/29/2014 - 6:00pm

A lot has happened with Hackage since my last update. Now that the Summer of Code is over, I’ll summarize the work I’ve done since then, and outline where this project will go next.

What’s “build reporting”?

Since my project covered a few obscure parts of Hackage and Cabal, I think it’s worthwhile to clear some terminology first.

If you’ve uploaded a library to Hackage before, you may have noticed that the Haddock documentation does not appear straight away. Since building a package can be quite resource intensive, the job is handled by a dedicated build bot. This bot continually polls for new packages, invokes cabal install on them (with some special flags, which I’ll go into later), and uploads the result.

Of course, this process does not always succeed. If a package fails to compile, then it will not have any documentation either. This is clearly very inconvenient.

Fortunately, recent versions of cabal include a feature called build reporting. When invoked with the --build-summary option, cabal creates a file containing useful information about the build. Here’s an example using the robot package:

$ cabal install robot --build-summary='$' ... $ cat package: robot- os: linux arch: x86_64 compiler: ghc-7.6.3 client: cabal-install- dependencies: xhb-0.5.2014.4.10 transformers- exceptions-0.6.1 containers- base- install-outcome: InstallOk docs-outcome: NotTried tests-outcome: NotTried

Since the build bot uses cabal, it has access to these reports as well. So whenever the bot completes a build — successful or not — it posts the corresponding report to Hackage. You can read these reports yourself via a special URL; for our robot example it’s

In summary: if the docs for a package are missing, then the reports will tell us why. If there are no reports, then it must mean the build bot hasn’t attempted the package yet. All is fine and dandy, at least in theory.


… not all builds were reported. The gaps were in two places: planning failures and package candidates. My latest patch to cabal fixed both these issues.

Reporting planning failures

A planning failure is when cabal-install cannot find a consistent set of dependencies to use. You can trigger a planning failure yourself:

$ cabal install robot --constraint='robot < 1.1' --constraint='robot > 1.1' cabal: Could not resolve dependencies: ...

Since we can’t have a robot which is both older and newer than 1.1, the resolver fails.

Formerly, as dependency resolution ran early in the build process, any failures at this stage did not generate a corresponding report. So if the build bot encountered a planning failure, all the user saw was missing documentation, with no hints as to what went wrong.

The fix was mostly straightforward, save for one issue: since users can report their own builds, a naïve implementation would have lead to Hackage being swamped with frivolous reports. So this feature is guarded behind a flag (--report-planning-failure), and disabled by default.

Reporting candidate builds

Hackage has a feature called build candidates. This lets package maintainers upload and test packages without publishing them to the main site.

Again, the problem was the lack of reporting: when a candidate was uploaded, the build bot would compile the package but not submit a report. This was a major issue, since this reporting was what motivated the feature in the first place.

After some digging, I traced this to a bug in cabal. A candidate is not published in the main package index (by definition), so it is impossible to refer to one by name (e.g. hello-1.0). So the build bot invokes cabal using the bare URL instead (e.g.

The problem was if only a URL was given, cabal considered it a “local” package and did not generate a report. The reason for this behavior is outside the scope of this post, but the fix was clear: change cabal to generate reports for all packages, no matter how they are specified on the command line.

Where to next?

Though the Summer of Code has ended, my work with Hackage has not. There are still many issues that need clearing up, especially with the candidates feature; I’ll continue hacking away at them in my spare time.

And lest I forget — many thanks to my mentor Duncan Coutts for his guidance throughout this project! I had plenty of fun this summer, and learned just as much.

Categories: Offsite Blogs

Announcing Persistent 2.0

Haskell on Reddit - Fri, 08/29/2014 - 5:05pm
Categories: Incoming News

Yesod Web Framework: Announcing Persistent 2

Planet Haskell - Fri, 08/29/2014 - 3:46pm

We are happy to announce the release of persistent 2.0

persistent 2.0 adds a flexible key type and makes some breaking changes. 2.0 is an unstable release that we want your feedback on for the soon to follow stable 2.1 release.

New Features
  • type-safe composite primary and foreign keys
  • added an upsert operation (update or insert)
  • added an insertMany_ operation
  • An Id suffix is no longer automatically assumed to be a Persistent type
  • JSON serialization * MongoDB ids no longer have a prefix 'o' character.
Breaking changes
  • Use a simple ReaderT for the underlying connection
  • fix postgreSQL timezone storage
  • remove the type parameter from EntityDef and FieldDef
In depthComposite keys

The biggest limitation of data modeling with persistent is an assumption of a simple (for current SQL backends an auto-increment) primary key. We learned from Groundhog that a more flexible primary key type is possible. Persistent adds a similar flexible key type while maintaining its existing invariant that a Key is tied to a particular table.

To understand the changes to the Key data type, lets look at a change in the test suite for persistent 2.

i <- liftIO $ randomRIO (0, 10000) - let k = Key $ PersistInt64 $ abs i + let k = PersonKey $ SqlBackendKey $ abs i

Previously Key contained a PersistValue. This was not type safe. PersistValue is meant to serialize any basic Haskell type to the database, but a given table only allows specific values as the key. Now we generate the PersonKey data constructor which specifies the Haskell key types. SqlBackendKey is the default key type for SQL backends.

Now lets look at code from CompositeTest.hs

mkPersist sqlSettings [persistLowerCase| Parent name String maxlen=20 name2 String maxlen=20 age Int Primary name name2 age deriving Show Eq Child name String maxlen=20 name2 String maxlen=20 age Int Foreign Parent fkparent name name2 age deriving Show Eq |]

Here Parent has a composite primary key made up of 3 fields. Child uses that as a foreign key. The primary key of Child is the default key for the backend.

let parent = Parent "a1" "b1" 11 let child = Child "a1" "b1" 11 kp <- insert parent _ <- insert child testChildFkparent child @== parentFuture changesShort-term improvements

Before the 2.1 release I would like to look at doing some simple things to speed up model compilation a little bit.

  • Speed up some of the compile-time persistent code (there is a lot of obviously naive code).
  • Reduce the size of Template Haskell generation (create a reference for each EntityDef and some other things rather than potentially repeatedly inlining it)
Medium-term improvement: better support for Haskell data types

We want to add better support for modeling ADTs, particularly for MongoDB where this is actually very easy to do in the database itself. Persistent already support a top-level entity Sum Type and a simple field ADT that is just an enumeration.

Another pain point is serializing types not declared in the schema. The declaration syntax in groundhog is very verbose but allows for this. So one possibility would be to allow the current DRY persistent declaration style and also a groundhog declaration style.

Long-term improvements: Projections

It would be possible to add projections now as groundhog or esqueleto have done. However, the result is not as end-user friendly as we would like. When the record namespace issue is dealt with in the GHC 7.10 release we plan on adding projections to persistent.

Ongoing: Database specific functionality

We always look forward to see more databases adapters for persistent. In the last year, a Redis and ODBC adapter were added.

Every database is different though, and you also want to take advantage of your database-specific features. esqueleto and persistent-mongoDB have shown how to build database specific features in a type-safe way on top of persistent.


Although the persistent code has no dependency on Yesod, I would like to make the infrastructure a little more independent of yesod. The first steps would be

  • putting it under a different organization on github.
  • having a separate mail list (should stackoverflow be prioritized over e-mail?)
Categories: Offsite Blogs