Functional Programming

August Haskell Daily puzzles and solutions

Planet Haskell - 40 min 4 sec ago
August, 2014August 1st, 2014: "But programming isn't math, so ..." Today's #haskell problem? 'Fix' yesterday's solution to be less ... 'icky.' http://lpaste.net/108559 π, fast (So you're not eating π? ... okay: 'quickly.') A solution set to today's exercises with Wow-o-wow results. http://lpaste.net/108576Bonus: August 1st, 2014: This is Embarrassing(ly parallel) to have π in da face!  http://lpaste.net/108562A-to-the-ST for da D-down-low-on-the-SL. Today's #haskell exercise is write your own language, then some rules. Yeah. http://lpaste.net/108733. LAWLZ! NAND on the A-to-the-ST! http://lpaste.net/108758 A solution to the first 2 exercises to today's problem. YMMV: not pretty nor generic.Baby needs a new pair of shoes! And you need a new daily #haskell problem to solve. http://lpaste.net/108820 Done! ;) Love is the Universal Language. No, wait. We were talking about Money, yes? Me confused. Solution to today's exercise http://lpaste.net/108829. I have a Yen for Thinking Japanese, or so I think so ... a solution to the bonus #haskell exercise http://lpaste.net/108871Bayes was a man of letters. A Bayesian classifier for letter-recognition? Sure, let's give it a go for today's #haskell exercise. http://lpaste.net/108901 So now we know 'M' looks like 'W' to some peeps but 'B', 'I', 'O' check out fine, so WE ARE READING WITH HASKELL! YAY http://lpaste.net/108916 ... added definitions to do test runs over the entire data set and then did various runs, tweaking the system. Results noted. Informative.Today's #haskell exercise. An expert system for blood donation. I use the term 'expert' loosely, eh? ;) http://lpaste.net/108989 Have at it! "I vant to drinq yur bloot! Bwa-hahaha!" Okay. That quote is just ... creepy. A solution to today's exercise is at http://lpaste.net/108994Veni, Vidi, ... Duci? http://lpaste.net/109043 Today's #haskell exercise. It is a relief to know that no tactical nukes were launched by testing the solution to today's #haskell exercise. http://lpaste.net/109061 or How do you count Mississippi's in Roman numerals?August 11th, 2014, Monday: You've heard of 'Rock Management'? How about ROCK LOBSTERS! GIVE ME A ROCK, NAOW!!!1!!!!11! Today's #haskell exercise http://lpaste.net/109188 August 12th, 2014, Tuesday: To Fract or Not to Fract: why are we even considering this question? Today's #haskell exercise http://lpaste.net/109219 Ooh! Bonus problem? On a Tuesday? Wowsers! Today's #haskell #bonus problem: "Continuum spectrum maximum... uh, 'thing'um" http://lpaste.net/109205August 13th, 2014, Wednesday. No problem! (literally), but: "Fract! The Cylons!" No... wait: Starbuck used a different word. A solution to yesterday's fracting problem is at http://lpaste.net/109341Flatliners. No fracting, no 'peak'ing, just a baseline data set of initializeSpectrum defined with flatline function.Twin Peaks. Still not fracted, but data set with two spikes rolled into the base data set with smoothSpike fn Fracted. Data set with peaks, fracted using the frackedSpike functionAugust 14th, 2014, Thursday: Pining for that next fibo date-time before 2584. Today's #haskell problem inspired by @AlgebraFact http://lpaste.net/109349. Updated problem. Tightened up return value, removing unnecessary semideterminism. So, it gives, leik, a septatuple answer, leik. ... Yeah. Time keeps flowing like a (Fibonacci) river, to the sea. http://lpaste.net/109389 A solution to  the 'next Fibonacci' problem posted today.Hail, Eris! or the Law of Fives or today's #haskell problem (implementing a Ripple-down rule set). Do it to it! http://lpaste.net/109350. One of three-parter solution to today's problem: Forall Existential(ism) http://lpaste.net/109458 A solution allowing forall-quantified values. Two of the three-part solution: All you need is fnord (la-di-da-di-dah)! Rippling down (and accumulating fired) rules http://lpaste.net/109433. Third of three-part solution: RippleDownRuleto ergo sum, adding rules to the RDR system http://lpaste.net/109473.  Updated the 3rd solution to the RDR (Writer monad definition) to ripple down to left and right, fixing inconsistency in rule findings.August 18th, 2014: What's FP good for? Crypto and technical (financial) indicators. Why? Um, let's do today's #haskell exercise! http://lpaste.net/109553. Full on, all the way! Double Rain-... wait: line-graph. Solution to today's #haskell exercise http://lpaste.net/109597August 19th, 2014: What does it all mean? All the way! No, wait: this is just today's #haskell exercise (backtesting SMA indicator ). http://lpaste.net/109617 Take the monoid and run(State-WriterT), or WAAH! WAAH! I lost 100 corn chips on my investment strategy or, solution: http://lpaste.net/109687 But, as solace, it does come with a pretty picture, illustrating today's solution. Ooh! August 20th, 2014: Next up for today's #haskell exercise is the Exponential Moving Average. http://lpaste.net/109689 A solution to the E(xponential)M(oving)A(verage) #haskell problem: Stately Conformance http://lpaste.net/109707 August 21st, 2014: My Jeans. No ... I meant: 'GENES'! That's it. Today's #haskell exercise. http://lpaste.net/109749 A solution to (not even CLOSE to) 'yesterday's' #haskell exercise: Nature or Nurture? We present a genetic algorithm http://lpaste.net/110330August 22nd, 2014: Today's (much delayed) #haskell problem: the Silver Ratio http://lpaste.net/109817 (from @AlgebraFact ) Every cloud has a silver lining .. Every Haskell problem has a solution. (sometimes) (except noncomputable problems) http://lpaste.net/109831August 25th, 2014: LYADCFGG! Today's #haskell exercise? (automated/learned) Document classification. http://lpaste.net/109980/August 26th, 2014: "Join me, Luke, on the Dark Side of the Force, and help me go #FORTH to solve today's #haskell exercise! MWA-HAHA!" http://lpaste.net/110062 The World's smallest DSL: Forth. A solution to today's #haskell exercise http://lpaste.net/edit/110085August 28th, 2014: "As I compose this #haskell problem ... p.s. I love you ... You! You! You!" #1960s #song http://lpaste.net/110135 A little card logic problem. Oh, NOES! LOOK OUT! IT'S A CARD-#SHARKNADO! Nah, it's just 'today's #haskell solution, is all http://lpaste.net/110334 August 29th, 2014: Groovitudes! WordNet Themes! or: today's #haskell exercise http://lpaste.net/110171 A 3x3 matrix has 36 possible solutions. A 5x5 matrix? Over 200M poss solutions? YIKES! A solution to the themed-words http://lpaste.net/110293NotesThe Forth language problem solution given on August 26th gives a very snazzy RPN ('reverse Polish notation') calculator, but that's all it does the ':'-defining word needs access and look-ahead to the program parsed stream, and that's a bit more to ask than pushing and popping stack operators.For the August 29th problem(WordNet themes) the raw generated solution set is over 209M possibilities. My little Haskell program was not finished scanning them over four hours when I killed the process. However, my dear wife solved the problem in under five minutes. Setting aside the fact that she's a genius, the program needs to be better. It needs to use the ontology of English-language words to eliminate fruitless endeavors during their generation, not afterwards during the test phase.

Planning Yesod 1.4

