News aggregator

FP Complete: School of Haskell 2.0

Planet Haskell - Mon, 05/04/2015 - 11:00am

As announced by Michael Snoyman a couple weeks ago, we are going to be releasing an open source version of the School of Haskell! The SoH provides interactive documentation and tutorials for newcomers and advanced haskellers alike. This interactivity comes in the form of editable code, inline in the webpage, letting you try things out as you learn them.

We are dedicated to supporting the community with excellent Haskell tools and infrastructure. As this is a community project, I'm writing this post to explain our plans, and to ask for feedback and ideas.

We are focused on eliminating any obstacles which have historically discouraged or prevented people from contributing to the School of Haskell. In particular, here are the changes we're planning:

  • Open Source! We'll encourage community participation on improving the service, via the bug tracker and pull requests. Anyone will be free to host their own version of the site.

  • Creative Commons license! While our old license was not intended to be restrictive, it turned away some potential contributors.

  • Git! Git will be used to store the SoH markdown pages. The core school repo will be hosted on GitHub. This means that editing, history, organization, and collaboration will all be based on a system that many people understand well.

  • Interactive code on any website! Any website will be able to include editable and runnable Haskell code. All you'll need to do is include a script tag like <script src="https://www.schoolofhaskell.com/soh.js">. When run, this script will replace code divs with the editor. This means that haddocks could potentially have examples that you can play with directly in the browser!

Questions for the Community

