Since the last release of ghc-heap-view, which was compatible with GHC-7.6, I got 8 requests for a GHC-7.8 compatible version. I started working on it in January, but got stuck and then kept putting it off.
Today, I got the ninths request, and I did not want to wait for the tenth, so I finally finished the work and you can use the new ghc-heap-view-0.5.2 with GHC-7.8.
I used this chance to migrate its source repository from Darcs to git (mirrored on GitHub), so maybe this means that when 7.10 comes out, the requests to update it come with working patches :-). I also added a small test script so that travis can check it:
I did not test it very thoroughly yet. In particular, I did not test whether ghc-vis works as expected.
I still think that the low-level interface that ghc-heap-view creates using custom Cmm code should move into GHC itself, so that it does not break that easily, but I still did not get around to propose a patch for that.
In January I announced my implementation of weight-biased leftist heaps verified with dependent types in Agda. This was part of my work on a paper submitted to CAV’14 conference. The paper got rejected and I decided not to resubmit it anywhere else. At this year’s ICFP listening to Stephanie Weirich’s keynote speech motivated me to finally port that implementation to Haskell, something that I had planned for a couple of months now. You can take a look at the result on github. Here I want to share some of my experiences and insights.
My overall impression is that porting from Agda to Haskell turned out to be fairly straightforward. It was definitely not a complete rewrite. More like syntax adjustments here and there. There were of course some surprises and bumps along the way but nothing too problematic. More precise details are given in the code comments.Agda beats Haskell
When it comes to programming with dependent types Agda, being a fully-fledged dependently-typed language, beats Haskell in many aspects:
- Agda has the same language for terms and types. Haskell separates these languages, which means that if I want to have addition for natural numbers then I need to have two separate definitions for terms and types. Moreover, to tie types and terms together I need singleton types. And once I have singleton types then I need to write third definition of addition that works on singletons. All of this is troublesome to write and use. (This tedious process can be automated by using singletons package.)
- interactive agda-mode for Emacs makes writing code much simpler in Agda. Here I was porting code that was already written so having an interactive Emacs mode for Haskell was not at all important. But if I were to write all that dependently-typed code from scratch in Haskell this would be painful. We definitely need better tools for dependently-typed programming in Haskell.
- Agda admits Unicode identifiers. This allows me to have type constructors like ≥ or variables like p≥b. In Haskell I have GEq and pgeb, respectively. I find that less readable. (This is very subjective.)
- Agda has implicit arguments that can be deduced from types. Haskell does not, which makes some function calls more difficult. Surprisingly that was not as huge problem as I initially thought it will be.
- Agda is total, while Haskell is not. Since there are bottoms in Haskell it is not sound as a logic. In other words we can prove false eg. by using undefined.
The list is noticeably shorter:
- Haskell has much better term-level syntax. In many places this resulted in significantly shorter code than in Agda.
- Haskell is not total. As stated earlier this has its drawbacks but it also has a good side: we don’t need to struggle with convincing the termination checker that our code does actually terminate. This was painful in Agda since it required using sized types.
- Haskell’s gcastWith function is much better than Agda’s subst. Both these functions allow type-safe casts given the proof that the cast is safe. The difference is that Agda’s subst requires more explicit arguments (as I noted earlier the opposite is usually the case) and restricts the cast to the last type parameter (Haskell allows cast for any type parameter).
While the list of wins is longer for Agda than it is for Haskell I’m actually very happy with Haskell’s performance in this task. The verification in Haskell is as powerful as it is in Agda. No compromises required.
It’s worth remarking that my implementation works with GHC 7.6, so you don’t need the latest fancy type-level features like closed type families. The really essential part are the promoted data types.
By turing tarpits, I mean programming languages such as the SKI calculus, bitwise cyclic tag, rule 110, brainfuck and so on. I'm interested in studying those languages, as well as their properties, but I couldn't find a single useful reference, book or anything.
Specifically, I'm curious in:
An extensive list of turing tarpits similar to SKI calculus (that is, work by expression reduction).
Sorting that list based on the kolmogorov complexity of a specific function under that system.
And so on. Anything to help me?submitted by eluspac
[link] [7 comments]
There are those that exists that may be having trouble solving an NP-Complete problem using haskell, and are possibly requesting the help of the mighty and ingenious people of /r/haskell.
This request is not made lightly, dozens of man hours have been spent by not-so-great minds trying to solve this problem, all to no avail. After countless hours reading about haskell and attempting to code, the heads are hitting the proverbial code wall.
The problem is thus:
Given 2 command line parameters, # of students and # of groups, create a program that outputs complete unique groups for 8 assignments, with a student being unable to work with another student more than once across all assignments. If the number of students and groups are such that this is not possible, an error message should print out.
Any input would be appreciated - solutions (YAY!), hints, websites or other threads that we have not found, literally anything.
You are Thanked in Advance, mighty denizens of this subreddit.submitted by CluelessInHaskell
[link] [1 comment]
It would be really great if someone uploaded a linux distro with every package on Hackage installed.
I'm saying this as someone really frustrated with Cabal. I'm sorry, I don't know what is wrong, but I can not get it to work. I waste hours/days trying to install a lib, and I don't understand the error messages. Yes, I've read the manual. This is my #1 problem with Haskell - everything else being great. To be honest, I am completely unable to do anything useful with Haskell because 95% of the time I am fighting Cabal. I'm not joking. So, yea, maybe it is a flaw on my part, but what can I do? If someone on this community is willing to be the hero, I would be really, really thankful for a linux distro with Haskell.submitted by eluspac
[link] [34 comments]
I want to study the complete grammar of Haskell (or GHC, which also includes some extensions to Haskell), but I want it to be in BNF syntax. I know that the Haskell 2010 record contains some BNF like syntax, but they are separated in different pages, and I even don't know what is needed and what not.etairi
[link] [13 comments]
Hello fellow Haskellers (and Werckers?),
I've made a Haskell box with all the exclusive Stackage packages preinstalled (all Stackage inclusive packages are available), so if you depend on these packages, you won't need to recompile them every time you test/deploy, and thus save time, electricity and polar bears.
The box is available here:
the recipes for creating the box are here:
I hope that this is the right place for these kind of announcements and that you will find it helpful :)Some additional notes
If you don't know what Wercker ( wercker.com ) is, it allows you do testing/deploying in cloud, kinda like Travis-CI, I suppose. It is a proprietary Service as a Software Substitute, so be warned.
You might also want to know what Stackage snapshots are actually being used. If you study the recipe, you will find, that it is maybe to clever for its own good. At the time of box creation, it uses the most up-to-date ones, using this alias
the actual snapshot hashes are printed to the log when deploying to the cloud
unfortunately, this log is accessible only to me as the creator
As of now, the Stackage (inclusive) snapshot being used is this one:
and the preinstalled packages are from the corresponding exclusive snapshot
If you would like to do something similar on your own machine, have a look at this
here are the logs:
this is such a simple (but crucial) step, that I forgot to mention it, sorry.
you use this by adding file wercker.yml to your repo with this content:box: firstname.lastname@example.org
and than add your repo (App) in the wercker web ui.submitted by sideEffffECt
[link] [7 comments]