Planet Haskell - 40 min 4 sec ago
Now that persistent 2.0 is out the door, it's time to start talking about Yesod version 1.4. First question you might ask: what happened to Yesod 1.3? Answer: a few of the Yesod libraries (e.g., yesod-auth) are already on version 1.3, so to avoid confusion, we're jumping straight to 1.4.Second question: what are we planning on breaking this time? Answer: hopefully nothing! The main purpose of this release is actually to just remove some backwards-compatibility hacks in the Yesod codebase for older versions of dependencies, like shakespeare pre-2.0, conduit pre-1.2, WAI pre-3.0, and persistent pre-2.0.There are few exceptions to this, which should hopefully have minimal impact on users. You can see these in the detailed change list. One change I'd like to call out is the updated routing system. This is a fundamental change to how yesod-routes works. The generated code is drastically simpler as a result. Instead of constructing a data structure that allows for efficient pattern matching of the request path and then attempting to parse the resulting pieces, the new code simply generates a series of clauses, one for each route, and ensures proper parsing using view patterns. In my initial benchmarking, this made routing twice as fast as Yesod 1.2. I would release this as part of 1.2, but it introduces a new requirement on the ViewPatterns language extension. So instead, I held it off for the 1.4 release.If there are other breaking changes that people would like to propose, now's the time to do it. But be aware that I'll likely push back hard on any breakage. If there's a very good reason for it, we can do it. But I'd rather keep stability wherever possible.There's one exception to that rule, which is the purpose of the rest of this blog post: the scaffolded site. Making changes to the scaffolded site never breaks existing application, and therefore we can be much more liberal about changing things there. There is a downside in terms of education: all existing tutorials on the scaffolding would need to be updated. But one of my points below addresses that.So here are my proposed scaffolding changes:Let's move away from config files towards environment variables for configuration. A config file is still a convenient way to record configuration, but injecting that configuration through environment variables means configuration can also be stored in a database or elsewhere and injected through environment variables the same way.Along the same lines, we would no longer need a command line argument to indicate which environment we're in (devel vs production, etc). All such settings would be controlled via environment variables.To allow for easy development, we would have a single YESOD_DEVEL environment variables which would indicate if we're currently in development. If so, it would apply a number of default environment variable values to avoid the need to set these in your shell manually.Finally, and I expect this to be controversial: let's use classy-prelude-yesod in the Import module, instead of just taking Prelude with a few objectionable functions filtered out.This is just a first pass at a scaffolding cleanup, I'm sure there are other improvements that can be made as well.I don't have a specific date on a Yesod 1.4 release, but I'm not expecting it to be a long development process. The vast majority of the work is already done (on the yesod-1.4 branch), and that codebase is already being used extensively in a rather large Yesod application, so I'm not too worried about regressions having slipped in.

DebConf 14

Planet Haskell - 40 min 4 sec ago
I’m writing this blog post on the plain 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 crazy idea” 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 people.debian.org 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 wuiet.debian.org and run ~nomeata/binNMUs --sql; it then uses the projectb and wanna-build databases directly. Thanks to the ftp team for opening up incoming.debian.org, 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. 2014-08-30T15:10:58Z Joachim Breitner mail@joachim-breitner.de

Howard on Curry-Howard

Planet Haskell - 40 min 4 sec ago
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 ConstructionDear 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, -- PAnd 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.Bill

Independent information on independence

Planet Haskell - 40 min 4 sec ago
A few sources of information that those interested may find helpful.https://fullfact.org/scotlandhttp://www.futureukandscotland.ac.uk/http://www.futureukandscotland.ac.uk/sites/default/files/papers/Scotland%27s%20Decision%20final%20ebook.pdfThanks 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.

Announcing Persistent 2

Planet Haskell - 40 min 4 sec ago
We are happy to announce the release of persistent 2.0persistent 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 Featurestype-safe composite primary and foreign keysadded an upsert operation (update or insert)added an insertMany_ operationFixesAn Id suffix is no longer automatically assumed to be a Persistent typeJSON serialization * MongoDB ids no longer have a prefix 'o' character.Breaking changesUse a simple ReaderT for the underlying connectionfix postgreSQL timezone storageremove the type parameter from EntityDef and FieldDefIn depthComposite keysThe 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 iPreviously 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.hsmkPersist 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 improvementsBefore 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 typesWe 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: ProjectionsIt 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 functionalityWe 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.OrganizationAlthough 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 beputting it under a different organization on github.having a separate mail list (should stackoverflow be prioritized over e-mail?)

Licentiate Thesis is now publicly available