Please help us guide this work to best serve you and the community!

  • Should all user content be licensed under the Creative Commons license? One option is to relicense all user content when it gets moved to the soh-migration-snapshot repo. Another option is to add a footnote to each page noting that its license is the SoH 1.0 license. After users migrate to their own repo, they are free to remove this footnote.

  • Should the markdown format change? We're considering switching to CommonMark, but perhaps having a stable format for migration is more important?

  • Does the system of git repos sound good (it's described below)? One issue is that it will require a little bit of setup for users to continue editing their SoH content. Is this acceptable to folks? Should we seek to streamline the process via the GitHub API?

  • Any other ideas? We've already got a fair amount of work cut out for us, but we'd love to hear more ideas, particularly of the low-hanging-fruit variety.

Plan for the Editor Service

The editor service will allow Haskell to be edited in the browser and run on the server. This service is independent of the markdown rendering service, described below.

Editor Features

Our plan is to support the following features in the SoH code editor / runner:

  • Standard input / output will use a console emulator in the browser. This means that things like ncurses apps will work!

  • GHCI support. Initially this will likely be a bit of a hack, directly running ghci rather than using ide-backend.

  • Type information will be available for sub-expressions, simply by selecting a sub-expression in the code.

  • -fdefer-type-errors will be used by default. This will likely be setup such that type errors still prevent running the code, but using this flag this means that type info is still yielded by GHC.

  • Support for looking up the haddocks associated with an identifier. Info from GHC will be used for this, and open the results in an IFrame.

  • Go-to-definition will tell you where an identifier is bound.

  • The capability to serve websites. This will work by detecting of when the user's code is acting as an HTTP server, and opening an IFrame / separate window for interacting with it.

This new version is going to be offering quite a lot of information! In order to have somewhere to put it all, there will be a tabbed info pane at the bottom of the snippet (much like the pane at the bottom of FPHC).

Implementation Changes

We've learned a lot about writing this sort of application since the initial creation of the School of Haskell. In particular, we're planning on making the following changes, although things aren't quite set in stone yet:

  • Using GHCJS instead of Fay. Back when the SoH was created, GHCJS wasn't quite ready, and so Fay was picked. Fay was quite nice for the task, but having full-blown GHC Haskell is even nicer.

  • Using Docker for managing Linux containers and images.

  • Using Ace instead of CodeMirror. Our experience with using Ace for stackage-view was quite positive. This will address a number of open bugs, and allow us to reuse some existing GHCJS bindings to Ace.

  • Using websockets instead of HTTP requests. Due to usage of Amazon's Elastic Load Balancer, in the past we couldn't use websockets.

  • The protocol will likely be based on ide-backend-client.

Plan for the Markdown Rendering Service

The markdown rendering service allows rendering of SoH markdown into documentation / tutorials which contain active Haskell code. We hope to make this largely backwards compatible with the old markdown format, as we'll be migrating content from the old site.

Our plan is to have a central GitHub repo which hosts the main "school" section. For example, it might be placed at https://github.com/schoolofhaskell/school. This will be a central place to put Haskell educational content, and we will heartily encourage pull requests.

You'll also be able to give the server a URL to your own publicly accessible git repo. The contents of this repo will then be served as SoH pages, possibly with a URL like https://schoolofhaskell.com/user/user-name/tutorial-name. To facilitate the migration, we'll provide a tarball of your current SoH pages, in a form readable by the new implementation.

All existing SoH URLs at https://fpcomplete.com will redirect to https://schoolofhaskell.com. In order to do this, we need to migrate the content to the new system. The current plan for this is to have a repo, possibly at https://github.com/schoolofhaskell/soh-migration-snapshot, which will be used as a fallback for users who haven't yet specified a repo for their account.

Categories: Offsite Blogs

ANN: Important lambabot update (5.0.2.1 release)

haskell-cafe - Sun, 05/03/2015 - 3:27pm
Hi, I've just released lambdabot-5.0.2.1 which plugs an embarrassing security hole in the < at >check command; if you are running lambdabot as an IRC bot, you should upgrade! Generally, lambdabot relies on SafeHaskell and not running user-supplied IO actions for safety. This is unlikely to be bullet-proof, so it's advisable to sandbox mueval. However, the < at >check command violated this basic principle, and allowed running arbitrary IO actions. This is now fixed by using the (new) QuickCheck-safe package that only uses unsafePerformIO for the specific purposes of catching exceptions and generating the initial seed for random number generation. Thanks to benzfr on Freenode for finding this! There are a few minor changes. Notably, we now ship compiler-specific versions of Pristine.hs so that lambdabot runs out of the box on both ghc-7.6.3 and ghc-7.8.3 (ghc-7.10.1 still needs some work.) and the dict plugin no longer supports looking up several words at once. Cheers, Bertram P.S. As I just realized, I forgot to
Categories: Offsite Discussion

Keegan McAllister: Modeling garbage collectors with Alloy: part 1

Planet Haskell - Sun, 05/03/2015 - 3:21pm

Formal methods for software verification are usually seen as a high-cost tool that you would only use on the most critical systems, and only after extensive informal verification. The Alloy project aims to be something completely different: a lightweight tool you can use at any stage of everyday software development. With just a few lines of code, you can build a simple model to explore design issues and corner cases, even before you've started writing the implementation. You can gradually make the model more detailed as your requirements and implementation get more complex. After a system is deployed, you can keep the model around to evaluate future changes at low cost.

Sounds great, doesn't it? I have only a tiny bit of prior experience with Alloy and I wanted to try it out on something more substantial. In this article we'll build a simple model of a garbage collector, visualize its behavior, and fix some problems. This is a warm-up for exploring more complex GC algorithms, which will be the subject of future articles.

I won't describe the Alloy syntax in full detail, but you should be able to follow along if you have some background in programming and logic. See also the Alloy documentation and especially the book Software Abstractions: Logic, Language, and Analysis by Daniel Jackson, which is a very practical and accessible introduction to Alloy. It's a highly recommended read for any software developer.

You can download Alloy as a self-contained Java executable, which can do analysis and visualization and includes an editor for Alloy code.

The model

We will start like so:

open util/ordering [State]

sig Object { }
one sig Root extends Object { }

sig State {
pointers: Object -> set Object,
collected: set Object,
}

The garbage-collected heap consists of Objects, each of which can point to any number of other Objects (including itself). There is a distinguished object Root which represents everything that's accessible without going through the heap, such as global variables and the function call stack. We also track which objects have already been garbage-collected. In a real implementation these would be candidates for re-use; in our model they stick around so that we can detect use-after-free.

The open statement invokes a library module to provide a total ordering on States, which we will interpret as the progression of time. More on this later.

Relations

In the code that follows, it may look like Alloy has lots of different data types, overloading operators with total abandon. In fact, all these behaviors arise from an exceptionally simple data model:

Every value is a relation; that is, a set of tuples of the same non-zero length.

When each tuple has length 1, we can view the relation as a set. When each tuple has length 2, we can view it as a binary relation and possibly as a function. And a singleton set is viewed as a single atom or tuple.

Since everything in Alloy is a relation, each operator has a single definition in terms of relations. For example, the operators . and [] are syntax for a flavor of relational join. If you think of the underlying relations as a database, then Alloy's clever syntax amounts to an object-relational mapping that is at once very simple and very powerful. Depending on context, these joins can look like field access, function calls, or data structure lookups, but they are all described by the same underlying framework.

The elements of the tuples in a relation are atoms, which are indivisible and have no meaning individually. Their meaning comes entirely from the relations and properties we define. Ultimately, atoms all live in the same universe, but Alloy gives "warnings" when the type system implied by the sig declarations can prove that an expression is always the empty relation.

Here are the relations implied by our GC model, as tuple sets along with their types:

Object: {Object} = {O1, O2, ..., Om}
Root: {Root} = {Root}
State: {State} = {S1, S2, ..., Sn}

pointers: {(State, Object, Object)}
collected: {(State, Object)}

first: {State} = {S1}
last: {State} = {Sn}
next: {(State, State)} = {(S1, S2), (S2, S3), ..., (S(n-1), Sn)}

The last three relations come from the util/ordering library. Note that a sig implicitly creates some atoms.

Dynamics

The live objects are everything reachable from the root:

fun live(s: State): set Object {
Root.*(s.pointers)
}

*(s.pointers) constructs the reflexive, transitive closure of the binary relation s.pointers; that is, the set of objects reachable from each object.

Of course the GC is only part of a system; there's also the code that actually uses these objects, which in GC terminology is called the mutator. We can describe the action of each part as a predicate relating "before" and "after" states.

pred mutate(s, t: State) {
t.collected = s.collected
t.pointers != s.pointers
all a: Object - t.live |
t.pointers[a] = s.pointers[a]
}

pred gc(s, t: State) {
t.pointers = s.pointers
t.collected = s.collected + (Object - s.live)
some t.collected - s.collected
}

The mutator cannot collect garbage, but it can change the pointers of any live object. The GC doesn't touch the pointers, but it collects any dead object. In both cases we require that something changes in the heap.

It's time to state the overall facts of our model:

fact {
no first.collected
first.pointers = Root -> (Object - Root)
all s: State - last |
let t = s.next |
mutate[s, t] or gc[s, t]
}

This says that in the initial state, no object has been collected, and every object is in the root set except Root itself. This means we don't have to model allocation as well. Each state except the last must be followed by a mutator step or a GC step.

The syntax all x: e | P says that the property P must hold for every tuple x in e. Alloy supports a variety of quantifiers like this.

Interacting with Alloy

The development above looks nice and tidy — I hope — but in reality, it took a fair bit of messing around to get to this point. Alloy provides a highly interactive development experience. At any time, you can visualize your model as a collection of concrete examples. Let's do that now by adding these commands:

pred Show {}
run Show for 5

Now we select this predicate from the "Execute" menu, then click "Show". The visualizer provides many options to customise the display of each atom and relation. The config that I made for this project is "projected over State", which means you see a graph of the heap at one moment in time, with forward/back buttons to reach the other States.

After clicking around a bit, you may notice some oddities:

The root isn't a heap object; it represents all of the pointers that are reachable without accessing the heap. So it's meaningless for an object to point to the root. We can exclude these cases from the model easily enough:

fact {
all s: State | no s.pointers.Root
}

(This can also be done more concisely as part of the original sig.)

Now we're ready to check the essential safety property of a garbage collector:

assert no_dangling {
all s: State | no (s.collected & s.live)
}

check no_dangling for 5 Object, 10 State

And Alloy says:

Executing "Check no_dangling for 5 Object, 10 State"
...
8338 vars. 314 primary vars. 17198 clauses. 40ms.
Counterexample found. Assertion is invalid. 14ms.

Clicking "Counterexample" brings up the visualization:

Whoops, we forgot to say that only pointers to live objects can be stored! We can fix this by modifying the mutate predicate:

pred mutate(s, t: State) {
t.collected = s.collected
t.pointers != s.pointers
all a: Object - t.live |
t.pointers[a] = s.pointers[a]

// new requirement!
all a: t.live |
t.pointers[a] in s.live
}

With the result:

Executing "Check no_dangling for 5 Object, 10 State"
...
8617 vars. 314 primary vars. 18207 clauses. 57ms.
No counterexample found. Assertion may be valid. 343ms.

SAT solvers and bounded model checking

"May be" valid? Fortunately this has a specific meaning. We asked Alloy to look for counterexamples involving at most 5 objects and 10 time steps. This bounds the search for counterexamples, but it's still vastly more than we could ever check by exhaustive brute force search. (See where it says "8617 vars"? Try raising 2 to that power.) Rather, Alloy turns the bounded model into a Boolean formula, and feeds it to a SAT solver.

This all hinges on one of the weirdest things about computing in the 21st century. In complexity theory, SAT (along with many equivalents) is the prototypical "hardest problem" in NP. Why do we intentionally convert our problem into an instance of this "hardest problem"? I guess for me it illustrates a few things:

  • The huge gulf between worst-case complexity (the subject of classes like NP) and average or "typical" cases that we encounter in the real world. For more on this, check out Impagliazzo's "Five Worlds" paper.

  • The fact that real-world difficulty involves a coordination game. SAT solvers got so powerful because everyone agrees SAT is the problem to solve. Standard input formats and public competitions were a key part of the amazing progress over the past decade or two.

Of course SAT solvers aren't quite omnipotent, and Alloy can quickly get overwhelmed when you scale up the size of your model. Applicability to the real world depends on the small scope hypothesis:

If an assertion is invalid, it probably has a small counterexample.

Or equivalently:

Systems that fail on large instances almost always fail on small instances with similar properties.

This is far from a sure thing, but it already underlies a lot of approaches to software testing. With Alloy we have the certainty of proof within the size bounds, so we don't have to resort to massive scale to find rare bugs. It's difficult (but not impossible!) to imagine a GC algorithm that absolutely cannot fail on fewer than 6 nodes, but is buggy for larger heaps. Implementations will often fall over at some arbitrary resource limit, but algorithms and models are more abstract.

Conclusion

It's not surprising that our correctness property

all s: State | no (s.collected & s.live)

holds, since it's practically a restatement of the garbage collection "algorithm":

t.collected = s.collected + (Object - s.live)

Because reachability is built into Alloy, via transitive closure, the simplest model of a garbage collector does not really describe an implementation. In the next article we'll look at incremental garbage collection, which breaks the reachability search into small units and allows the mutator to run in-between. This is highly desirable for interactive or real-time apps; it also complicates the algorithm quite a bit. We'll use Alloy to uncover some of these complications.

In the meantime, you can play around with the simple GC model and ask Alloy to visualize any scenario you like. For example, we can look at runs where the final state includes at least 5 pointers, and at least one collected object:

pred Show {
#(last.pointers) >= 5
some last.collected
}

run Show for 5

Thanks for reading! You can find the code in a GitHub repository which I'll update if/when we get around to modeling more complex GCs.

Categories: Offsite Blogs

Attempt at getting primes

Haskell on Reddit - Sun, 05/03/2015 - 2:59pm

Alright so I just started learning (as of an hour ago I ended up reading about scanl etc in Learn You A Haskell) and I tried to write something that would get all the primes under 100. I suppose there are way better/quicker ways to figure out those primes but I'm just curious if the way I typed it out is fine.

It uses 'trial division'.

So here's the code:

module Main where import Data.Fixed getPrimes :: [Float] getPrimes = takeWhile (<100) (filter checkIfPrime [2.0,3.0..]) checkIfPrime :: Float -> Bool checkIfPrime x | x == 2 || x == 3 = True | (x `mod'` 2 == 0) || (x `mod'` 3 == 0) = False | 0.0 `elem` map (mod' x) numberList = False | otherwise = True where numberList = numbersToCheck (sqrt x) numbersToCheck :: Float -> [Float] numbersToCheck x = takeWhile (<=x) (5 : 7 : map (+6) (numbersToCheck x)) main :: IO() main = print getPrimes submitted by Piegie
[link] [17 comments]
Categories: Incoming News

Paid - Looking for help troubleshooting a Haskell program a friend wrote for me.

Haskell on Reddit - Sun, 05/03/2015 - 11:44am

Hi everyone,

Recently a friend wrote a small program for me to help me with my small business. Unfortunately, we ran out of time before I could put it through all its paces and he left for a several month trip abroad. I need some help troubleshooting what I think are just the last couple of stumbling blocks.

In my admittedly non-expert opinion, I don't think it would take more than a couple hours to work out. It could be an easy way to make a $100 for a sufficiently skilled programmer.

The program records user preferences through a web form, compares against a database of inventory (games), matches the best choice (based on the submitted preferences), and generates shipping/fulfillment information as a result. All the information is recorded to and stored in Excel.

Everything seems to function properly except for the web submitted preferences being written to the spreadsheet of user information, though that is the first step in the process.

If you're interested in taking a crack at it, direct message me and I'll send you a link to the program's github.

Thanks!

submitted by HamillianActor
[link] [14 comments]
Categories: Incoming News

Implement hashmap using list

Haskell on Reddit - Sun, 05/03/2015 - 11:24am

Are there some functions that can be used when implementing hashmap using list? For example , a map :: [(Char, Int)] If I want to check whether there is a key 'p' in this map, currently I defined a recursion function to check. Are there any nice functions similar to this?

submitted by Arcovitcher
[link] [5 comments]
Categories: Incoming News

CF STUDENT POSTERS for Innovations'15 (No registration fees), Dubai, November 01-03, 2015

General haskell list - Sun, 05/03/2015 - 10:17am
From: Nabeel Al-Qirim Sent: Monday, March 09, 2015 3:23 PM To: haskell< at >haskell.org; Haskell Cafe Subject: CF STUDENT POSTERS for Innovations'15 (No registration fees), Dubai, November 01-03, 2015 CF STUDENT POSTERS for Innovations'15 (No registration fees), Dubai, November 01-03, 2015 IIT’15: The 11th International Conference on Innovations in Information Technology 2015 URL: http://www.it-innovations.ae/iit2015/posters.html The IIT’15 Student Poster and Demos Committee invites all undergraduate and graduate students to submit an extended (2 pages max.) abstract and to display it as a poster during the IIT’15. The poster topic should fall within the conference’s theme and tracks. SUBMISSION Extended abstracts should be sent to Dr. Nabeel Al-Qirim at nalqirim< at >uaeu.ac.ae. All students are encouraged to review their abstracts with their faculty advisers prior to submission. All accepted abstracts will be published by the IIT’15 proceedings. IMPORTANT DATES -Student
Categories: Incoming News

BER MetaOCaml -- an OCaml dialect for multi-stage programming

Lambda the Ultimate - Sun, 05/03/2015 - 10:16am
BER MetaOCaml -- an OCaml dialect for multi-stage programming
Oleg Kiselyov
2010-2015-

BER MetaOCaml is a conservative extension of OCaml for ``writing programs that generate programs''. BER MetaOCaml adds to OCaml the type of code values (denoting ``program code'', or future-stage computations), and two basic constructs to build them: quoting and splicing. The generated code can be printed, stored in a file -- or compiled and linked-back to the running program, thus implementing run-time code optimization. A well-typed BER MetaOCaml program generates only well-scoped and well-typed programs: The generated code shall compile without type errors. The generated code may run in the future but it is type checked now. BER MetaOCaml is a complete re-implementation of the original MetaOCaml by Walid Taha, Cristiano Calcagno and collaborators.

Introduction to staging and MetaOCaml

The standard example of meta-programming -- the running example of A.P.Ershov's 1977 paper that begat partial evaluation -- is the power function, computing x^n. In OCaml:

let square x = x * x let rec power n x = if n = 0 then 1 else if n mod 2 = 0 then square (power (n/2) x) else x * (power (n-1) x)

[...]

In MetaOCaml, we may also specialize the power function to a particular value n, obtaining the code which will later receive x and compute x^n. We re-write power n x annotating expressions as computed `now' (when n is known) or `later' (when x is given).

let rec spower n x = if n = 0 then .<1>. else if n mod 2 = 0 then .<square .~(spower (n/2) x)>. else .<.~x * .~(spower (n-1) x)>.;; A brief history of (BER) MetaOCaml

As MetaOCaml was being developed, new versions of the mainline OCaml were released with sometimes many fixes and improvements. The MetaOCaml team tracked new OCaml releases and merged the changes into MetaOCaml. (The MetaOCaml version number has as its base OCaml's release version.) The merge was not painless. For example, any new function in the OCaml compiler that dealt with Parsetree (AST) or Typedtree has to be modified to handle MetaOCaml extensions to these data structures. The merge process became more and more painful as the two languages diverged. For instance, native code compilation that first appeared in MetaOCaml 3.07 relied on SCaml, a large set of patches to OCaml by malc at pulsesoft.com to support dynamic linking. OCaml 3.08 brought many changes that were incompatible with SCaml. Therefore, in MetaOCaml 3.08 the native compilation mode was broken. The mode was brought back in the Summer 2005, by re-engineering the SCaml patch and implementing the needed parts of dynamic linking without any modification to the OCaml code. The revived native compilation has survived through the end.

[...]

BER MetaOCaml has been re-structured to minimize the amount of changes to the OCaml type-checker and to separate the `kernel' from the `user-level'. The kernel is a set of patches and additions to OCaml, responsible for producing and type-checking code values. The processing of built code values -- so-called `running' -- is user-level. Currently the user-level metalib supports printing, type-checking, and byte-compiling and linking of code values. Users have added other ways of running the code, for example, compiling it to machine code, C or LLVM -- without any need to hack into (Meta)OCaml or even recompile it.

[...]

By relying on attributes, the feature of OCaml 4.02, BER N102 has become much closer integrated with OCaml. It is instructive to compare the amount of changes BER MetaOCaml makes to the OCaml distribution. The previous version (BER N101) modified 32 OCaml files. The new BER N102 modifies only 7 (that number could be further reduced to only 2; the only file with nontrivial modifications is typing/typecore.ml). It is now a distinct possibility that -- with small hooks that may be provided in the future OCaml versions -- MetaOCaml becomes just a regular library or a plug-in, rather being a fork.

Categories: Offsite Discussion

apfelmus: GUI - Release of the threepenny-gui library, version 0.6.0.1

Planet Haskell - Sun, 05/03/2015 - 9:33am

I am pleased to announce release of threepenny-gui version 0.6, a cheap and simple library to satisfy your immediate GUI needs in Haskell.

Want to write a small GUI thing but forgot to sacrifice to the giant rubber duck in the sky before trying to install wxHaskell or Gtk2Hs? Then this library is for you! Threepenny is easy to install because it uses the web browser as a display.

The library also has functional reactive programming (FRP) built-in, which makes it a lot easier to write GUI application without getting caught in spaghetti code. For an introduction to FRP, see for example my slides from a tutorial I gave in 2012. (The API is slightly different in Reactive.Threepenny.)

In version 0.6, the communication with the web browser has been overhauled completely. On a technical level, Threepenny implements a HTTP server that sends JavaScript code to the web browser and receives JSON data back. However, this is not the right level of abstraction to look at the problem. What we really want is a foreign function interface for JavaScript, i.e. we want to be able to call arbitrary JavaScript functions from our Haskell code. As of this version, Threepenny implements just that: The module Foreign.JavaScript gives you the essential tools you need to interface with the JavaScript engine in a web browser, very similar to how the module Foreign and related modules from the base library give you the ability to call C code from Haskell. You can manipulate JavaScript objects, call JavaScript functions and export Haskell functions to be called from JavaScript.

However, the foreign calls are still made over a HTTP connection (Threepenny does not compile Haskell code to JavaScript). This presents some challenges, which I have tried to solve with the following design choices:

  • Garbage collection. I don’t know any FFI that has attemped to implement cross-runtime garbage collection. The main problem are cyclic references, which happen very often in a GUI setting, where an event handler references a widget, which in turn references the event handler. In Threepenny, I have opted to leave garbage collection entirely to the Haskell side, because garbage collectors in current JavaScript engines are vastly inferior to what GHC provides. The module Foreign.RemotePtr gives you the necessary tools to keep track of objects on the JavaScript (“remote”) side where necessary.

  • Foreign exports. Since the browser and the HTTP server run concurrently, there is no shared “instruction pointer” that keeps track of whether you are currently executing code on the Haskell side or the JavaScript side. I have chosen to handle this in the following way: Threepenny supports synchronous calls to JavaScript functions, but Haskell functions can only be called as “asynchronous event handlers” from the JavaScript side, i.e. the calls are queued and they don’t return results.

  • Latency, fault tolerance. Being a GUI library, Threepenny assumes that both the browser and the Haskell code run on localhost, so all network problems are ignored. This is definitely not the right way to implement a genuine web application, but of course, you can abuse it for writing quick and dirty GUI apps over your local network (see the Chat.hs example).

To see Threepenny in action, have a look at the following applications:

Daniel Austin’s FNIStash
Editor for Torchlight 2 inventories.
Chaddai’s CurveProject
Plotting curves for math teachers.

Get the library here:

Note that the API is still in flux and is likely to change radically in the future. You’ll have to convert frequently or develop against a fixed version.

Categories: Offsite Blogs

Meet some problem when installing Agda

haskell-cafe - Sat, 05/02/2015 - 9:48pm
Hi I want to use Agda on my computer and I follow the instruction http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.MacOSX However when I was using cabal install Agda to install agda, the terminal said The program cpphs version >=1.18.6 && <1.19 is required but the version found at /Users/XXXXXX/Library/Haskell/bin/cpphs is version 1.19 Do you have some idea how could i fix that problem? Zongzhe Yuan This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please send it back to me, and immediately delete it. Please do not use, copy or disclose the information contained in this message or in any attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham. This message has been checked for viruses but the contents of an attachment may still contain software viruses which could damage your computer system, you are advis
Categories: Offsite Discussion

ANN: applicative-fail-1.0.0

haskell-cafe - Sat, 05/02/2015 - 9:32pm
Hi guys, here is reworked applicative-fail http://hackage.haskell.org/package/applicative-fail-1.0.0 You can use it to e.g. parse requests in your web application, or in any other parse-like stuff. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe< at >haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Categories: Offsite Discussion

Start GHCI with a static library

haskell-cafe - Sat, 05/02/2015 - 4:24pm
Hi all, I have a Haskell library I'd like to load up in GHCI along with a statically linked C library (libblah.a) . Is there any way to do this? My Googling only turns up instructions on loading a shared library (libblah.so). Thanks! -deech _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe< at >haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Categories: Offsite Discussion

Roman Cheplyaka: Smarter validation

Planet Haskell - Sat, 05/02/2015 - 2:00pm

Today we’ll explore different ways of handling and reporting errors in Haskell. We shall start with the well-known Either monad, proceed to a somewhat less common Validation applicative, and then improve its efficiency and user experience.

The article contains several exercises that will hopefully help you better understand the issues that are being addressed here.

Running example {-# LANGUAGE GeneralizedNewtypeDeriving, KindSignatures, DataKinds, ScopedTypeVariables, RankNTypes, DeriveFunctor #-} import Text.Printf import Text.Read import Control.Monad import Control.Applicative import Control.Applicative.Lift (Lift) import Control.Arrow (left) import Data.Functor.Constant (Constant) import Data.Monoid import Data.Traversable (sequenceA) import Data.List (intercalate, genericTake, genericLength) import Data.Proxy import System.Exit import System.IO import GHC.TypeLits

Our running example will consist of reading a list of integer numbers from a file, one number per line, and printing their sum.

Here’s the simplest way to do this in Haskell:

printSum1 :: FilePath -> IO () printSum1 path = print . sum . map read . lines =<< readFile path

This code works as expected for a well-formed file; however, if a line in the file can’t be parsed as a number, we’ll get unhelpful

Prelude.read: no parse Either monad

Let’s rewrite our function to be aware of possible errors.

parseNum :: Int -- line number (for error reporting) -> String -- line contents -> Either String Integer -- either parsed number or error message parseNum ln str = case readMaybe str of Just num -> Right num Nothing -> Left $ printf "Bad number on line %d: %s" ln str -- Print a message and exit die :: String -> IO () die msg = do hPutStrLn stderr msg exitFailure printSum2 :: FilePath -> IO () printSum2 path = either die print . liftM sum . sequence . zipWith parseNum [1..] . lines =<< readFile path

Now, upon reading a line that is not a number, we’d see something like

Bad number on line 2: foo

This is a rather standard usage of the Either monad, so I won’t get into details here. I’ll just note that there are two ways in which this version is different from the first one:

  1. We call readMaybe instead of read and, upon detecting an error, construct a helpful error message. For this reason, we keep track of the line number.
  2. Instead of throwing a runtime exception right away (using the error function), we return a pure Either value, and then combine these Eithers together using the Moand Either isntance.

The two changes are independent; there’s no reason why we couldn’t use error and get the same helpful error message. The exceptions emulated by the Either monad have the same semantics here as the runtime exceptions. The benefit of the pure formulation is that the semantics of runtime exceptions is built-in; but the semantics of the pure data is programmable, and we will take advantage of this fact below.

Validation applicative

You get a thousand-line file with numbers from your accountant. He asks you to sum them up because his enterprise software mysteriously crashes when trying to read it.

You accept the challenge, knowing that your Haskell program won’t let you down. The program tells you

Bad number on line 378: 12o0

— I see! Someone put o instead of zero. Let me fix it.

You locate the line 378 in your editor and replace 12o0 with 1200. Then you save the file, exit the editor, and re-run the program.

Bad number on line 380: 11i3

— Come on! There’s another similar mistake just two lines below. Except now 1 got replaced by i. If you told me about both errors from the beginning, I could fix them faster!

Indeed, there’s no reason why our program couldn’t try to parse every line in the file and tell us about all the mistakes at once.

Except now we can’t use the standard Monad and Applicative instances of Either. We need the Validation applicative.

The Validation applicative combines two Either values in such a way that, if they are both Left, their left values are combined with a monoidal operation. (In fact, even a Semigroup would suffice.) This allows us to collect errors from different lines.

newtype Validation e a = Validation { getValidation :: Either e a } deriving Functor instance Monoid e => Applicative (Validation e) where pure = Validation . Right Validation a <*> Validation b = Validation $ case a of Right va -> fmap va b Left ea -> either (Left . mappend ea) (const $ Left ea) b

The following example demonstrates the difference between the standard Applicative instance and the Validation one:

> let e1 = Left "error1"; e2 = Left " error2" > e1 *> e2 Left "error1" > getValidation $ Validation e1 *> Validation e2 Left "error1 error2"

A clever implementation of the same applicative functor exists inside the transformers package. Ross Paterson observes that this functor can be constructed as

type Errors e = Lift (Constant e)

(see Control.Applicative.Lift).

Anyway, let’s use this to improve our summing program.

printSum3 :: FilePath -> IO () printSum3 path = either (die . intercalate "\n") print . liftM sum . getValidation . sequenceA . map (Validation . left (\e -> [e])) . zipWith parseNum [1..] . lines =<< readFile path

Now a single invocation of the program shows all the errors it can find:

Bad number on line 378: 12o0 Bad number on line 380: 11i3

Exercise. Could we use Writer [String] to collect error messages?

Exercise. When appending lists, there is a danger of incurring quadratic complexity. Does that happen in the above function? Could it happen in a different function that uses the Validation applicative based on the list monoid?

Smarter Validation applicative

Next day your accountant sends you another thousand-line file to sum up. This time your terminal gets flooded by error messages:

Bad number on line 1: 27297. Bad number on line 2: 11986. Bad number on line 3: 18938. Bad number on line 4: 22820. ...

You already see the problem: every number ends with a dot. This is trivial to diagnose and fix, and there is absolutely no need to print a thousand error messages.

In fact, there are two different reasons to limit the number of reported errors:

  1. User experience: it is unlikely that the user will pay attention to more than, say, 10 messages at once. If we try to display too many errors on a web page, it may get slow and ugly.
  2. Efficiency: if we agree it’s only worth printing the first 10 errors, then, once we gather 10 errors, there is no point processing the data further.

Turns out, each of the two goals outlined above will need its own mechanism.

Bounded lists

We first develop a list-like datatype which stores only the first n elements and discards anything else that may get appended. This primarily addresses our first goal, user experience, although it will be handy for achieving the second goal too.

Although for validation purposes we may settle with the limit of 10, it’s nice to make this a generic, reusable type with a flexible limit. So we’ll make the limit a part of the type, taking advantage of the type-level number literals.

Exercise. Think of the alternatives to storing the limit in the type. What are their pros and cons?

On the value level, we will base the new type on difference lists, to avoid the quadratic complexity issue that I allude to above.

data BoundedList (n :: Nat) a = BoundedList !Integer -- current length of the list (Endo [a])

Exercise. Why is it important to cache the current length instead of computing it from the difference list?

Once we’ve figured out the main ideas (encoding the limit in the type, using difference lists, caching the current length), the actual implementation is straightforward.

singleton :: KnownNat n => a -> BoundedList n a singleton a = fromList [a] toList :: BoundedList n a -> [a] toList (BoundedList _ (Endo f)) = f [] fromList :: forall a n . KnownNat n => [a] -> BoundedList n a fromList lst = BoundedList (min len limit) (Endo (genericTake limit lst ++)) where limit = natVal (Proxy :: Proxy n) len = genericLength lst instance KnownNat n => Monoid (BoundedList n a) where mempty = BoundedList 0 mempty mappend b1@(BoundedList l1 f1) (BoundedList l2 f2) | l1 >= limit = b1 | l1 + l2 <= limit = BoundedList (l1 + l2) (f1 <> f2) | otherwise = BoundedList limit (f1 <> Endo (genericTake (limit - l1)) <> f2) where limit = natVal (Proxy :: Proxy n) full :: forall a n . KnownNat n => BoundedList n a -> Bool full (BoundedList l _) = l >= natVal (Proxy :: Proxy n) null :: BoundedList n a -> Bool null (BoundedList l _) = l <= 0 SmartValidation

Now we will build the smart validation applicative which stops doing work when it doesn’t make sense to collect errors further anymore. This is a balance between the Either applicative, which can only store a single error, and Validation, which collects all of them.

Implementing such an applicative functor is not as trivial as it may appear at first. In fact, before reading the code below, I recommend doing the following

Exercise. Try implementing a type and an applicative instance for it which adheres to the above specification.

Did you try it? Did you succeed? This is not a rhetorical question, I am actually interested, so let me know. Is your implementation the same as mine, or is it simpler, or more complicated?

Alright, here’s my implementation.

newtype SmartValidation (n :: Nat) e a = SmartValidation { getSmartValidation :: forall r . Either (BoundedList n e) (a -> r) -> Either (BoundedList n e) r } deriving Functor instance KnownNat n => Applicative (SmartValidation n e) where pure x = SmartValidation $ \k -> k <*> Right x SmartValidation a <*> SmartValidation b = SmartValidation $ \k -> let k' = fmap (.) k in case a k' of Left errs | full errs -> Left errs r -> b r

And here are some functions to construct and analyze SmartValidation values.

-- Convert SmartValidation to Either fatal :: SmartValidation n e a -> Either [e] a fatal = left toList . ($ Right id) . getSmartValidation -- Convert Either to SmartValidation nonFatal :: KnownNat n => Either e a -> SmartValidation n e a nonFatal a = SmartValidation $ (\k -> k <+> left singleton a) -- like <*>, but mappends the errors (<+>) :: Monoid e => Either e (a -> b) -> Either e a -> Either e b a <+> b = case (a,b) of (Right va, Right vb) -> Right $ va vb (Left e, Right _) -> Left e (Right _, Left e) -> Left e (Left e1, Left e2) -> Left $ e1 <> e2

Exercise. Work out what fmap (.) k does in the definition of <*>.

Exercise. In the definition of <*>, should we check whether k is full before evaluating a k'?

Exercise. We developed two mechanisms — BoundedList and SmartValidation, which seem to do about the same thing on different levels. Would any one of these two mechanisms suffice to achieve both our goals, user experience and efficiency, when there are many errors being reported?

Exercise. If the SmartValidation applicative was based on ordinary lists instead of difference lists, would we be less or more likely to run into the quadratic complexity problem compared to simple Validation?

Conclusion

Although the Validation applicative is known among Haskellers, the need to limit the number of errors it produces is rarely (if ever) discussed. Implementing an applicative functor that limits the number of errors and avoids doing extra work is somewhat tricky. Thus, I am happy to share my solution and curious about how other people have dealt with this problem.

Categories: Offsite Blogs

Strongly-typed ghci commands

Haskell on Reddit - Sat, 05/02/2015 - 1:56pm
Categories: Incoming News

Parsing YAML with varying structure

haskell-cafe - Sat, 05/02/2015 - 1:55pm
Dear Cafe, I need help parsing YAML files with varying structure. The minimal example is: a yaml file that has one key, which can hold either one key-value pair or two key value pairs. I have data types for the one key, and the two possible sub-keys: To read MyList and Item from the file I wrote FromJSON instances I also have read functions for MyList and Item: The file test.yaml looks like or, alternatively The question is how I can decode test.yaml to get Var. Trying to code readVar like readItem (having FromJSON Var like FromJSON Item) failed. For convenience I attached the relevant source files. Regards, Johannes. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe< at >haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Categories: Offsite Discussion