Planet Haskell - 40 min 4 sec ago
My recently accepted Licentiate Thesis, which I posted about a couple of days ago, is now available in JyX. Here is the abstract again for reference: Kaijanaho, Antti-Juhani The extent of empirical evidence that could inform evidence-based design of programming languages. A systematic mapping study. Jyväskylä: University of Jyväskylä, 2014, 243 p. (Jyväskylä Licentiate Theses […]

Senior Software Engineer (Functional) at McGraw-Hill Education (Full-time)

Planet Haskell - 40 min 4 sec ago
This Senior Software Engineer position is with the new LearnSmart team at McGraw-Hill Education's new and growing Research & Development center in Boston's Innovation District. We make software that helps college students study smarter, earn better grades, and retain more knowledge. The LearnSmart adaptive engine powers the products in our LearnSmart Advantage suite — LearnSmart, SmartBook, LearnSmart Achieve, LearnSmart Prep, and LearnSmart Labs. These products provide a personalized learning path that continuously adapts course content based on a student’s current knowledge and confidence level. On our team, you'll get to: Move textbooks and learning into the digital era Create software used by millions of students Advance the state of the art in adaptive learning technology Make a real difference in education Our team's products are built with Flow, a functional language in the ML family. Flow lets us write code once and deliver it to students on multiple platforms and device types. Other languages in our development ecosystem include especially JavaScript, but also C++, SWF (Flash), and Haxe. If you're interested in functional languages like Scala, Swift, Erlang, Clojure, F#, Lisp, Haskell, and OCaml, then you'll enjoy learning Flow. We don't require that you have previous experience with functional programming, only enthusiasm for learning it. But if you have do some experience with functional languages, so much the better! (On-the-job experience is best, but coursework, personal projects, and open-source contributions count too.) We require only that you: Have a solid grasp of CS fundamentals (languages, algorithms, and data structures) Be comfortable moving between multiple programming languages Be comfortable with modern software practices: version control (Git), test-driven development, continuous integration, Agile Get information on how to apply for this position. 2014-08-28T21:18:54Z

Dealing with Asynchronous Exceptions during Resource Acquisition

Planet Haskell - 40 min 4 sec ago
Introduction ------------ Consider the following code: we open a socket, compute with it, and finally close the socket again. The computation happens inside an exception handler (try), so even when an exception happens we still close the socket: ``` {.Haskell} example1 :: (Socket -> IO a) -> IO a [...]

Calling a Rust library from C (or anything else!)

Planet Haskell - 40 min 4 sec ago
One reason I'm excited about Rust is that I can compile Rust code to a simple native-code library, without heavy runtime dependencies, and then call it from any language. Imagine writing performance-critical extensions for Python, Ruby, or Node in a safe, pleasant language that has static lifetime checking, pattern matching, a real macro system, and other goodies like that. For this reason, when I started html5ever some six months ago, I wanted it to be more than another "Foo for BarLang" project. I want it to be the HTML parser of choice, for a wide variety of applications in any language.Today I started work in earnest on the C API for html5ever. In only a few hours I had a working demo. And this is a fairly complicated library, with 5,000+ lines of code incorporatingmost of the hilariously complicated parsing rules in the HTML spec,a Rust syntax extension for writing parse rules in a concise form that matches the spec,compile-time perfect hash maps for string interning and named characters, andlots and lots of generic code — if this library were written in C++, almost all of it would be in header files.It's pretty cool that we can use all this machinery from C, or any language that can call C. I'll describe first how to build and use the library, and then I'll talk about the implementation of the C API.html5ever (for C or for Rust) is not finished yet, but if you're feeling adventurous, you are welcome to try it out! And I'd love to have more contributors. Let me know on GitHub about any issues you run into.Using html5ever from CLike most Rust libraries, html5ever builds with Cargo.$ git clone https://github.com/kmcallister/html5ever$ cd html5ever$ git checkout dev$ cargo build Updating git repository `https://github.com/sfackler/rust-phf` Compiling phf_mac v0.0.0 (https://github.com/sfackler/rust-phf#f21e2a41) Compiling html5ever-macros v0.0.0 (file:///tmp/html5ever) Compiling phf v0.0.0 (https://github.com/sfackler/rust-phf#f21e2a41) Compiling html5ever v0.0.0 (file:///tmp/html5ever)The C API isn't Cargo-ified yet, so we'll build it using the older Makefile-based system.$ mkdir build$ cd build$ ../configure$ make libhtml5ever_for_c.arustc -D warnings -C rpath -L /tmp/html5ever/target -L /tmp/html5ever/target/deps \ -o libhtml5ever_for_c.a --cfg for_c --crate-type staticlib /tmp/html5ever/src/lib.rswarning: link against the following native artifacts when linking against this static librarynote: the order and any duplication can be significant on some platforms, and so may need to be preservednote: library: rtnote: library: dlnote: library: pthreadnote: library: gcc_snote: library: pthreadnote: library: cnote: library: mNow we can build an example C program using that library, and following the link instructions produced by rustc.$ H5E_PATH=/tmp/html5ever$ gcc -Wall -o tokenize tokenize.c -I $H5E_PATH/capi -L $H5E_PATH/build \ -lhtml5ever_for_c -lrt -ldl -lpthread -lgcc_s -lpthread -lc -lm$ ./tokenize 'Hello, world!'CHARS : HelloCHARS : ,CHARS : TAG : ATTR: class="excellent"CHARS : world!TAG : The build process is pretty standard for C; we just link a .a file and its dependencies. The biggest obstacle right now is that you won't find the Rust compiler in your distro's package manager, because the language is still changing so rapidly. But there's a ton of effort going into stabilizing the language for a Rust 1.0 release this year. It won't be too long before rustc is a reasonable build dependency.Let's look at the C client code.#include #include "html5ever.h"void put_str(const char *x) { fputs(x, stdout);}void put_buf(struct h5e_buf text) { fwrite(text.data, text.len, 1, stdout);}void do_start_tag(void *user, struct h5e_buf name, int self_closing, size_t num_attrs) { put_str("TAG : <"); put_buf(name); if (self_closing) { putchar('/'); } put_str(">\n");}// ...struct h5e_token_ops ops = { .do_chars = do_chars, .do_start_tag = do_start_tag, .do_tag_attr = do_tag_attr, .do_end_tag = do_end_tag,};struct h5e_token_sink sink = { .ops = &ops, .user = NULL,};int main(int argc, char *argv[]) { if (argc < 2) { printf("Usage: %s 'HTML fragment'\n", argv[0]); return 1; } struct h5e_tokenizer *tok = h5e_tokenizer_new(&sink); h5e_tokenizer_feed(tok, h5e_buf_from_cstr(argv[1])); h5e_tokenizer_end(tok); h5e_tokenizer_free(tok); return 0;}The struct h5e_token_ops contains pointers to callbacks. Any events we don't care to handle are left as NULL function pointers. Inside main, we create a tokenizer and feed it a string. html5ever for C uses a simple pointer+length representation of buffers, which is this struct h5e_buf you see being passed by value.This demo only does tokenization, not tree construction. html5ever can perform both phases of parsing, but the API surface for tree construction is much larger and I didn't get around to writing C bindings yet.Implementing the C APISome parts of Rust's libstd depend on runtime services, such as task-local data, that a C program may not have initialized. So the first step in building a C API was to eliminate all std:: imports. This isn't nearly as bad as it sounds, because large parts of libstd are just re-exports from other libraries like libcore that we can use with no trouble. To be fair, I did write html5ever with the goal of a C API in mind, and I avoided features like threading that would be difficult to integrate. So your library might give you more trouble, depending on which Rust features you use.The next step was to add the #![no_std] crate attribute. This means we no longer import the standard prelude into every module. To compensate, I added use core::prelude::*; to most of my modules. This brings in the parts of the prelude that can be used without runtime system support. I also added many imports for ubiquitous types like String and Vec, which come from libcollections.After that I had to get rid of the last references to libstd. The biggest obstacle here involved macros and deriving, which would produce references to names under std::. To work around this, I create a fake little mod std which re-exports the necessary parts of core and collections. This is similar to libstd's "curious inner-module".I also had to remove all uses of format!(), println!(), etc., or move them inside #[cfg(not(for_c))]. I needed to copy in the vec!() macro which is only provided by libstd, even though the Vec type is provided by libcollections. And I had to omit debug log messages when building for C; I did this with conditionally-defined macros.With all this preliminary work done, it was time to write the C bindings. Here's how the struct of function pointers looks on the Rust side:#[repr(C)]pub struct h5e_token_ops { do_start_tag: extern "C" fn(user: *mut c_void, name: h5e_buf, self_closing: c_int, num_attrs: size_t), do_tag_attr: extern "C" fn(user: *mut c_void, name: h5e_buf, value: h5e_buf), do_end_tag: extern "C" fn(user: *mut c_void, name: h5e_buf), // ...}The processing of tokens is straightforward. We pattern-match and then call the appropriate function pointer, unless that pointer is NULL. (Edit: eddyb points out that storing NULL as an extern "C" fn is undefined behavior. Better to use Option, which will optimize to the same one-word representation.) To create a tokenizer, we heap-allocate the Rust data structure in a Box, and then transmute that to a raw C pointer. When the C client calls h5e_tokenizer_free, we transmute this pointer back to a box and drop it, which will invoke destructors and finally free the memory.You'll note that the functions exported to C have several special annotations:#[no_mangle]: skip name mangling, so we end up with a linker symbol named h5e_tokenizer_free instead of _ZN5for_c9tokenizer18h5e_tokenizer_free.unsafe: don't let Rust code call these functions unless it promises to be careful.extern "C": make sure the exported function has a C-compatible ABI. The data structures similarly get a #[repr(C)] attribute.Then I wrote a C header file matching this ABI:struct h5e_buf { unsigned char *data; size_t len;};struct h5e_buf h5e_buf_from_cstr(const char *str);struct h5e_token_ops { void (*do_start_tag)(void *user, struct h5e_buf name, int self_closing, size_t num_attrs); void (*do_tag_attr)(void *user, struct h5e_buf name, struct h5e_buf value); void (*do_end_tag)(void *user, struct h5e_buf name); /// ...};struct h5e_tokenizer;struct h5e_tokenizer *h5e_tokenizer_new(struct h5e_token_sink *sink);void h5e_tokenizer_free(struct h5e_tokenizer *tok);void h5e_tokenizer_feed(struct h5e_tokenizer *tok, struct h5e_buf buf);void h5e_tokenizer_end(struct h5e_tokenizer *tok);One remaining issue is that Rust is hard-wired to use jemalloc, so linking html5ever will bring that in alongside the system's libc malloc. Having two separate malloc heaps will likely increase memory consumption, and it prevents us from doing fun things like allocating Boxes in Rust that can be used and freed in C. Before Rust can really be a great choice for writing C libraries, we need a better solution for integrating the allocators.If you'd like to talk about calling Rust from C, you can find me as kmc in #rust and #rust-internals on irc.mozilla.org. And if you run into any issues with html5ever, do let me know, preferably by opening an issue on GitHub. Happy hacking!

Informatics Independence Referendum Debate - the result

Planet Haskell - 40 min 4 sec ago
Here is the outcome of the debate announced earlier:BeforeYes 19No 25Undecided 28AfterYes 28No 31Undecided 26(Either some people entered after the debate began, or some people began the debate unsure even whether they were undecided.)Thank you to Alan, Mike, and the audience for a fantastic debate. The audience asked amazing questions on both sides, clearly much involved with the process. Video of debate here.Alan's slides here.My slides here.

Creating well-behaved Hakyll blog posts

Planet Haskell - 40 min 4 sec ago
Posts in a Hakyll-powered blog need to be created with care, if you want your feed to work well with clients and aggregators. There are many things to remember: If you have clones of your site, decide which one to work in and make sure it’s up to date Create the file in the right place Name it consistently (I use YYYY-MM-DD-url-safe-title.md) In my setup, prefix it with _ if it’s a draft (I render but don’t publish those) Set title, tags, and author with a metadata block Set published time with metadata to get a more precise timestamp than Hakyll can guess from the filename. Include a time zone. Use the right format. When moving a post from draft to published: Update the published time Update the file name if the title or publish date has changed If changing a post after it has been published: set updated time in the metadata At some point, commit it to version control and sync it to other clones I find this makes blogging feel tedious, especially after an absence when I’ve forgotten the details. Case in point, I managed to share an ugly template post with Planet Haskell readers while working on this one. So I’m trying out this bash shell script, maybe it will help. Adjust to suit your setup.(updated 2014/8/27) # add to ~/.bashrc BLOGDIR=~/src/MYSITE.com/blog # List recent blog posts. alias blog-ls="ls $BLOGDIR | tail -10" # Create a new hakyll-compatible draft blog post. # blog-new ["The Title" ["tag1, tag2" ["Author Name"]]] function blog-new() { ( TITLE=${1:-Default Title} TAGS=${2:-defaulttag1, defaulttag2} AUTHOR=${3:-Default Author Name} SLUG=${TITLE// /-} DATE=`date +"%Y-%m-%d"` TIME=`date +"%Y-%m-%d %H:%M:%S%Z"` FILE=_$DATE-$SLUG.md echo creating $BLOGDIR/$FILE cat <>$BLOGDIR/$FILE && emacsclient -n $BLOGDIR/$FILE --- title: $TITLE tags: $TAGS author: $AUTHOR published: $TIME --- EOF ) } An example: $ blog-new 'Scripted Hakyll blog post creation' 'hakyll, haskell' creating _2014-05-03-Scripted-Hakyll-blog-post-creation.md (file opens in emacs, edit & save) $ make ./site build Initialising... Creating store... Creating provider... Running rules... Checking for out-of-date items Compiling updated blog/_2014-05-03-Scripted-Hakyll-blog-post-creation.md Success See also part 2. 2014-08-27T02:15:00Z 2014-05-03T16:08:00Z

Well-behaved Hakyll blog posts, continued

Planet Haskell - 40 min 4 sec ago
More hakyll blog fixes: Ugly things showing on planets My posts were showing unwanted things on planet haskell - double heading, redundant date, tag links, and ugly disqus html. By comparing with Jasper Van der Jeugt’s blog, I found the problem: I was snapshotting content for the feed at the wrong time, after applying the post template: >>= return . fmap demoteHeaders >>= loadAndApplyTemplate "templates/post.html" (postCtx tags) >>= saveSnapshot "content" >>= loadAndApplyTemplate "templates/default.html" defaultContext Better: >>= saveSnapshot "content" -- >>= return . fmap demoteHeaders >>= loadAndApplyTemplate "templates/post.html" (postCtx tags) >>= loadAndApplyTemplate "templates/default.html" defaultContext Manual feed publishing The main blog feed is now generated with a _ prefix, and I must manually rename it (with make feed) to make it live it on Planet Haskell. This will hopefully reduce snafus (and not create new ones). ./site.hs 95 - create ["blog.xml"] $ do + create ["_blog.xml"] $ do ./Makefile 14 +feed: _site/blog.xml + +_site/blog.xml: _site/_blog.xml + cp _site/_blog.xml _site/blog.xml + Better HTML titles Changed the “Joyful Systems” prefix to a suffix in the HTML page titles, making search results and browser tab names more useful. 2014-08-27T02:00:00Z 2014-05-06T13:40:00Z

IAP: conduit stream fusion

Planet Haskell - 40 min 4 sec ago
Both the changes described in this blog post, and in the previous blog post, are now merged to the master branch of conduit, and have been released to Hackage as conduit 1.2.0. That doesn't indicate stream fusion is complete (far from it!). Rather, the optimizations we have so far are valuable enough that I want them to be available immediately, and future stream fusion work is highly unlikely to introduce further breaking changes. Having the code on Hackage will hopefully also make it easier for others to participate in the discussion around this code.Stream fusionLast time, I talked about applying the codensity transform to speed up conduit. This greatly increases performance when performing many monadic binds. However, this does nothing to help us with speeding up the "categorical composition" of conduit, where we connect two components of a pipeline together so the output from the first flows into the second. conduit usually refers to this as fusion, but given the topic at hand (stream fusion), I think that nomenclature will become confusing. So let's stick to categorical composition, even though conduit isn't actually a category.Duncan Coutts, Roman Leshchinskiy and Don Stewart wrote the stream fusion paper, and that technique has become integral to getting high performance in the vector and text packages. The paper is well worth the read, but for those unfamiliar with the technique, let me give a very brief summary:GHC is very good at optimising non-recursive functions.We express all of our streaming functions has a combination of some internal state, and a function to step over that state.Stepping either indicates that the stream is complete, there's a new value and a new state, or there's a new state without a new value (this last case helps avoid recursion for a number of functions like filter).A stream transformers (like map) takes a Stream as input and produces a new Stream as output.The final consuming functions, like fold, are the only place where recursion happens. This allows all other components of the pipeline to be inlined, rewritten to more efficient formats, and optimized by GHC.Let's see how this looks compared to conduit.Data typesI'm going to slightly rename data types from stream fusion to avoid conflicts with existing conduit names. I'm also going to add an extra type parameter to represent the final return value of a stream; this is a concept that exists in conduit, but not common stream fusion.data Step s o r = Emit s o | Skip s | Stop r data Stream m o r = forall s. Stream (s -> m (Step s o r)) (m s)The Step datatype takes three parameters. s is the internal state used by the stream, o is the type of the stream of values it generates, and r is the final result value. The Stream datatype uses an existential to hide away that internal state. It then consists of a step function that takes a state and gives us a new Step, as well as an initial state value (which is a monadic action, for cases where we want to do some initialization when starting a stream).Let's look at some functions to get a feel for what this programming style looks like:enumFromToS_int :: (Integral a, Monad m) => a -> a -> Stream m a () enumFromToS_int !x0 !y = Stream step (return x0) where step x | x <= y = return $ Emit (x + 1) x | otherwise = return $ Stop ()This function generates a stream of integral values from x0 to y. The internal state is the current value to be emitted. If the current value is less than or equal to y, we emit our current value, and update our state to be the next value. Otherwise, we stop.We can also write a function that transforms an existing stream. mapS is likely the simplest example of this:mapS :: Monad m => (a -> b) -> Stream m a r -> Stream m b r mapS f (Stream step ms0) = Stream step' ms0 where step' s = do res <- step s return $ case res of Stop r -> Stop r Emit s' a -> Emit s' (f a) Skip s' -> Skip s'The trick here is to make a function from one Stream to another. We unpack the input Stream constructor to get the input step and state functions. Since mapS has no state of its own, we simply keep the input state unmodified. We then provide our modified step' function. This calls the input step function, and any time it sees an Emit, applies the user-provided f function to the emitted value.Finally, let's consider the consumption of a stream with a strict left fold:foldS :: Monad m => (b -> a -> b) -> b -> Stream m a () -> m b foldS f b0 (Stream step ms0) = ms0 >>= loop b0 where loop !b s = do res <- step s case res of Stop () -> return b Skip s' -> loop b s' Emit s' a -> loop (f b a) s'We unpack the input Stream constructor again, get the initial state, and then loop. Each loop, we run the input step function.Match and mismatch with conduitThere's a simple, straightforward conversion from a Stream to a Source:toSource :: Monad m => Stream m a () -> Producer m a toSource (Stream step ms0) = lift ms0 >>= loop where loop s = do res <- lift $ step s case res of Stop () -> return () Skip s' -> loop s' Emit s' a -> yield a >> loop s'We extract the state, and then loop over it, calling yield for each emitted value. And ignoring finalizers for the moment, there's even a way to convert a Source into a Stream:fromSource :: Monad m => Source m a -> Stream m a () fromSource (ConduitM src0) = Stream step (return $ src0 Done) where step (Done ()) = return $ Stop () step (Leftover p ()) = return $ Skip p step (NeedInput _ p) = return $ Skip $ p () step (PipeM mp) = liftM Skip mp step (HaveOutput p _finalizer o) = return $ Emit p oUnfortunately, there's no straightforward conversion for Conduits (transformers) and Sinks (consumers). There's simply a mismatch in the conduit world- which is fully continuation based- to the stream world- where the upstream is provided in an encapsulated value. I did find a few representations that mostly work, but the performance characteristics are terrible.If anyone has insights into this that I missed, please contact me, as this could have an important impact on the future of stream fusion in conduit. But for the remainder of this blog post, I will continue under the assumption that only Source and Stream can be efficiently converted.StreamConduitOnce I accepted that I wouldn't be able to convert a stream transformation into a conduit transformation, I was left with a simple approach to start working on fusion: have two representations of each function we want to be able to fuse. The first representation would use normal conduit code, and the second would be streaming. This looks like:data StreamConduit i o m r = StreamConduit (ConduitM i o m r) (Stream m i () -> Stream m o r)Notice that the second field uses the stream fusion concept of a Stream-transforming function. At first, this may seem like it doesn't properly address Sources and Sinks, since the former doesn't have an input Stream, and the latter results in a single output value, not a Stream. However, those are really just special cases of the more general form used here. For Sources, we provide an empty input stream, and for Sinks, we continue executing the Stream until we get a Stop constructor with the final result. You can see both of these in the implementation of the connectStream function (whose purpose I'll explain in a moment):connectStream :: Monad m => StreamConduit () i m () -> StreamConduit i Void m r -> m r connectStream (StreamConduit _ stream) (StreamConduit _ f) = run $ f $ stream $ Stream emptyStep (return ()) where emptyStep _ = return $ Stop () run (Stream step ms0) = ms0 >>= loop where loop s = do res <- step s case res of Stop r -> return r Skip s' -> loop s' Emit _ o -> absurd oNotice how we've created an empty Stream using emptyStep and a dummy () state. And on the run side, we loop through the results. The type system (via the Void datatype) prevents the possibility of a meaningful Emit constructor, and we witness this with the absurd function. For Stop we return the final value, and Skip implies another loop.Fusing StreamConduitAssuming we have some functions that use StreamConduit, how do we get things to fuse? We still need all of our functions to have a ConduitM type signature, so we start off with a function to convert a StreamConduit into a ConduitM:unstream :: StreamConduit i o m r -> ConduitM i o m r unstream (StreamConduit c _) = c {-# INLINE [0] unstream #-}Note that we hold off on any inlining until simplification phase 0. This is vital to our next few rewrite rules, which is where all the magic happens.The next thing we want to be able to do is categorically compose two StreamConduits together. This is easy to do, since a StreamConduit is made up of ConduitMs which compose via the =$= operator, and Stream transformers, which compose via normal function composition. This results in a function:fuseStream :: Monad m => StreamConduit a b m () -> StreamConduit b c m r -> StreamConduit a c m r fuseStream (StreamConduit a x) (StreamConduit b y) = StreamConduit (a =$= b) (y . x) {-# INLINE fuseStream #-}That's very logical, but still not magical. The final trick is a rewrite rule:{-# RULES "fuseStream" forall left right. unstream left =$= unstream right = unstream (fuseStream left right) #-}We're telling GHC that, if we see a composition of two streamable conduits, then we can compose the stream versions of them and get the same result. But this isn't enough yet; unstream will still end up throwing away the stream version. We now need to deal with running these things. The first case we'll handle is connecting two streamable conduits, which is where the connectStream function from above comes into play. If you go back and look at that code, you'll see that the ConduitM fields are never used. All that's left is telling GHC to use connectStream when appropriate:{-# RULES "connectStream" forall left right. unstream left $$ unstream right = connectStream left right #-}The next case we'll handle is when we connect a streamable source to a non-streamable sink. This is less efficient than the previous case, since it still requires allocating ConduitM constructors, and doesn't expose as many opportunities for GHC to inline and optimize our code. However, it's still better than nothing:connectStream1 :: Monad m => StreamConduit () i m () -> ConduitM i Void m r -> m r connectStream1 (StreamConduit _ fstream) (ConduitM sink0) = case fstream $ Stream (const $ return $ Stop ()) (return ()) of Stream step ms0 -> let loop _ (Done r) _ = return r loop ls (PipeM mp) s = mp >>= flip (loop ls) s loop ls (Leftover p l) s = loop (l:ls) p s loop _ (HaveOutput _ _ o) _ = absurd o loop (l:ls) (NeedInput p _) s = loop ls (p l) s loop [] (NeedInput p c) s = do res <- step s case res of Stop () -> loop [] (c ()) s Skip s' -> loop [] (NeedInput p c) s' Emit s' i -> loop [] (p i) s' in ms0 >>= loop [] (sink0 Done) {-# INLINE connectStream1 #-} {-# RULES "connectStream1" forall left right. unstream left $$ right = connectStream1 left right #-}There's a third case that's worth considering: a streamable sink and non-streamable source. However, I ran into two problems when implementing such a rewrite rule:GHC did not end up firing the rule.There are some corner cases regarding finalizers that need to be dealt with. In our previous examples, the upstream was always a stream, which has no concept of finalizers. But when the upstream is a conduit, we need to make sure to call them appropriately.So for now, fusion only works for cases where all of the functions can by fused, or all of the functions before the $$ operator can be fused. Otherwise, we'll revert to the normal performance of conduit code.BenchmarksI took the benchmarks from our previous blog post and modified them slightly. The biggest addition was including an example of enumFromTo =$= map =$= map =$= fold, which really stresses out the fusion capabilities, and demonstrates the performance gap stream fusion offers.The other thing to note is that, in the "before fusion" benchmarks, the sum results are skewed by the fact that we have the overly eager rewrite rules for enumFromTo $$ fold (for more information, see the previous blog post). For the "after fusion" benchmarks, there are no special-case rewrite rules in place. Instead, the results you're seeing are actual artifacts of having a proper fusion framework in place. In other words, you can expect this to translate into real-world speedups.You can compare before fusion and after fusion. Let me provide a few select comparisons: Benchmark Low level or vector Before fusion After fusion Speedup map + sum 5.95us 636us 5.96us 99% monte carlo 3.45ms 5.34ms 3.70ms 71% sliding window size 10, Seq 1.53ms 1.89ms 1.53ms 21% sliding vector size 10, unboxed 2.25ms 4.05ms 2.33ms 42% Note at the map + sum benchmark is very extreme, since the inner loop is doing very cheap work, so the conduit overhead dominated the analysis.Streamifying a conduitHere's an example of making a conduit function stream fusion-compliant, using the map function:mapC :: Monad m => (a -> b) -> Conduit a m b mapC f = awaitForever $ yield . f {-# INLINE mapC #-} mapS :: Monad m => (a -> b) -> Stream m a r -> Stream m b r mapS f (Stream step ms0) = Stream step' ms0 where step' s = do res <- step s return $ case res of Stop r -> Stop r Emit s' a -> Emit s' (f a) Skip s' -> Skip s' {-# INLINE mapS #-} map :: Monad m => (a -> b) -> Conduit a m b map = mapC {-# INLINE [0] map #-} {-# RULES "unstream map" forall f. map f = unstream (StreamConduit (mapC f) (mapS f)) #-}Notice the three steps here:Define a pure-conduit implementation (mapC), which looks just like conduit 1.1's map function.Define a pure-stream implementation (mapS), which looks very similar to vector's mapS.Define map, which by default simply reexposes mapC. But then, use an INLINE statement to delay inlining until simplification phase 0, and use a rewrite rule to rewrite map in terms of unstream and our two helper functions mapC and mapS.While tedious, this is all we need to do for each function to expose it to the fusion framework.Vector vs conduit, mapM styleOverall, vector has been both the inspiration for the work I've done here, and the bar I've used to compare against, since it is generally the fastest implementation you can get in Haskell (and tends to be high-level code to boot). However, there seems to be one workflow where conduit drastically outperforms vector: chaining together monadic transformations.I put together a benchmark which does the same enumFromTo+map+sum benchmark I demonstrated previously. But this time, I have four versions: vector with pure functions, vector with IO functions, conduit with pure functions, and conduit with IO functions. You can see the results here, the important takeaway is:Pure is always faster, since it exposes more optimizations to GHC.vector and conduit pure are almost identical, at 57.7us and 58.1us.Monadic conduit code does have a slowdown (86.3us). However, monadic vector code has a drastic slowdown (305us), presumably because monadic binds defeat its fusion framework.So there seems to be at least one workflow for which conduit's fusion framework can outperform even vector!DownsidesThe biggest downside to this implementation of stream fusion is that we need to write all of our algorithms twice. This can possibly be mitigated by having a few helper functions in place, and implementing others in terms of those. For example, mapM_ can be implemented in terms foldM.There's one exception to this: using the streamSource function, we can convert a Stream into a Source without having to write our algorithm twice. However, due to differences in how monadic actions are performed between Stream and Conduit, this could introduce a performance degredation for pure Sources. We can work around that with a special case function streamSourcePure for the Identity monad as a base.Getting good performanceIn order to take advantage of the new stream fusion framework, try to follow these guidelines:Use fusion functions whenever possible. Explicit usage of await and yield will immediately kick you back to non-fusion (the same as explicit pattern matching defeats list fusion).If you absolutely cannot use an existing fusion function, consider writing your own fusion variant.When mixing fusion and non-fusion, put as many fusion functions as possible together with the $= operator before the connect operator $$.Next stepsEven though this work is now publicly available on Hackage, there's still a lot of work to be done. This falls into three main categories:Continue rewriting core library functions in streaming style. Michael Sloan has been working on a lot of these functions, and we're hoping to have almost all the combinators from Data.Conduit.List and Data.Conduit.Combinators done soon.Research why rewrite rules and inlining don't play nicely together. In a number of places, we've had to explicitly use rewrite rules to force fusion to happen, when theoretically inlining should have taken care of it for us.Look into any possible alternative formulations of stream fusion that provide better code reuse or more reliable rewrite rule firing.Community assistance on all three points, but especially 2 and 3, are much appreciated!

NSNotificationCenter, Swift and blocks

Planet Haskell - 40 min 4 sec ago
The conventional way to register observers with NSNotificationCenter is to use the target-action pattern. While this gets the job done, it's inherently not type-safe.For example, the following Swift snippet will compile perfectly:    NSNotificationCenter.defaultCenter().addObserver(self, selector: Selector("itemAdded:"),      name: MyNotificationItemAdded, object: nil)even though at runtime it will fail unless self has a method named itemAdded that takes exactly one parameter (leaving off that last colon in the selector will turn this line into a no-op). Plus, this method gives you no way to take advantages of Swift's closures, which would allow the observer to access local variables in the method that adds the observer and would eliminate the need to create a dedicated method to handle the event.A better way to do this is to use blocks. And NSNotificationCenter does include a block-based API:    NSNotificationCenter.defaultCenter().addObserverForName(MyNotificationItemAdded, object: nil, queue: nil) { note in      // ...    }This is much nicer, especially with Swift's trailing closure syntax. There are no method names to be looked up at runtime, we can refer to local variables in the method that registered the observer and we can perform small bits of logic in reaction to events without having to create and name dedicated methods.The catch comes in resource management. It's very important that an object remove its event observers when it's deallocated, or else NSNotificationCenter will try to invoke methods on invalid pointers.The traditional target-action method has the one advantage that we can easily handle this requirement with a single call in deinit:  deinit {    NSNotificationCenter.defaultCenter().removeObserver(self)  }With the block API, however, since there is no explicit target object, each call to addObserverForName returns "an opaque object to act as observer." So your observer class would need to track all of these objects and then remove them all from the notification center in deinit, which is a pain.In fact, the hassle of having to do bookkeeping on the observer objects almost cancels out the convenience of using the block API. Frustrated by this situation, I sat down and created a simple helper class, NotificationManager:class NotificationManager {  private var observerTokens: [AnyObject] = []  deinit {    deregisterAll()  }  func deregisterAll() {    for token in observerTokens {      NSNotificationCenter.defaultCenter().removeObserver(token)    }    observerTokens = []  }  func registerObserver(name: String!, block: (NSNotification! -> ()?)) {    let newToken = NSNotificationCenter.defaultCenter().addObserverForName(name, object: nil, queue: nil) {note in      block(note)      ()    }    observerTokens.append(newToken)  }    func registerObserver(name: String!, forObject object: AnyObject!, block: (NSNotification! -> ()?)) {    let newToken = NSNotificationCenter.defaultCenter().addObserverForName(name, object: object, queue: nil) {note in      block(note)      ()    }        observerTokens.append(newToken)  }}First, this simple class provides a Swift-specialized API around NSNotificationCenter.  It provides an additional convenience method without an object parameter (rarely used, in my experience) to make it easier to use trailing-closure syntax. But most importantly, it keeps track of the observer objects generated when observers are registered, and removes them when the object is deinit'd.A client of this class can simply keep a member variable of type NotificationManager and use it to register its observers. When the parent class is deallocated, the deinit method will automatically be called on its NotificationManager member variable, and its observers will be properly disposed of:class MyController: UIViewController {  private let notificationManager = NotificationManager()    override init() {    notificationManager.registerObserver(MyNotificationItemAdded) { note in      println("item added!")    }        super.init()  }    required init(coder: NSCoder) {    fatalError("decoding not implemented")  }}When the MyController instance is deallocated, its NotificationManager member variable will be automatically deallocated, triggering the call to deregisterAll that will remove the dead objects from NSNotificationCenter.In my apps, I add a notificationManager instance to my common UIViewController base class so I don't have to explicitly declare the member variable in all of my controller subclasses.Another benefit of using my own wrapper around NSNotificationCenter is that I can add useful functionality, like group observers: an observer that's triggered when any one of a group of notifications are posted:struct NotificationGroup {  let entries: [String]    init(_ newEntries: String...) {    entries = newEntries  }}extension NotificationManager {  func registerGroupObserver(group: NotificationGroup, block: (NSNotification! -> ()?)) {    for name in group.entries {      registerObserver(name, block: block)    }  }}This can be a great way to easily set up an event handler to run when, for example, an item is changed in any way at all:   let MyNotificationItemsChanged = NotificationGroup(      MyNotificationItemAdded,      MyNotificationItemDeleted,      MyNotificationItemMoved,      MyNotificationItemEdited    )    notificationManager.registerGroupObserver(MyNotificationItemsChanged) { note in      // ...    }

A taste of Cabalized Backpack

Planet Haskell - 40 min 4 sec ago
So perhaps you've bought into modules and modularity and want to get to using Backpack straightaway. How can you do it? In this blog post, I want to give a tutorial-style taste of how to program Cabal in the Backpack style. None of these examples are executable, because only some of this system is in […]

On CodeWorld and Haskell

Planet Haskell - 40 min 4 sec ago
I’ve been pouring a lot of effort into CodeWorld lately… and I wanted to write a sort of apology to the Haskell community.  Well, perhaps not an apology, because I believe I did the right thing.  But at the same time, I realize that decisions I’ve made haven’t been entirely popular among Haskell programmers.  I’d […]

Haskell Vectors and Sampling from a Categorical Distribution

Planet Haskell - 40 min 4 sec ago
Introduction Suppose we have a vector of weights which sum to 1.0 and we wish to sample n samples randomly according to these weights. There is a well known trick in Matlab / Octave using sampling from a uniform distribution. … Continue reading →

Dylan: the harsh realities of the market

Planet Haskell - 40 min 4 sec ago
So, this is a little case study.I did everything for Dylan. And when I say everything, I mean everything.  Here's my resumé:I got excited about Dylan as a user, and I used it. I bought an old Mac that I don't ever remember the designation for, it's so '90's old, and got the floppies for the Dylan IDE from Apple research.I'm not joking.I integrated Dylan into my work at work, building an XML parser then open-sourcing it to the community under the (then) non-restrictive license. I think mine was the only XML parser that was industrial-strength for Dylan. Can't claim originality: I ported over the Common-LISP one, but it was a lot of (fun) work.I made improvements to the gwydion-dylan compiler, including some library documentation (you can see my name right there, right in the compiler code), including some library functionality, did I work on the compiler itself? The Dylan syntax extensions or type system? I don't recall; if not in those places, I know I've looked at those guts: I had my fingers all over parts of the compiler.I was in the Dylan compiler code. For you ll-types ('little language') that's no big deal.But ask a software developer in industry if they've ever been in their compiler code. I have, too: I've found bugs in Java Sun-compiler that I fixed locally and reported up the chain.I taught a course at our community college on Dylan. I had five students from our company that made satellite mission software.I effing had commercial licenses bought when the boss asked me: what do we have to do to get this (my system) done/integrated into the build. I put my job on the line, for Dylan. ... The boss bought the licenses: he'd rather spend the $x than spending six weeks to back-port down to Java or C++.I built a rule-based man-power scheduling system that had previously took three administrative assistants three days each quarter to generate. My system did it, and printed out a PDF in less than one second. I sold it, so that means I started a commercial company and sold my software.I sold commercial Dylan software. That I wrote. Myself. And sold. Because people bought it. Because it was that good.Hells yeah.Question: what more could I have done?I kept Dylan alive for awhile. In industry. For real.So why is Dylan dead?That's not the question.Or, that question is answered over and over and over again.Good languages, beautiful languages, right-thing languages languish and die all the time.Dylan was the right-thing, and they (Apple) killed it in the lab, and for a reason.Who is Dylan for?That's not the question either. Because you get vague, general, useless answers.The question is to ask it like Paul Graham answered it for LISP.Lisp is a pointless, useless, weird language that nobody uses.But Paul and his partner didn't care. They didn't give a ...Something.... what anybody else thought. They knew that this language, the language they loved, was built and designed and made for them. Just them and only them, because the only other people who were using it were college kids on comp.lang.lisp asking for the answers for problem-set 3 on last night's homework.That's what Lisp was good for: nothing.That's who Lisp was good for: nobody.Same exact scenario for Erlang. Exactly the same. Erlang was only good for Joe Armstrong and a couple of buddies/weirdos like him, you know: kooks, who believed that Erlang was the right-thing for what they were doing, because they were on a mission, see, and nothing nobody could say could stop them nor stand against them, and all who would rise up against them would fall.All.What made Lisp and Haskell and Erlang and Scala and Prolog (yes, Prolog, although you'll never hear that success story publicly, but $26M and three lives saved? Because of a Prolog system I wrote? And that's just one day in one month's report for data? I call that a success) work when nobody sane would say that these things would work?Well, it took a few crazy ones to say, no, not: 'say' that it would work, but would make it work with their beloved programming language come hell or high water or, worse: indifferent silence, or ridicule, or pity from the rest of the world.That is the lesson of perl and python and all these other languages. They're not good for anything. They suck. And they suck in libraries and syntax and semantics and weirdness-factor and everything.But two, not one, but at least two people loved that language enough to risk everything, and ...They lost.Wait. What?Did you think I was going to paint the rosy picture and lie to you and say 'they won'?Because they didn't.Who uses Lisp commercially? Or Haskell, except some fringers, or Scala or Clojure or Erlang or Smalltalk or Prolog... or Dylan.These languages are defined, right there in the dictionary.Erlang: see 'career wrecker.'Nobody uses those languages nor admits to even touching them with a 10-foot (3-meter) pole. I had an intern from college. 'Yeah, we studied this weird language called ML in Comp.sci. Nobody uses it.'She was blown away when I started singing ML's praises and what it can do.A meta-language, and she called it useless? Seriously?Because that's what the mainstream sees.Newsflash. I'm sorry. Dylan, Haskell, Idris: these aren't main-stream, and they never will be.Algebraic types? Dependent types? You'll never see them. They're too ... research-y. They stink of academe, which is: they stink of uselessness-to-industry. You'll be dead and buried to see them in this form, even after they discover the eternity elixir. Sorry.Or you'll see them in Visual Basic as a new Type-class form that only a few Microserfs use because they happened to have written those extensions. Everybody else?Nah.Here's how Dylan will succeed, right now.Bruce and I will put our heads together, start a company, and we'll code something. Not for anybody else to use and to love and to cherish, just for us, only for us, and it will blow out the effing doors, and we'll be bought out for $40M because our real worth is $127M.And the first thing that Apple will do, after they bought us, is to show us the door, then convert the code into Java. Or Swift. Or Objective-C, or whatever.And that's how we'll win.Not the $40M. Not the lecture series on 'How to Make Functional Programming Work in Industry for Real' afterwards at FLoC and ICFP conferences with fan-bois and -girls wanting to talk to us afterwards and ask us how they can get a job doing functional programming.Not that.We'll win because we made something in Dylan, and it was real, and it worked, and it actually did something for enough people that we can now go to our graves knowing that we did something once with our lives (and we can do it again and again, too: there's no upper limit on the successes you're allowed to have, people) that meant something to some bodies. And we did that. With Dylan.Nyaah!I've done that several times already, by my counting: the Prolog project, the Dylan project, the Mercury project, and my writing.I'm ready to do that, again.Because, actually, fundamentally, doing something in this world and for it ... there's nothing like it.You write that research paper, and I come up to you, waving it in your face, demanding you implement your research because I need it to do my job in Industry?I've done that to three professors so far. Effing changed their world-view in that moment. "What?" they said, to a person, "somebody actually wants to use this?" The look of bemused surprise on their faces?It was sad, actually, because they did write something that somebody out there (moiself) needed, but they never knew that what they were doing meant something.And it did.Effing change your world-view. Your job? Your research? Your programming language?That's status quo, and that's good and necessary and dulce and de leche (or decorum, I forget which).But get up out of the level you're at, and do something with it so that that other person, slouched in their chair, sits up and takes notice, and a light comes over their face and they say, 'Ooh! That does that? Wow!' and watch their world change, because of you and what you've done.Dylan is for nothing and for nobody.So is everything under the Sun, my friend.Put your hand to the plow, and with the sweat of your brow, make it yours for this specific thing.Regardless of the long hours, long months of unrewarded work, and regardless of the hecklers, naysayers, and concerned friends and parents, and regardless of the mountain of unpaid bills.You make it work, and you don't stop until it does.That's how I've won.Every time.

Introduction to Dependent Types: Haskell on Steroids

Planet Haskell - 40 min 4 sec ago
Posted on August 25, 2014 I’d like to start another series of blog posts. This time on something that I’ve wanted to write about for a while, dependent types. There’s a noticeable lack of accessible materials introducing dependent types at a high level aimed at functional programmers. That’s what this series sets out help fill. Therefore, if you’re a Haskell programmer and don’t understand something, it’s a bug! Please comment so I can help make this a more useful resource for you :) There are four parts to this series, each answering one question What are dependent types? What does a dependently typed language look like? What does it feel like to write programs with dependent types? What does it mean to “prove” something? So first things first, what are dependent types? Most people by now have heard the unhelpful quick answer A dependent type is a type that depends on a value, not just other types. But that’s not helpful! What does this actually look like? To try to understand this we’re going to write some Haskell code that pushes us as close as we can get to dependent types in Haskell. Kicking GHC in the Teeth Let’s start with the flurry of extensions we need {-# LANGUAGE DataKinds #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-} Now our first definition is a standard formulation of natural numbers data Nat = Z | S Nat Here Z represents 0 and S means + 1. So you should read S Z as 1, S (S Z) as 2 and so on and so on. If you’re having some trouble, this function to convert an Int to a Nat might help -- Naively assume n >= 0 toNat :: Int -> Nat toNat 0 = Z toNat n = S (toNat $ n - 1) We can use this definition to formulate addition plus :: Nat -> Nat -> Nat plus Z n = n plus (S n) m = S (plus n m) This definition proceeds by “structural induction”. That’s a scary word that pops up around dependent types. It’s not all that complicated, all that it means is that we use recursion only on strictly smaller terms. There is a way to formally define smaller, if a term is a constructor applied to several (recursive) arguments. Any argument to the constructor is strictly smaller than the original terms. In a strict language if we restrict ourselves to only structural recursion we’re guaranteed that our function will terminate. This isn’t quite the case in Haskell since we have infinite structures. toInt :: Nat -> Int toInt (S n) = 1 + toInt n toInt Z = 0 bigNumber = S bigNumber main = print (toInt bigNumber) -- Uh oh! Often people will cheerfully ignore this part of Haskell when talking about reasoning with Haskell and I’ll stick to that tradition (for now). Now back to the matter at hand. Since our definition of Nat is quite straightforward, it get’s promoted to the kind level by DataKinds. Now we can “reflect” values back up to this new kind with a second GADTed definition of natural numbers. data RNat :: Nat -> * where RZ :: RNat Z RS :: RNat n -> RNat (S n) Now, let’s precisely specify the somewhat handwavy term “reflection”. I’m using it in the imprecise sense meaning that we’ve lifted a value into something isomorphic at the type level. Later we’ll talk about reflection precisely mean lifting a value into the type level. That’s currently not possible since we can’t have values in our types! What on earth could that be useful for? Well with this we can do something fancy with the definition of addition. type family Plus n m :: Nat where Plus Z n = n Plus (S n) m = S (Plus n m) Now we’ve reflected our definition of addition to the type family. More than that, what we’ve written above is fairly obviously correct. We can now force our value level definition of addition to respect this type family plus' :: RNat n -> RNat m -> RNat (Plus n m) plus' RZ n = n plus' (RS n) m = RS (plus' n m) Now if we messed up this definition we’d get a type error! plus' :: RNat n -> RNat m -> RNat (Plus n m) plus' RZ n = n plus' (RS n) m = plus' n m -- Unification error! n ~ S n Super! We know have types that express strict guarantees about our program. But how useable is this? To put it to the test, let’s try to write some code that reads to integers for standard input and prints their sum. We can easily do this with our normal plus readNat :: IO Nat readNat = toNat <$> readLn main :: IO () main = plus <$> readNat <*> readNat Easy as pie! But what about RNat, how can we convert a Nat to an RNat? Well we could try something with type classes I guess class Reify a where type N reify :: a -> RNat N But wait, that doesn’t work since we can only have once instance for all Nats. What if we did the opposite class Reify (n :: Nat) where nat :: RNat n -> Nat This let’s us go in the other direction.. but that doesn’t help us! In fact there’s no obvious way to propagate runtime values back into the types. We’re stuck. GHC with Iron Dentures Now, if we could add some magical extension to GHC could we write something like above program? Yes of course! The key idea is to not reflect up our types with data kinds, but rather just allow the values to exist in the types on their own. For these I propose two basic ideas A special reflective function type Lifting expressions into types For our special function types, we allow the return type to use the supplied value. These are called pi types. We’ll give this the following syntax (x :: A) -> B x Where A :: * and B :: A -> * are some sort of type. Notice that that A in B’s kind isn’t the data kind promoted version, but just the goodness to honest normal value. Now in order to allow B to actually make use of it’s supplied value, our second idea let’s normal types be indexed on values! Just like how GADTs can be indexed on types. We’ll call these GGADTs. So let’s define a new version of RNat data RNat :: Nat -> * where RZ :: RNat Z RS :: RNat n -> RNat (S n) This looks exactly like what we had before, but our semantics are different now. Those Z’s and S’s are meant to represent actual values, not members of some kind. There’s no promoting types to singleton kinds anymore, just plain old values being held in fancier types. Because we can depend on normal values, we don’t even have to use our simple custom natural numbers. data RInt :: Int -> * where RZ :: RInt 0 RS :: RInt n -> RInt (1 + n) Notice that we allowed our types to call functions, like +. This can potentially be undecidable, something that we’ll address later. Now we can write our function with a combination of these two ideas toRInt :: (n :: Int) -> RInt n toRInt 0 = RZ toRInt n = RS (toRInt $ n - 1) Notice how we used pi types to change the return type dependent on the input value. Now we can feed this any old value, including ones we read from standard input. main = print . toInt $ plus' <$> fmap toRInt readLn <*> fmap toRInt readLn Now, one might wonder how the typechecker could possibly know how to handle such things, after all how could it know what’ll be read from stdin! The answer is that it doesn’t. When a value is reflected to the type level we can’t do anything with it. For example, if we had a type like (n :: Int) -> (if n == 0 then Bool else ()) Then we would have to pattern match on n at the value level to propagate information about n back to the type level. If we did something like foo :: (n :: Int) -> (if n == 0 then Bool else ()) foo n = case n of 0 -> True _ -> () Then the typechecker would see that we’re matching on n, so if we get into the 0 -> ... branch then n must be 0. It can then reduce the return type to if 0 == 0 then Bool else () and finally Bool. A very important thing to note here is that the typechecker doesn’t evaluate the program. It’s examining the function in isolation of all other values. This means we sometimes have to hold its hand to ensure that it can figure out that all branches have the correct type. This means that when we use pi types we often have to pattern match on our arguments in order to help the typechecker figure out what’s going on. To make this clear, let’s play the typechecker for this function. I’m reverting to the Nat type since it’s nicer for pattern matching. toRNat :: (n :: Nat) -> RNat n toRNat Z = RZ -- We know that n is `Z` in this branch toRNat (S n) = RS (toRNat n {- This has the type RNat n' -}) p :: (n :: Nat) -> (m :: Int) -> RNat (plus n m) p Z m = toRNat m p (S n) m = RS (toRNat n m) First the type checker goes through toRNat. In the first branch we have n equals Z, so RZ trivially typechecks. Next we have the case S n. We know that toRNat n has the type RNat n' by induction We also know that S n' = n. Therefore RS builds us a term of type RNat n. Now for p. We start in much the same manner. if we enter the p Z m case we know that n is Z. we can reduce plus n m since plus Z m is by definition equal to m Look at the definition of plus to confirm this). We know how to produce RNat m easily since we have a function toRNat :: (n :: Nat) -> RNat n. We can apply this to m and the resulting term has the type RNat m. In the RS case we know that we’re trying to produce a term of type RNat (plus (S n) m). Now since we know that the constructor for the first argument of plus, we can reduce plus (S n) m to S (plus n m) by the definition of plus. We’re looking to build a term of type plus n m and that’s as simple as a recursive call. From here we just need to apply RS to give us S (plus n m) As we previously noted S (plus n m) is equal to plus (S n) m Notice how as we stepped through this as the typechecker we never needed to do any arbitrary reductions. We only ever reduce definitions when we have the outer constructor (WHNF) of one of the arguments. While I’m not actually proposing adding {-# LANGUAGE PiTypes #-} to GHC, it’s clear that with only a few orthogonal editions to system F we can get some seriously cool types. Wrap Up Believe or not we’ve just gone through two of the most central concepts in dependent types Indexed type families (GGADTs) Dependent function types (Pi types) Not so bad was it? :) From here we’ll look in the next post how to translate our faux Haskell into actual Agda code. From there we’ll go through a few more detailed examples of pi types and GGADTs by poking through some of the Agda standard library. Thanks for reading, I must run since I’m late for class. It’s an FP class ironically enough. /* * * CONFIGURATION VARIABLES: EDIT BEFORE PASTING INTO YOUR WEBPAGE * * */ var disqus_shortname = 'codeco'; // required: replace example with your forum shortname /* * * DON'T EDIT BELOW THIS LINE * * */ (function() { var dsq = document.createElement('script'); dsq.type = 'text/javascript'; dsq.async = true; dsq.src = '//' + disqus_shortname + '.disqus.com/embed.js'; (document.getElementsByTagName('head')[0] || document.getElementsByTagName('body')[0]).appendChild(dsq); })(); Please enable JavaScript to view the comments powered by Disqus. comments powered by Disqus 2014-08-25T00:00:00Z
Syndicate content