Functional Programming

Google Maps on Android demands I let Google track me

Planet Haskell - Sun, 03/29/2015 - 06:00
I recently upgraded to Android 5.1 on my Nexus 10. One app I often use is Google Maps. This has a "show my location" button:  When I clicked on this I got the following dialog box:Notice that I have two options: I either agree to let Google track me, or I cancel the request. There is no "just show my location" option. As a matter of principle, I don't want Google to be tracking me. I'm aware that Google can offer me all sorts of useful services if I just let it know every little detail of my life, but I prefer to do without them. But now it seems that zooming in on my GPS-derived location has been added to the list of features I can't have. There is no technical reason for this; it didn't used to be the case. But Google has decided that as the price for looking at the map of where I am, I now have to tell them where I am all the time.I'm aware that of course my cellphone company knows roughly where I am and who I talk to, and my ISP knows which websites I visit and can see my email (although unlike GMail I don't think they derive any information about me from the contents), and of course Google knows what I search for. But I can at least keep that information compartmentalised in different companies. I suspect that the power of personal data increases non-linearly with the volume and scope, so having one company know where I am and another company read my email means less loss of privacy than putting both location and email in the same pot. Hey, Google, stop being evil!

An academic birthday present

Planet Haskell - Sun, 03/29/2015 - 06:00
Yesterday, which happened to be my 30th birthday, a small package got delivered to my office: The printed proceedings of last year's “Trends in Functional Programming” conference, where I published a paper on Call Arity (preprint). Although I doubt the usefulness of printed proceedings, it was a nicely timed birthday present. Looking at the rather short table of contents – only 8 papers, after 27 presented and 22 submitted – I thought that this might mean that, with some luck, I might have chances to get the “Best student paper award”, which I presumed to be announced at the next iteration of the conference. For no particular reason I was leisurely browsing through the book, and started to read the preface. And what do I read there? Among the papers selected for these proceedings, two papers stood out. The award for Best Student Paper went to Joachim Breitner for his paper entitled Call Arity, and the award for Best Paper Overall went to Edwin Brady for his paper entitled Resource-dependent Algebraic Effects. Congratulations! Now, that is a real nice birthday present! Not sure if I even would have found out about it, had I not have thrown a quick glance at page V... I hope that it is a good omen for my related ICFP'15 submission. 2015-03-28T13:13:15Z Joachim Breitner mail@joachim-breitner.de

Algebraic side effects

Planet Haskell - Sun, 03/29/2015 - 06:00
Haskell differentiates itself from most other functional languages by letting you reason mathematically about programs with side effects. This post begins with a pure Haskell example that obeys algebraic equations and then generalizes the example to impure code that still obeys the same equations.AlgebraIn school, you probably learned algebraic rules like this one:f * (xs + ys) = (f * xs) + (f * ys)Now let's make the following substitutions:Replace the mathematical multiplication with Haskell's map functionReplace the mathematical addition with Haskell's ++operatorThese two substitutions produce the following Haskell equation:map f (xs ++ ys) = (map f xs) ++ (map f ys)In other words, if you concatenate the list xs with the list ys and then map a function named f over the combined list, the result is indistinguishable from mapping f over each list individually and then concatenating them.Let's test this equation out using the Haskell REPL:>>> map (+ 1) ([2, 3] ++ [4, 5])[3,4,5,6]>>> (map (+ 1) [2, 3]) ++ (map (+ 1) [4, 5])[3,4,5,6]Evaluation orderHowever, the above equation does not hold in most other languages. These other languages use function evaluation to trigger side effects, and therefore if you change the order of evaluation you change the order of side effects.Let's use Scala to illustrate this. Given the following definitions:>>> def xs() = { print("!"); Seq(1, 2) }>>> def ys() = { print("?"); Seq(3, 4) }>>> def f(x : Int) = { print("*"); x + 1 }.. the order of side effects differs depending on whether I concatenate or map first:>>> (xs() ++ ys()).map(f)!?****res0: Seq[Int] = List(2, 3, 4, 5)>>> (xs().map(f)) ++ (ys().map(f))!**?**res1: Seq[Int] = List(2, 3, 4, 5)One line #1, the two lists are evaluated first, printing "!" and "?", followed by evaluating the function f on all four elements, printing "*" four times. On line #2, we call f on each element of xs before beginning to evaluate ys. Since evaluation order matters in Scala we get two different programs which print the punctuation characters in different order.The solutionHaskell, on the other hand, strictly separates evaluation order from side effect order using a two-phase system. In the first phase you evaluate your program to build an abstract syntax tree of side effects. In the second phase the Haskell runtime executes the tree by interpreting it for its side effects. This phase distinction ensures that algebraic laws continue to behave even in the presence of side effects.To illustrate this, we'll generalize our original Haskell code to interleave side effects with list elements and show that it still obeys the same algebraic properties as before. The only difference from before is that we will:Generalize pure lists to their impure analog, ListTGeneralize functions to impure functions that wrap side effects with liftGeneralize (++) (list concatenation) to (<|>) (ListT concatenation)Generalize map to (=<<), which streams elements through an impure functionThis means that our new equation becomes:-- f * (xs + ys) = (f * xs) + (f * ys) f =<< (xs <|> ys) = (f =<< xs) <|> (f=<< ys)You can read this as saying: if we concatenate xs and ys and then stream their values through the impure function f, the behavior is indistinguishable from streaming each individual list through f first and then concatenating them.Let's test this equation out with some sample definitions for xs, ys, and f that mirror their Scala analogs:>>> import Control.Applicative>>> import Pipes>>> let xs = do { lift (putChar '!'); return 1<|> return 2 }>>> let ys = do { lift (putChar '?'); return 3<|> return 4 }>>> let f x = do { lift (putChar '*'); return (x + 1) }>>> runListT (f =<< (xs <|> ys)) -- Note:`runListT` discards the result!**?**>>> runListT ((f =<< xs) <|> (f =<< ys))!**?**>>>The resulting punctuation order is identical. Many people mistakenly believe that Haskell's mathematical elegance breaks down when confronted with side effects, but nothing could be further from the truth.ConclusionHaskell preserves algebraic equations even in the presence of side effects, which simplifies reasoning about impure code. Haskell separates evaluation order from side effect order so that you spend less time reasoning about evaluation order and more time reasoning about your program logic.

The basics of coinduction

Planet Haskell - Sun, 03/29/2015 - 06:00
I don’t remember when I first heard the terms “coinduction” and “corecursion” but it must have been quite long ago. I had this impression that they are yet another of these difficult theoretical concepts and that I should learn about them one day. That “one day” happened recently while reading chapter 5 of “Certified Programming […]

Qualified Goals in the Cabal Solver

Planet Haskell - Sun, 03/29/2015 - 06:00
When you ask cabal-install to install one or more packages, it needs to solve a constraint satisfaction problem: select a version for each of the packages you want to install, plus all their dependencies, such that all version constraints are satisfied. Those version constraints come both from the user [...]

MinGHC for GHC 7.10

Planet Haskell - Sun, 03/29/2015 - 06:00
We're happy to announce the availability of MinGHC for GHC 7.10. MinGHC is a minimal GHC installer for Windows, consisting of:GHC itselfcabal-installMSYS, which is necessary for building some packages such as networkMinGHC came out of some conversation Neil Mitchell and I had at ICFP last year about pain on the Windows platform, and consists of a lot of good code by Neil, and some hacky attempts by me at understanding Windows installer processes. While this project predates the Commercial Haskell SIG by a few months, it's essentially the first project undertaken by the group.While MinGHC is relatively young, it's also a minimalistic product, simply repackaging and serving upstream components unmodified. Additionally, it has become the recommended installer by quite a few sites, and therefore has already received significant testing. Also, due to its minimal nature, it's easy to pop out new releases of MinGHC. For example, this current release was made less than two hours after GHC itself was released!While this project is stable, additional testers and contributors are certainly welcome. Please check out the Github project page for more information.

Value vs Monomorphism Restriction

Planet Haskell - Sun, 03/29/2015 - 06:00
Posted on March 27, 2015 Tags: sml, haskell I’m taking the undergraduate course on programming languages at CMU. For the record, I still get really excited about the novelty of taking a class (at school!) on programming languages. I’m easily made happy. We started talking about System F and before long we touched on the value restriction. Specifically, how most people think of the value restriction incorrectly. To understand why this is, let’s first define the value restriction since it’s probably new to you if you don’t use SML. The Value Restriction In SML there are value level declarations just like in Haskell. We can write things like val x = 1 val y = x + 1 and we end up with x bound to 1 and y bound to 2. Note that SML is strict so these bindings are evaluated right as we reach them. Also like in Haskell, SML has polymorphism, so we can write map fun map f [] = [] | map f (x :: xs) = f x :: map f xs And it gets the type ('a -> 'b) -> ('a list -> 'b list). Aside from minor syntatic differences, this is pretty much identical to what we’d write in Haskell. The value restriction concerns the intersection of these two things. In SML, the following should not compile under the standard val x = rev [] This is because SML requires that all polymorphic val bindings be values! In practice all implementations will do something besides this but we’ll just focus on what the standard says. Now the reason for this value restriction is widely misunderstood. Most people believe that the value restrictions val r = ref NONE val () = r := SOME 1 val _ = case !r of SOME s => s | NONE => "" This seems to illustrate a pretty big issue for SML! We’re filling in polymorphic reference with one type and unboxing it with a different one! Clearly this would segfault without the value restriction. However, there’s a catch. SML is based on System F (did you really think I could get through a blog post without some theory?) which is sometimes called the “polymorphic lambda calculus”. It’s the minimal language with polymorphism and functions. In this language there’s a construct for making polymorphic things: Λ. In this language we write polymorphism explicitly by saying Λ τ. e which has the type ∀ t. T. So for example we write the identity function as id ≡ Λ τ. λ x : τ. x () = id[unit] () Now SML (and vanilla Haskell) have a limited subset of the power of Λ. Specifically all these lambdas have to appear at the start of a toplevel term. Meaning that they have to be of the form val x = Λ α. Λ β. ... e This is called “prenex” form and is what makes type inference for SML possible. Now since we don’t show anyone the hidden Λs it doesn’t make sense to show them the type application that comes with them and SML infers and adds those for us too. What’s particularly interesting is that SML is often formalized as having this property: values start with Λ and are implicitly applied to the appropriate types where used. Even more interesting, how do you suppose we should evaluate a Λ? What for example, should this code do val x = Λ τ. raise[τ] Fail (* Meaning raise an exception and say we have type τ *) val () = print "I made it here" val () = x[unit] It seems clear that Λ should be evaluated just like how we evaluate λ, when we apply it. So I’d (and the formalization of SML) would expect this to print "I made it here" before throwing that exception. This might now surprise you just by parallels with code like this val x = fn () => raise[τ] Fail val () = print "I made it here" val () = x () However, what about when those lambdas are implicit? In the actual source language of ML our code snippet would be val x = raise Fail val () = print "I made it here" val () = x[unit] Uhoh, this really looks like it ought to throw an exception but it apparently doesn’t! More worringly, what about when we have something like fun die () = raise Fail val x = die () val () = print "Made it here" Since x is never specialized, this doesn’t even throw an error! Yikes! Clearly this is a little confusing. It is however, type safe. Consider our original motivation for the value restriction. With explicit type application val r = Λ τ. ref[τ] NONE val () = r[int] := SOME 1 val _ = case !(r[string]) of SOME s => s | NONE => "" Since the body of this function is run every time we do something with r, we’re just creating a whole bunch of new references in this code! There’s no type safety failure since !(r[string]) returns a fresh ref cell, completely different from the one we modified on the line above! This code always runs the NONE case. In fact, if this did the wrong thing it’s just a canary in the coal mine, a symptom of the fact that our system evaluates under (big) lambda binders. So the value restriction is really not at all about type safety, it’s about comprehensibility. Mostly since the fact that a polymorphic expression is evaluated at usage rather than location is really strange. Most documentation seems to be wrong about this, everyone here seems agree that this is unfortunate but such is life. The Monomorphism Restriction Now let’s talk about the monomorphism restriction. This is better understood but still worth recapping. In Haskell we have type classes. They let us overload function to behave differently on different types. Everyone’s favoriate example is the type class for numbers which let’s us write fact :: (Eq a, Num a) => a -> a fact 0 = 1 fact n = n * fact (n - 1) And this works for all numbers, not just int or something. Under the hood, this works by passing a record of functions like *, fromInteger, and - to make the code work. That => is really just a sort of function arrow that happens to only take particular “implicit” records as an argument. Now what do you suppose the most polymorphic type this code is? x = fact 10000 It could potentially work on all numbers so it gets the type x :: (Num a, Eq a) => a However this is really like a function! This means that fact :: Integer and fact :: Int evaluate that computation twice. In fact each time we call fact we supply a new record and end up evaluating again. This is very costly and also very surprising to most folks. After all, why should something that looks like a normal number evaluate every time we use it! The monomorphism restriction is essentially If you have a binding Whose type is (C1, C2 ...) => t And has no arguments to the left of the = Don’t generalize it This is intended to keep us from the surprise of evaluating a seemingly fully reduced term twice. Sound familiar? Just like with the value restriction the whole point of the monomorphism restriction is to prevent a hidden function, either type abstraction or type constraints, from causing us to silently and dangerously duplicate work. While neither of them are essential to type safety: without it some really simple looking pieces of code become exponential. Wrap Up That about covers things. It turns out that both of these restrictions are just patches to cover some surprising areas of the semantics but both are easily understood when you look at the elaborated version. I deliberately went a bit faster through the monomorphism restriction since quite a lot of ink has already been spilled on the subject and unlike the value restriction, most of it is correct :) As one final note, the way that Haskell handles the monomorphism restriction is precisely how OCaml handles the value restriction: weak polymorphism. Both of them mark the type variables they refuse to generalize as weak type variables. Whenever we first instantiate them to something we go back and retroactively modify the definition to pretend we had used this type all along. In this way, we only evaluate things once but can handle a lot of simple cases of binding a value and using it once. The more you know. var disqus_shortname = 'codeco'; (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 2015-03-27T00:00:00Z

Schrödinger’s Box

Planet Haskell - Sun, 03/29/2015 - 06:00
In Objective-C, NSValue provides a universal container that can hold scalars and value types in addition to references. Conversely, in Swift, we quickly learnt to appreciate Box as a wrapper to embed (cyclic) references in enums and structs (especially due to limitations in the initial versions of the Swift compiler): final public class Box { public let unbox: T public init(_ value: T) { self.unbox = value } } NSValue is also useful to wrap reference. For example, if we want to turn a strong reference into a weak reference (possibly to store it in a collection, such as NSArray), we can create an NSValue with +valueWithNonretainedObject. How do we achieve that in Swift without losing type information, as using NSValue would? We use Schrödinger’s Box: final public class WeakBox { private weak var box: T? public var unbox: T? { get { return box } } public init(_ value: T) { self.box = value } } You can put something into Schrödinger’s Box, which will or will not be gone by the time you try to retrieve it. It enables, for example, to build a typed collection of weakly referenced objects (to avoid retain cycles). NB: The definition of WeakBox is fine with the latest Swift 1.2 compiler. However, the Swift 1.1 compiler can only handle it with -Onone; otherwise, it crashes. 2015-03-26T23:43:21Z

New website with new talks

Planet Haskell - Sun, 03/29/2015 - 06:00
My website is now located at ndmitchell.com and has a few new talks on it:Slides and Video from Gluing things together with Haskell given at Code Mesh 2014. I argue that shell script should die, and talk about how Shake, NSIS and Bake are helping that happen. Slides from Building stuff with Shake given at FP Days 2014 - an introduction to Shake through a series of examples.My old website at community.haskell.org is going to stop being updated, and I'll be putting in redirections shortly. That server is going to stop hosting websites, so I bought myself a domain name and setup a GitHub pages website. The repo is here, including all the data, metadata, templates and scripts. 2015-03-26T22:01:00Z Neil Mitchell noreply@blogger.com

Our composable community infrastructure

Planet Haskell - Sun, 03/29/2015 - 06:00
Our composable community infrastructureTL;DR: we propose to factor Hackage into a separate, very simple service serving a stash of Haskell packages, with the rest of Hackage built on top of that, in the name of availability, reliability and extensibility.One of the main strengths of Haskell is just how much it encourages composable code. As programmers, we are goaded along a good path for composability by the strictures of purity, which forces us to be honest about the side effects we might use, but first and foremost because first class functions and lazy evaluation afford us the freedom to decompose solutions into orthogonal components and recompose them elsewhere. In the words of John Hughes, Haskell provides the necessary glue to build composable programs, ultimately enabling robust code reuse. Perhaps we ought to build our shared community infrastructure along the same principles: freedom to build awesome new services by assembling together existing ones, made possible by the discipline to write these basic building blocks as stateless, scalable, essentially pure services. Let's think about how, taking packages hosting as an example, with a view towards solving three concrete problems:Availability of package metadata and source code (currently these are no longer available when hackage.haskell.org goes down).Long cabal update download times.The difficulty of third party services and other community services to interoperate with hackage.haskell.org and extend it in any direction the community deems fit.Haskell packagesToday Haskell packages are sets of files with a distinguished *.cabal file containing the package metadata. We host these files on a central package repository called Hackage, a community supported service. Hackage is a large service that has by and large served the community well, and has done so since 2007. The repository has grown tremendously, by now hosting no less than 5,600 packages. It implements many features, some of which include package management. In particular, Hackage allows registered users to:Upload a new package: either from the browser or via cabal upload.Download an index of all packages available: this index includes the full content of all *.cabal files for all packages and all versions.Query the package database via a web interface: from listing all packages available by category, to searching packages by name. Hackage maintains additional metadata for each package not stored in the package itself, such as download counts, package availability in various popular Linux distributions. Perhaps in the future this metadata will also include social features such as number of "stars", à la Github.Some of the above constitute the defining features of a central package repository. Of course, Hackage is much more than just that today - it is a portal for exploring what packages are out there through a full blown web interface, running nightly builds on all packages to make sure they compile and putting together build reports, generating package API documentation and providing access to the resulting HTML files, maintaining RSS feeds for new package uploads, generating activity graphs, integration with Hoogle and Hayoo, etc.In the rest of this blog post, we'll explore why it's important to tweeze out the package repository from the rest, and build the Hackage portal on top of that. That is to say, talk separately about Hackage-the-repository and Hackage-the-portal.A central hub is the cement of the communityA tell-tale sign of a thriving development community is that a number of services pop up independently to address the needs of niche segments of the community or indeed the community as a whole. Over time, these community resources together as a set of resources form an ecosystem, or perhaps even a market, in much the same way that the set of all Haskell packages form an ecosystem. There is no central authority deciding which package ought to be the unique consecrated package for e.g. manipulating filesystem paths: on Hackage today there are at least 5, each exploring different parts of the design space.However, we do need common infrastructure in place, because we do need consensus about what package names refer to what code and where to find it. People often refer to Hackage as the "wild west" of Haskell, due to its very permissive policies about what content makes it on Hackage. But that's not to say that it's an entirely chaotic free-for-all: package names are unique, only designated maintainers can upload new versions of some given package and version numbers are bound to a specific set of source files and content for all time.The core value of Hackage-the-repository then, is to establish consensus about who maintains what package, what versions are available and the metadata associated with each version. If Alice has created a package called foolib, then Bob can't claim foolib for any of his own packages, he must instead choose another name. There is therefore agreement across the community about what foolib means. Agreement makes life much easier for users, tools and developers talking about these packages.What doesn't need consensus is anything outside of package metadata and authorization: we may want multiple portals to Haskell code, or indeed have some portals dedicated to particular views (a particular subset of the full package set) of the central repository. For example, stackage.org today is one such portal, dedicated to LTS Haskell and Stackage Nightly, two popular views of consistent package sets maintained by FP Complete. We fully anticipate that others will over time contribute other views — general-purpose or niche (e.g. specialized for a particular web framework) — or indeed alternative portals — ranging from small, fast and stable to experimental and replete with social features aplenty. Think powerful new search functionality, querying reverse dependencies, pre-built package sets for Windows, OS X and Linux, package reviews, package voting ... you name it!Finally, by carving out the central package repository into its own simple and reliable service, we limit the impact of bugs on both availability and reliably, and thus preserve on one of our most valuable assets: the code that we together as a community have written. Complex solutions invariably affect reliability. Keeping the core infrastructure small and making it easy to build on top is how we manage that.The next section details one way to carve the central package repository, to illustrate my point. Alternative designs are possible of course - I merely wish to seek agreement that a modular architecture with at its core a set of very small and simple services as our community commons would be beneficial to the community.Pairing down the central hub to its bare essenceBefore we proceed, let's first introduce a little bit of terminology:A persistent data structure is an data structure that is never destructively updated: when modified, all previous versions of the data structure are still available. Data.Map from the containers package is persistent in this sense, as are lists and most other data structures in Haskell.A service is stateless if its response is a function of the state of other services and the content of the request. Stateless services are trivially scaled horizontally - limited only by the scalability of the services they depend on.A persistent service is a service that maintains its only state as a persistent data structure. Most resources served by a persistent service are immutable. Persistent services share many of the same properties as stateless services: keeping complexity down and scaling them is easy because concurrent access and modification of a persistent data structure requires little to no coordination (think locks, critical sections, etc).A central hub for all open source Haskell packages might look something like this:A persistent read-only directory of metadata for all versions of all packages (i.e. the content of the .cabal file). Only the upload service may modify this directory, and even then, only in a persistent way.A persistent read-only directory of the packages themselves, that is to say the content of the archives produced by cabal sdist.An upload service, for uploading new revisions of the metadata directory. This service maintains no state of its own, therefore multiple upload services can be spawned if necessary.An authentication service, granting access tokens to users for adding a new package or modifying the metadata for their own existing packages via the upload service(s).The metadata and package directories together form a central repository of all open source Haskell packages. Just as is the case with Hackage today, anyone is allowed to upload any package they like via the upload service. We might call these directories collectively The Haskell Stash. End-user command-line tools, such as cabal-install, need only interact with the Stash to get the latest list of packages and versions. If the upload or authentication services go down, existing packages can still be downloaded without any issue.Availability is a crucial property for such a core piece of infrastructure: users from around the world rely on it today to locate the dependencies necessary for building and deploying Haskell code. The strategy for maintaining high availability can be worked out independently for each service. A tried and tested approach is to avoid reinventing as much of the wheel as we can, reusing existing protocols and infrastructure where possible. I envision the following implementation:Serve the metadata directory as a simple Git repository. A Git repository is persistent (objects are immutable and live forever), easy to add new content to, easy to backup, easy to mirror and easy to mine for insights on how packages changes over time. Advanced features such as package candidates fall out nearly for free. Rather than serving in its entirety a whole new static tarball of all package metadata (totalling close to 9MB of compressed data) as we do today, we can leverage the existing Git wire protocol to transfer new versions to end users much more efficiently. In short, a faster cabal update!.The point here is very much not to use Git as a favoured version control system (VCS), fine as it may be for that purpose, at the expense of any other such tool. Git is at its core an efficient persistent object store first and foremost, with a VCS layered on top. The idea is to not reinvent our own object store. It features a simple disk format that has remained incredibly stable over the years. Hosting all our metadata as a simple Git repository means we can leverage any number of existing Git hosting providers to serve our community content with high uptime guarantees.Serve package source archives (produced by cabal sdist) via S3, a de facto standard API for file storage, supported by a large array of cloud providers. These archives can be large, but unlike package metadata, their content is fixed for all time. Uploading a new version of a package means uploading a new source archive with a different name. Serving our package content via a standard API means we can have that content hosted on a reliable cloud platform. In short, better uptime and higher chance that cabal install will not randomly fail.ConclusionThe Haskell Stash is a repository in which to store our community's shared code assets in as simple, highly available and composable a manner as possible. Reduced to its bare essence, easily consumable by all manner of downstream services, most notably, Hackage itself, packdeps.haskellers.org, hdiff.luite.com, stackage.org, etc. It is by enabling people to extend core infrastructure in arbitrary directions that we can hope to build a thriving community that meets not just the needs of those that happened to seed it, but that furthermore embraces new uses, new needs, new people.Provided community interest in this approach, the next steps would be:implement the Haskell Stash;implement support for the Haskell Stash in Hackage Server;in the interim, if needed, mirror Hackage content in the Haskell Stash.In the next post in this series, we'll explore ways to apply the same principles of composability to our command-line tooling, in the interest of making our tools more hackable, more powerful and ship with fewer bugs.

FP Complete's Hackage mirror

Planet Haskell - Sun, 03/29/2015 - 06:00
We have been running a mirror of Hackage package repository which we use internally for the FP Complete Haskell Centre's IDE, building Stackage, and other purposes. This has been an open secret, but now we're making it official.To use it, replace the remote-repo line in your ~/.cabal/config with the following:remote-repo: hackage.fpcomplete.com:http://hackage.fpcomplete.com/Then run cabal update, and you're all set.This mirror is updated every half-hour. It is statically hosted on Amazon S3 so downtime should be very rare (Amazon claims 99.99% availability).The mirror does not include the HTML documentation. However, Stackage hosts documentation for a large set of packages.We have also released our hackage-mirror tool. It takes care of efficiently updating a static mirror of Hackage on S3, should anyone wish to host their own. While the official hackage-server has its own support for mirroring, our tool differs in that it does not require running a hackage-server process to host the mirror.HTTPS for StackageOn a tangentially related note, we have enabled TLS for www.stackage.org. Since cabal-install does not support TLS at this time, we have not set up an automatic redirect from insecure connections to the https:// URL.

Can you trust science?

Planet Haskell - Sun, 03/29/2015 - 06:00
Hardly a week goes by without newspaper writing about new and exciting results from science. Perhaps scientists have discovered a new wonderful drug for cancer treatment, or maybe they have found a physiological cause for CFS. Or perhaps this time they finally proved that homeopathy works? And in spite of these bold announcements, we still don't seem to have cured cancer. Science is supposed to be the method which enables us to answer questions about how the world works, but one could be forgiven for wondering whether it, in fact, works at all. As my latest contribution to my local journal club, I presented a paper by Ioannidis, titled Why most published research findings are false 1. This created something of a stir when it was published in 2005, because it points out some simple mathematical reasons why science isn't as accurate as we would like to believe. The ubiquitous p-value Science is about finding out what is true. For instance, is there a relationship between treatment with some drug and the progress of some disease - or is there not? There are several ways to go about finding out, but in essence, it boils down to making some measurements, and doing some statistical calculations. Usually, the result will be reported along with a p-value, which is a by-product of the statistical calculations saying something about how certain we are of the results. Specifically, if we claim there is a relationship, the associated p-value is the probability we would make such a claim even if there is no relationship in reality. We would like this probability to be low, of course, and since we usually are free to select the p-value threshold, it is usually chosen to be 0.05 (or 0.01), meaning that if the claim is false, we will only accept it 5% (or 1%) of the times. The positive predictive value Now, the p-value is often interpreted as the probability of our (positive) claim being wrong. This is incorrect! There is a subtle difference here, which it is important to be aware of. What you must realize, is that the probability α relies on the assumption that the hypothesis is wrong - which may or may not be true, we don't know (which is precisely why we want to find out). The probability of a claim being wrong after the fact is called the positive predictive value (PPV). In order to say something about this, we also need to take into account the probability of claiming there exists a relationship when the claim is true. Our methods aren't perfect, and even if a claim is true, we might not have sufficient evidence to say for sure. So, take one step back and looking at our options. Our hypothesis (e.g., drug X works against disease Y) can be true or false. In either case, our experiment and analysis can lead us to reject or accept it with some probability. This gives us the following 2-by-2 table: True False Accept 1-β α Reject β 1-α Here, α is the probability of accepting a false relationship by accident (i.e., the p-value), and β is the probability of missing a true relationship -- we reject a hypothesis, even when it is true. To see why β matters, consider a hypothetical really really poor method, which has no chance of identifying a true relationship, in other words, $\beta$=1. Then, every accepted hypothesis must come from the False column, as long as α is at all positive. Even if the p-value threshold only accepts 1 in 20 false relationships, that's all you will get, and as such, they constitute 100% of the accepted relationships. But looking at β is not sufficient either. Let's say a team of researchers test hundreds of hypotheses, which all happen to be false? Then again, some of them will get accepted anyway (sneaking in under the p-value threshold α), and since there are no hypotheses in the True column, again every positive claim is false. A β of 1 or a field of research with 100% false hypotheses are extreme cases2, and in reality, things are not quite so terrible. The Economist had a good article with a nice illustration showing how this might work in practice with more reasonable numbers. It should still be clear that the ratio of true to false hypotheses being tested, as well as the power of the analysis to identify true hypotheses are important factors. And if these numbers approach their limits, things can get quite bad enough. More elaborate models Other factors also influence the PPV. Try as we might to be objective, scientists often try hard to find a relationship -- that's what you can publish, after all3. Perhaps in combination with a less firm grasp of statistics than one could wish for (and scientists who think they know enough statistics are few and far between - I'm certainly no exception there), this introduces bias towards acceptance. Multiple teams pursuing the same challenges in a hot and rapidly developing field also decrease the chance of results being correct, and there's a whole cottage industry of scientist reporting spectacular and surprising results in high-ranking journals, followed by a trickle of failures to replicate. Solving this One option is to be stricter - this is the default when you do multiple hypothesis testing, you require a lower p-value threshold in order to reduce α. The problem with this is that if you are stricter with what you accept as true, you will also reject more actually true hypotheses. In other words, you can reduce α, but only at the cost of increasing β. On the other hand, you can reduce β by running a larger experiment. One obvious problem with this is cost, for many problems, a cohort of a hundred thousand or more is necessary, and not everybody can afford to run that kind of studies. Perhaps even worse, a large cohort means that almost any systematic difference will be found significant. Biases that normally are negligible will show up as glowing bonfires in your data. In practice? Modern biology has changed a lot in recent years, and today we are routinely using high-throughput methods to test the expression of tens of thousands of genes, or the value of hundreds of thousands of genetic markers. In other words, we simultaneously test an extreme number of hypotheses, where we expect a vast majority of them to be false, and in many cases, the effect size and the cohort are both small. It's often a new and exciting field, and we usually strive to use the latest version of the latest technology, always looking for new and improved analysis tools. To put it bluntly, it is extremely unlikely that any result from this kind of study will be correct. Some people will claim these methods are still good for "hypothesis generation", but Ioannidis shows a hypothetical example where a positive result increases the likelihood that a hypothesis is correct by 50%. This doesn't sound so bad, perhaps, but in reality, the likelihood is only improved from 1 in 10000 to 1 in 7000 or so. I guess three thousand fewer trials to run in the lab is something, but you're still going to spend the rest of your life running the remaining ones. You might expect scientists to be on guard for this kind of thing, and I think most scientists will claim they desire to publish correct results. But what counts for your career is publications and citations, and incorrect results are no less publishable than correct ones - and might even get cited more, as people fail to replicate them. And as you climb the academic ladder, publications in high-ranking journals is what counts, an for that you need spectacular results. And it is much easier to get spectacular incorrect results than spectacular correct ones. So the academic system rewards and encourages bad science. Consequences The bottom line is to be skeptical of any reported scientific results. The ability of the experiment and analysis to discover true relationships is critical, and one should always ask what the effect size is, and what the statistical power -- the probability of detecting a real effect -- is. In addition, the prior probability of the hypothesis being true is crucial. Apparently-solid, empirical evidence of people getting cancer from cell phone radiation, or working homeopathic treatment of disease can almost be dismissed out of hand - there simply is no probable explanation for how that would work. A third thing to look out for, is how well studied a problem is, and how the results add up. For health effects of GMO foods, there is a large body of scientific publications, and an overwhelming majority of them find no ill effects. If this was really dangerous, wouldn't some of these investigations show it conclusively? For other things, like the decline of honey bees, or the cause of CFS, there is a large body of contradictory material. Again - if there was a simple explanation, wouldn't we know it by now? And since you ask: No, the irony of substantiating this claim with a scientific paper is not lost on me.↩ Actually, I would suggest that research in paranormal phenomena is such a field. They still manage to publish rigorous scientific works, see this Less Wrong article for a really interesting take.↩ I think the problem is not so much that you can't publish a result claiming no effect, but that you can rarely claim it with any confidence. Most likely, you just didn't design your study well enough to tell.↩ 2015-03-25T20:00:00Z

GHC Weekly News - 2015/03/24

Planet Haskell - Sun, 03/29/2015 - 06:00
Hi *, It's time for the GHC weekly news. We've had an absence of the last one, mostly due to a lot of hustle to try and get 7.10 out the door (more on that shortly throughout this post). But now we're back and everything seems to be taken care of. This week, in the wake of the GHC 7.10 release (which is occuring EOD, hopefully), GHC HQ met up for a brief chat and caught up: This week GHC HQ met for only a very short time to discuss the pending release - it looks like all the blocking bugs have been fixed, and we've got everything triaged appropriately. You'll hopefully see the 7.10 announcement shortly after reading this. We've also had small amounts of list activity (the past 6-8 weeks have been very, very quiet it seems): Your editor sent out a call for developers to fill information in on the Status page about what they plan to do. If you're working on something, please add it there! ​https://mail.haskell.org/pipermail/ghc-devs/2015-March/008661.html Herbert Valerio Riedel asked about a possible regression regarding identifiers containing unicode subscripts - but nobody has replied! ​https://mail.haskell.org/pipermail/ghc-devs/2015-March/008503.html Doug Burke chimed in as a new contributor and wrote down some notes on what it took to write his first patch and submit it to us - and we really appreciate the feedback, Doug! ​https://mail.haskell.org/pipermail/ghc-devs/2015-March/008526.html Yitzchak Gale revived a thread he started a while back, which puttered out: bootstrapping GHC 7.8 with GHC 7.10. The long and short of it is, it should just about work - although we still haven't committed to this policy, it looks like Yitz and some others are quite adamant about it. ​https://mail.haskell.org/pipermail/ghc-devs/2015-March/008531.html Neil Mitchell uncovered a nasty bug in GHC 7.10.1 RC3, submitted it to us. He also wrote a fantastic ​blog post explaining the issue. And it was promply diagnosed, fixed, and taken care of by our own Joachim Breitner. Thank you for the fast response Joachim and Neil! ​https://mail.haskell.org/pipermail/ghc-devs/2015-March/008532.html Mark Lentczner has announced Alpha releases of the Haskell Platform 2015.2.0.0, containing GHC 7.10.1 RC3: ​https://mail.haskell.org/pipermail/ghc-devs/2015-March/008597.html Simon Peyton Jones asks: what's the current state about having simultaneous installations of a package? Simon is a bit confused as to why this is still a problem when we have all the tools to solve it, it looks like! (But read on for more): ​https://mail.haskell.org/pipermail/ghc-devs/2015-March/008602.html Michael Snoyman asks: can we get a new feature patch in GHC 7.10.2? The answer seems to be an unfortunate 'no', but with some tips, Michael may end up backporting the changes from HEAD to GHC 7.10 himself. ​https://mail.haskell.org/pipermail/ghc-devs/2015-March/008612.html Some noteworthy commits that went into ghc.git in the past two weeks include: Commit 71fcc4c096ec0b575522e4c2d0104ef7a71a13c5 - GHC defaults to using the gold linker on ARM/Android and ARM/Linux targets. Commit 9dfdd16a61e79cb03c633d442190a81fe5c0b6b8 - Bump ghc-prim to version 0.4.0.0. Commit 42448e3757f25735a0a5b5e2b7ee456b5e8b0039 - GHC HEAD now always looks for LLVM 3.6 specifically. Closed tickets this past week include: #9122, #10099, #10081, #9886, #9722, #9619, #9920, #9691, #8976, #9873, #9541, #9619, #9799, #9823, #10156, #1820, #6079, #9056, #9963, #10164, #10138, #10166, #10115, #9921, #9873, #9956, #9609, #7191, #10165, #10011, #8379, #10177, #9261, #10176, #10151, #9839, #8078, #8727, #9849, #10146, #9194, #10158, #7788, #9554, #8550, #10079, #10139, #10180, #10181, #10170, #10186, #10038, #10164, and #8976. 2015-03-25T02:20:19Z thoughtpolice

First impressions of Coq and “Certified Programming with Dependent Types”

Planet Haskell - Sun, 03/29/2015 - 06:00
A simplistic view of strongly typed functional programming ecosystem is that the two most influential languages are Haskell and ML. Haskell is my language of choice so when it came to learning dependently-typed programming I stayed on the Haskell side of the spectrum and went with Agda and Idris. I chose the two over the […]

Infernu’s type system informal summary – first draft

Planet Haskell - Sun, 03/29/2015 - 06:00
I just finished a first draft describing Infernu’s type system. Target audience is potential users. Comments welcome!

A Tiny Compiler For A Typed Higher Order Language

Planet Haskell - Sun, 03/29/2015 - 06:00
Posted on March 24, 2015 Tags: compilers, types, haskell Hi folks, the last week or so I was a little tired of schoolwork so I decided to scratch out some fun code. The end result is an extremely small compiler for a typed, higher order functional language called PCF to C. In this post I’ll explain attempt to explain the whole thing, from front to back :) What’s PCF First things first, it’s important to define the language we’re compiling. The language, PCF short for “partial computable functions”, is an extremely small language you generally find in a book on programming languages, it originates with Plotkin if I’m not mistaken. PCF is based around 3 core elements: natural numbers, functions (closures), and general recursion. There are two constants for creating numbers, Zero and Suc. Zero is self explanatory and Suc e is the successor of the natural number e evaluates to. In most programming languages this just means Suc e = 1 + e but + isn’t a primitive in PCF (we can define it as a normal function). For functions, we have lambdas like you’d find in any functional language. Since PCF includes no polymorphism it’s necessary to annotate the function’s argument with it’s type. Finally, the weird bit: recursion. In PCF we write recursive things with fix x : τ in e. Here we get to use x in e and we should understand that x “stands for” the whole expression, fix .... As an example, here’s how we define +. plus = fix rec : nat -> nat -> nat in λ m : nat. λ n : nat. ifz m { Zero => n | Suc x => Suc (rec x n) } Now Let’s Compile It Now compilation is broken up into a bunch of phases and intermediate languages. Even in this small of a compiler there are 3 (count-em) languages so along with the source and target language there are 5 different languages running around inside of this compiler. Each phase with the exception of typechecking is just translating one intermediate language (IL) into another and in the process making one small modification to the program as a whole. The AST This compiler starts with an AST, I have no desire to write a parser for this because parsers make me itchy. Here’s the AST data Ty = Arr Ty Ty | Nat deriving Eq data Exp a = V a | App (Exp a) (Exp a) | Ifz (Exp a) (Exp a) (Scope () Exp a) | Lam Ty (Scope () Exp a) | Fix Ty (Scope () Exp a) | Suc (Exp a) | Zero deriving (Eq, Functor, Foldable, Traversable) What’s interesting here is that our AST uses bound to manage variables. Unfortunately there really isn’t time to write both a bound tutorial and a PCF compiler one. I’ve written about using bound before here otherwise you can just check out the official docs. The important bits here are that Scope () ... binds one variable and that a stands for the free variables in an expression. 3 constructs bind variables here, Ifz for pattern matching, Fix for recursive bindings, and Lam for the argument. Note also that Fix and Lam both must be annotated with a type otherwise stuff like fix x in x and fn x => x are ambiguous. Type Checking First up is type checking. This should be familiar to most people we’ve written a type checker before since PCF is simply typed. We simply have a Map of variables to types. Since we want to go under binders defined using Scope we’ll have to use instantiate. However this demands we be able to create fresh free variables so we don’t accidentally cause clashes. To prevent this we use monad-gen to generate fresh free variables. To warm up, here’s a helper function to check that an expression has a particular type. This uses the more general typeCheck function which actually produces the type of an expression. type TyM a = MaybeT (Gen a) assertTy :: (Enum a, Ord a) => M.Map a Ty -> Exp a -> Ty -> TyM a () assertTy env e t = (== t) <$> typeCheck env e >>= guard This type checks the variable in an environment (something that stores the types of all of the free variables). Once it receives that it compares it to the type we expected and chucks the resulting boolean into guard. This code is used in places like Ifz where we happen to know that the first expression has the type Nat. Now on to the main code, typeCheck typeCheck :: (Enum a, Ord a) => M.Map a Ty -> Exp a -> TyM a Ty typeCheck _ Zero = return Nat typeCheck env (Suc e) = assertTy env e Nat >> return Nat The first two cases for typeCheck are nice and straightforward. All we if we get a Zero then it has type Nat. If we get a Suc e we assert that e is an integer and then the whole thing has the type Nat. typeCheck env (V a) = MaybeT . return $ M.lookup a env For variables we just look things up in the environment. Since this returns a Maybe it’s nice and easy to just jam it into our MaybeT. typeCheck env (App f a) = typeCheck env f >>= \case Arr fTy tTy -> assertTy env a fTy >> return tTy _ -> mzero Application is a little more interesting. We recurse over the function and make sure it has an actual function type. If it does, we assert the argument has the argument type and return the domain. If it doesn’t have a function type, we just fail. typeCheck env (Lam t bind) = do v <- gen Arr t <$> typeCheck (M.insert v t env) (instantiate1 (V v) bind) typeCheck env (Fix t bind) = do v <- gen assertTy (M.insert v t env) (instantiate1 (V v) bind) t return t Type checking lambdas and fixpoints is quite similar. In both cases we generate a fresh variable to unravel the binder with. We know what type this variable is supposed to have because we required explicit annotations so we add that to the map constituting our environment. Here’s where they diverge. For a fixpoint we want to make sure that the body has the type as we said it would so we use assertTy. For a lambda we infer the body type and return a function from the given argument type to the body type. typeCheck env (Ifz i t e) = do assertTy env i Nat ty <- typeCheck env t v <- gen assertTy (M.insert v Nat env) (instantiate1 (V v) e) ty return ty For Ifz we want to ensure that we actually are casing on a Nat so we use assertTy. Next we figure out what type the zero branch returns and make sure that the else branch has the same type. All in all this type checker is not particularly fascinating since all we have are simple types. Things get a bit more interesting with polymorphism. I’d suggest looking at that if you want to see a more interesting type checker. Closure Conversion Now for our first interesting compilation phase, closure conversion. In this phase we make closures explicit by annotating lambdas and fixpoints with the variables that they close over. Those variables are then explicitly bound in the scope of the lambda. With these changes, our new syntax tree looks like this -- Invariant, Clos only contains VCs, can't be enforced statically due -- to annoying monad instance type Clos a = [ExpC a] data ExpC a = VC a | AppC (ExpC a) (ExpC a) | LamC Ty (Clos a) (Scope Int ExpC a) | FixC Ty (Clos a) (Scope Int ExpC a) | IfzC (ExpC a) (ExpC a) (Scope () ExpC a) | SucC (ExpC a) | ZeroC deriving (Eq, Functor, Foldable, Traversable) The interesting parts are the additions of Clos and the fact that the Scope for a lambda and a fixpoint now binds an arbitrary number of variables instead of just one. Here if a lambda or fixpoint binds n variables, the first n - 1 are stored in the Clos and the last one is the “argument”. Closure conversion is thus just the process of converting an Exp to an ExpC. closConv :: Ord a => Exp a -> Gen a (ExpC a) closConv (V a) = return (VC a) closConv Zero = return ZeroC closConv (Suc e) = SucC <$> closConv e closConv (App f a) = AppC <$> closConv f <*> closConv a closConv (Ifz i t e) = do v <- gen e' <- abstract1 v <$> closConv (instantiate1 (V v) e) IfzC <$> closConv i <*> closConv t <*> return e' Most of the cases here are just recursing and building things back up applicatively. There’s the moderately interesting case where we instantiate the else branch of an Ifz with a fresh variable and then recurse, but the interesting cases are for fixpoints and lambdas. Since they’re completely identical we only present the case for Fix. closConv (Fix t bind) = do v <- gen body <- closConv (instantiate1 (V v) bind) let freeVars = S.toList . S.delete v $ foldMap S.singleton body rebind v' = elemIndex v' freeVars <|> (guard (v' == v) *> (Just $ length freeVars)) return $ FixC t (map VC freeVars) (abstract rebind body) There’s a lot going on here but it boils down into three parts. Recurse under the binder Gather all the free variables in the body Rebind the body together so that all the free variables map to their position in the closure and the argument is n where n is the number of free variables. The first is accomplished in much the same way as in the above cases. To gather the number of free variables all we need to is use the readily available notion of a monoid on sets. The whole process is just foldMap S.singleton! There’s one small catch: we don’t want to put the argument into the list of variables we close over so we carefully delete it from the closure. We then convert it to a list which gives us an actual Clos a. Now for the third step we have rebind. rebind maps a free variable to Maybe Int. It maps a free variable to it’s binding occurrence it has one here. This boils down to using elemIndex to look up somethings position in the Clos we just built up. We also have a special case for when the variable we’re looking at is the “argument” of the function we’re fixing. In this case we want to map it to the last thing we’re binding, which is just length n. To capture the “try this and then that” semantics we use the alternative instance for Maybe which works wonderfully. With this, we’ve removed implicit closures from our language: one of the passes on our way to C. Lambda Lifting Next up we remove both fixpoints and lambdas from being expressions. We want them to have an explicit binding occurrence because we plan to completely remove them from expressions soon. In order to do this, we define a language with lambdas and fixpoints explicitly declared in let expressions. The process of converting from ExpC to this new language is called “lambda lifting” because we’re lifting things into let bindings. Here’s our new language. data BindL a = RecL Ty [ExpL a] (Scope Int ExpL a) | NRecL Ty [ExpL a] (Scope Int ExpL a) deriving (Eq, Functor, Foldable, Traversable) data ExpL a = VL a | AppL (ExpL a) (ExpL a) | LetL [BindL a] (Scope Int ExpL a) | IfzL (ExpL a) (ExpL a) (Scope () ExpL a) | SucL (ExpL a) | ZeroL deriving (Eq, Functor, Foldable, Traversable) Much here is the same except we’ve romved both lambdas and fixpoints and replaced them with LetL. LetL works over bindings which are either recursive (Fix) or nonrecursive (Lam). Lambda lifting in this compiler is rather simplistic in how it lifts lambdas: we just boost everything one level up and turn λ (x : τ). ... into let foo = λ (x : τ). ... in foo Just like before, this procedure is captured by transforming an ExpC into an ExpL. llift :: Eq a => ExpC a -> Gen a (ExpL a) llift (VC a) = return (VL a) llift ZeroC = return ZeroL llift (SucC e) = SucL <$> llift e llift (AppC f a) = AppL <$> llift f <*> llift a llift (IfzC i t e) = do v <- gen e' <- abstract1 v <$> llift (instantiate1 (VC v) e) IfzL <$> llift i <*> llift t <*> return e' Just like in closConv we start with a lot of very boring and trivial “recurse and build back up” cases. These handle everything but the cases where we actually convert constructs into a LetL. Once again, the interesting cases are pretty much identical. Let’s look at the case for LamC for variety. llift (LamC t clos bind) = do vs <- replicateM (length clos + 1) gen body <- llift $ instantiate (VC . (!!) vs) bind clos' <- mapM llift clos let bind' = abstract (flip elemIndex vs) body return (LetL [NRecL t clos' bind'] trivLetBody) Here we first generate a bunch of fresh variables and unbind the body of our lambda. We then recurse on it. We also have to recurse across all of our closed over arguments but since those are variables we know that should be pretty trivial (why do we know this?). Once we’ve straightened out the body and the closure all we do is transform the lambda into a trivial let expression as shown above. Here trivLetBody is. trivLetBody :: Scope Int ExpL a trivLetBody = fromJust . closed . abstract (const $ Just 0) $ VL () Which is just a body that returns the first thing bound in the let. With this done, we’ve pretty much transformed our expression language to C. In order to get rid of the nesting, we want to make one more simplification before we actually generate C. C-With-Expression C-With-Expressions is our next intermediate language. It has no notion of nested functions or of fixpoints. I suppose now I should finally fess up to why I keep talking about fixpoints and functions as if they’re the same and why this compiler is handling them identically. The long and short of it is that fixpoints are really a combination of a “fixed point combinator” and a function. Really when we say fix x : τ in ... It’s as if we had sayed F (λ x : τ. ...) Where F is a magical constant with the type F :: (a -> a) -> a F calculates the fixpoint of a function. This means that f (F f) = F f. This formula underlies all recursive bindings (in Haskell too!). In the compiler we basically compile a Fix to a closure (the runtime representation of a function) and pass it to a C function fixedPoint which actually calculates the fixed point. Now it might seem dubious that a function has a fixed point. After all, it would seem that there’s no x so that (λ (x : nat). suc x) = x right? Well the key is to think of these functions as not ranging over just values in our language, but a domain where infinite loops (bottom values) are also represented. In the above equation, the solution is that x should be bottom, an infinite loop. That’s why fix x : nat in suc x should loop! There’s actual some wonderful math going on here about how computable functions are continuous functions over a domain and that we can always calculate the least fixed point of them in this manner. The curious reader is encouraged to check out domain theory. Anyways, so that’s why I keep handling fixpoints and lambdas in the same way, because to me a fixpoint is a lambda + some magic. This is going to become very clear in C-With-Expressions (FauxC from now on) because we’re going to promote both sorts of let bindings to the same thing, a FauxC toplevel function. Without further ado, here’s the next IL. -- Invariant: the Integer part of a FauxCTop is a globally unique -- identifier that will be used as a name for that binding. type NumArgs = Int data BindTy = Int | Clos deriving Eq data FauxCTop a = FauxCTop Integer NumArgs (Scope Int FauxC a) deriving (Eq, Functor, Foldable, Traversable) data BindFC a = NRecFC Integer [FauxC a] | RecFC BindTy Integer [FauxC a] deriving (Eq, Functor, Foldable, Traversable) data FauxC a = VFC a | AppFC (FauxC a) (FauxC a) | IfzFC (FauxC a) (FauxC a) (Scope () FauxC a) | LetFC [BindFC a] (Scope Int FauxC a) | SucFC (FauxC a) | ZeroFC deriving (Eq, Functor, Foldable, Traversable) The big difference is that we’ve lifted things out of let bindings. They now contain references to some global function instead of actually having the value right there. We also tag fixpoints as either fixing an Int or a Clos. The reasons for this will be apparent in a bit. Now for the conversion. We don’t just have a function from ExpL to FauxC because we also want to make note of all the nested lets we’re lifting out of the program. Thus we use WriterT to gather a lift of toplevel functions as we traverse the program. Other than that this is much like what we’ve seen before. type FauxCM a = WriterT [FauxCTop a] (Gen a) fauxc :: ExpL Integer -> FauxCM Integer (FauxC Integer) fauxc (VL a) = return (VFC a) fauxc (AppL f a) = AppFC <$> fauxc f <*> fauxc a fauxc ZeroL = return ZeroFC fauxc (SucL e) = SucFC <$> fauxc e fauxc (IfzL i t e) = do v <- gen e' <- abstract1 v <$> fauxc (instantiate1 (VL v) e) IfzFC <$> fauxc i <*> fauxc t <*> return e' In the first couple cases we just recurse. as we’ve seen before. Things only get interesting once we get to LetL fauxc (LetL binds e) = do binds' <- mapM liftBinds binds vs <- replicateM (length binds) gen body <- fauxc $ instantiate (VL . (!!) vs) e let e' = abstract (flip elemIndex vs) body return (LetFC binds' e') In this case we recurse with the function liftBinds across all the bindings, then do what we’ve done before and unwrap the body of the let and recurse in it. So the meat of this transformation is in liftBinds. where liftBinds (NRecL t clos bind) = lifter NRecFC clos bind liftBinds (RecL t clos bind) = lifter (RecFC $ bindTy t) clos bind lifter bindingConstr clos bind = do guid <- gen vs <- replicateM (length clos + 1) gen body <- fauxc $ instantiate (VL . (!!) vs) bind let bind' = abstract (flip elemIndex vs) body tell [FauxCTop guid (length clos + 1) bind'] bindingConstr guid <$> mapM fauxc clos bindTy (Arr _ _) = Clos bindTy Nat = Int To lift a binding all we do is generate a globally unique identifier for the toplevel. Once we have that we that we can unwrap the particular binding we’re looking at. This is going to comprise the body of the TopC function we’re building. Since we need it to be FauxC code as well we recurse on it. No we have a bunch of faux-C code for the body of the toplevel function. We then just repackage the body up into a binding (a FauxCTop needs one) and use tell to make a note of it. Once we’ve done that we return the stripped down let binding that just remembers the guid that we created for the toplevel function. In an example, this code transformers let x = λ (x : τ). ... in ... x ... into TOP = λ (x : τ). ... let x = TOP in ... x ... With this done our language is now 80% of the way to C! Converting To SSA-ish C Converting our faux-C language to actual C has one complication: C doesn’t have let expressions. Given this, we have to flatten out a faux-C expression so we can turn a let expression into a normal C declaration. This conversion is almost a conversion to single static assignment form, SSA. I say almost because there’s precisely one place where we break the single assignment discipline. This is just because it seemed rather pointless to me to introduce an SSA IL with φ just so I could compile it to C. YMMV. This is what LLVM uses for its intermediate language and because of this I strongly suspect regearing this compiler to target LLVM should be pretty trivial. Now we’re using a library called c-dsl to make generating the C less painful, but there’s still a couple of things we’d like to add. First of all, all our names our integers so we have i2e and i2d for converting an integer into a C declaration or an expression. i2d :: Integer -> CDeclr i2d = fromString . ('_':) . show i2e :: Integer -> CExpr i2e = var . fromString . ('_':) . show We also have a shorthand for the type of all expression in our generated C code. taggedTy :: CDeclSpec taggedTy = CTypeSpec "tagged_ptr" Finally, we have our writer monad and helper function for implementing the SSA conversion. We write C99 block items and use tellDecl binding an expression to a fresh variable and then we return this variable. type RealCM = WriterT [CBlockItem] (Gen Integer) tellDecl :: CExpr -> RealCM CExpr tellDecl e = do i <- gen tell [CBlockDecl $ decl taggedTy (i2d i) $ Just e] return (i2e i) Next we have the conversion procedure. Most of this is pretty straightforward because we shell out to calls in the runtime system for all the hardwork. We have the following RTS functions mkZero, create a zero value inc, increment an integer value dec, decrement an integer value apply, apply a closure to an argument mkClos, make a closure with a closing over some values EMPTY, an empty pointer, useful for default values isZero, check if something is zero fixedPoint, find the fixed point of function INT_SIZE, the size of the runtime representation of an integer CLOS_SIZE, the size of the runtime representation of a closure Most of this code is therefore just converting the expression to SSA form and using the RTS functions to shell do the appropriate computation at each step. Note that c-dsl provides a few overloaded string instances and so to generate the C code to apply a function we just use "foo"#[1, "these", "are", "arguments"]. The first few cases for conversion are nice and straightforward. realc :: FauxC CExpr -> RealCM CExpr realc (VFC e) = return e realc (AppFC f a) = ("apply" #) <$> mapM realc [f, a] >>= tellDecl realc ZeroFC = tellDecl $ "mkZero" # [] realc (SucFC e) = realc e >>= tellDecl . ("inc"#) . (:[]) We take advantage of the fact that realc returns it’s result and we can almost make this look like the applicative cases we had before. One particularly slick case is how Suc works. We compute the value of e and apply the result to suc. We then feed this expression into tellDecl which binds it to a fresh variable and returns the variable. Haskell is pretty slick. realc (IfzFC i t e) = do outi <- realc i deci <- tellDecl ("dec" # [outi]) let e' = instantiate1 (VFC deci) e (outt, blockt) <- lift . runWriterT $ (realc t) (oute, blocke) <- lift . runWriterT $ (realc e') out <- tellDecl "EMPTY" let branch b tempOut = CCompound [] (b ++ [CBlockStmt . liftE $ out <-- tempOut]) undefNode ifStat = cifElse ("isZero"#[outi]) (branch blockt outt) (branch blocke oute) tell [CBlockStmt ifStat] return out In this next case we’re translating Ifz. For this we obviously need to compute the value of i. We do that by recursing and storing the result in outi. Now we want to be able to use 1 less than the value of i in case we go into the successor branch. This is done by calling dec on outi and storing it for later. Next we do something a little odd. We recurse on the branches of Ifz but we definitely don’t want to compute both of them! So we can’t just use a normal recursive call. If we did they’d be added to the block we’re building up in the writer monad. So we use lift . runWriterT to give us back the blocks without adding them to the current one we’re building. Now it’s just a matter of generating the appropriate if statement. To do this we add one instruction to the end of both branches, to assign to some output variable. This ensures that no matter which branch we go down we’ll end up the result in one place. This is also the one place where we are no longer doing SSA. Properly speaking we should write this with a φ but who has time for that? :) Finally we build add the if statement and the handful of declarations that precede it to our block. Now for the last case. realc (LetFC binds bind) = do bindings <- mapM goBind binds realc $ instantiate (VFC . (bindings !!)) bind where sizeOf Int = "INT_SIZE" sizeOf Clos = "CLOS_SIZE" goBind (NRecFC i cs) = ("mkClos" #) <$> (i2e i :) . (fromIntegral (length cs) :) <$> mapM realc cs >>= tellDecl goBind (RecFC t i cs) = do f <- ("mkClos" #) <$> (i2e i :) . (fromIntegral (length cs) :) <$> mapM realc cs >>= tellDecl tellDecl ("fixedPoint"#[f, sizeOf t]) For our last case we have to deal with lets. For this we simply traverse all the bindings which are now flat and then flatten the expression under the binder. When we mapM over the bindings we actually get back a list of all the expressions each binding evaluated to. This is perfect for use with instantiate making the actual toplevel function quite pleasant. goBind is slightly less so. In the nonrecursive case all we have to do is create a closure. So goBind of a nonrecursive binding shells out to mkClos. This mkClos is applied to the number of closed over expressions as well as all the closed over expressions. This is because mkClos is variadic. Finally we shove the result into tellDecl as usual. For a recursive call there’s a slight difference, namely after doing all of that we apply fixedPoint to the output and to the size of the type of the thing we’re fixing. This is why we kept types around for these bindings! With them we can avoid dragging the size with every value since we know it statically. Next, we have a function for converting a faux C function into an actual function definition. This is the function that we use realc in. topc :: FauxCTop CExpr -> Gen Integer CFunDef topc (FauxCTop i numArgs body) = do binds <- gen let getArg = (!!) (args (i2e binds) numArgs) (out, block) <- runWriterT . realc $ instantiate getArg body return $ fun [taggedTy] ('_' : show i) [decl taggedTy $ ptr (i2d binds)] $ CCompound [] (block ++ [CBlockStmt . creturn $ out]) undefNode where indexArg binds i = binds ! fromIntegral i args binds na = map (VFC . indexArg binds) [0..na - 1] This isn’t the most interesting function. We have one array of arguments to our C function, and then we unbind the body of the FauxC function by indexing into this array. It’s not explicitly stated in the code but the array contains the closed over expressions for the first n - 1 entries and the nth is the actual argument to the function. This is inline with how the variables are actually bound in the body of the function which makes unwrapping the body to index into the argument array very simple. We then call realc which transforms our faux-c expression into a block of actual C code. We add one last statement to the end of the block that returns the final outputted variable. All that’s left to do is bind it up into a C function and call it a day. Putting It All Together Finally, at the end of it all we have a function from expression to Maybe CTranslUnit, a C program. compile :: Exp Integer -> Maybe CTranslUnit compile e = runGen . runMaybeT $ do assertTy M.empty e Nat funs <- lift $ pipe e return . transUnit . map export $ funs where pipe e = do simplified <- closConv e >>= llift (main, funs) <- runWriterT $ fauxc simplified i <- gen let topMain = FauxCTop i 1 (abstract (const Nothing) main) funs' = map (i2e <$>) (funs ++ [topMain]) (++ [makeCMain i]) <$> mapM topc funs' makeCMain entry = fun [intTy] "main"[] $ hBlock ["call"#[i2e entry]] This combines all the previous compilation passes together. First we typecheck and ensure that the program is a Nat. Then we closure convert it and immediately lambda lift. This simplified program is then fed into fauxc giving a fauxc expression for main and a bunch of functions called by main. We wrap up the main expression in a function that ignores all it’s arguments. We then map realc over all of these fauxc functions. This gives us actual C code. Finally, we take on a trivial C main to call the generated code and return the whole thing. And that’s our PCF compiler. Wrap Up Well if you’ve made it this far congratulations. We just went through a full compiler from a typed higher order language to C. Along the way we ended up implementing A Type Checker Closure Conversion Lambda Lifting Conversion to Faux-C SSA Conversion If you’d like to fiddle a bit more, some fun project might be Writing type checkers for all the intermediate languages. They’re all typeable except perhaps Faux-C Implement compilation to LLVM instead of C. As I said before, this shouldn’t be awful Cheers, var disqus_shortname = 'codeco'; (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 2015-03-24T00:00:00Z

Finding a GHC bug

Planet Haskell - Sun, 03/29/2015 - 06:00
Summary: I found a nasty bug in GHC 7.10 RC3. It's been fixed.For Shake, I have an extensive test suite (2500+ lines of tests). I also test on 7 GHC versions, including GHC HEAD. After adding GHC 7.10 Release Candidate 3 to the mix one of the tests started failing. A week later the bug has been simplified, diagnosed and fixed as bug #10176. Below is a tale of how that happened, including a technical explanation of the bug in Step 8.Step 1: Write a lot of testsThe Shake test that caught this particular bug checks that if the user makes a mistake then the error message must contain certain substrings correctly identifying the problem. With GHC 7.10 RC3 on Travis this test stopped throwing an exception entirely, continuing as though nothing were wrong. Weird.Step 2: Reproduce locallyI tried to reproduce the failure locally, which ended up spotting a fatal bug in the GHC 7.10 RC3 32bit Windows version. After opting for the 64bit version, at first I couldn't reproduce the error. Eventually I realised that you needed to turn on optimisation (at -O1), and that running through ghci (how I usually develop Haskell) didn't cause the problem. Noticing that -O1 was required gave me a clue, that it was related to an optimisation. The typical cause of programs that work without optimisation but fail with it are programs that raise exceptions in pure code (since the exception can change due to optimisations) or those that call unsafePerformIO (it has unsafe in the name for a reason). I certainly do both those things in Shake, but I wasn't aware of anywhere I did them in a dubious manner.Step 3: Reduce the test caseI spent a lot of time trying to reduce the test case. By inserting print statements I narrowed the place the difference was happening to Development.Shake.Core.applyKeyValue, which is a pretty core bit of Shake. However, while I was able to chop out a lot of auxiliary features (lint tracking, command tracing) the actual code remained difficult to reduce to any great extent, for two reasons. Firstly, the bug was incredibly fragile - moving a monomorphic NOINLINE function from one module to another made the bug disappear. Secondly, the applyKeyValue function is right in the middle of Shake, and the test required a few successful Shake runs to set up things for the failing test, so I couldn't change its observable semantics too much.What I did conclude was that Shake didn't seem to be doing anything dodgy in the small patch of code that seemed relevant, giving me the first hint that maybe GHC was at fault, not Shake. Step 4: Differences at the Core levelAt this point, I reached out to the GHC mailing list, asking if anyone had any ideas of a culprit. They didn't, but Simon Peyton Jones suggested finding the smallest breaking change and comparing the generated Core. You can do that by compiling with -ddump-simpl, and adding -dsuppress-all -dsuppress-uniques to get something a bit easier to diff. Fortunately, by this point I had a very small change to make the error appear/disappear (moving a function from one module to another), so the difference in Core was tiny. The change in the problematic version read:case (\_ -> error "here") of {}In GHC Core a case always evaluates its scrutinee until it has the outermost value available (aka WHNF). The empty alternatives mean that GHC has proven that the evaluation always results in an exception. However, a lambda already has a value available (namely the lambda) so evaluation never throws an exception. As a result, GHC has violated the rules of Core and bad things happen.Step 5: Reducing furtherIn order to reduce the bug further I now had a better test, namely:ghc Core.hs -O -ddump-simpl | grep -F "case (\\"With this test I didn't have to keep the internals of Shake working, and in fact didn't even have to provide a runnable entry point - all I had to do was look for the dodgy construction in the Core language. Note that I'm not actually looking for case of a lambda with empty alternatives, reasoning (seemingly correctly) that any case on a lambda with non-empty alternatives would be eliminated by the GHC simplifier, so any case followed by lambda is buggy.I reduced by having a ghcid Window open in one corner, using the warnings -fwarn-unused-binds and -fwarn-unused-imports. I hacked out some part of the program and then patched everything up so it no longer raised an error using ghcid for rapid feedback. I then ran the grep test. If the bug had gone I put the program back to how it was and tried somewhere else. If the bug remained I then cleaned up the now redundant declarations and imports and checked again, repeating until the code was minimal.Several hours later I was left with something like:buggy :: (() -> Bool) -> () -> Bool -> IO ()buggy fun unit bool = runReaderT ( (if bool then liftIO $ print () else p) >> (if fun unit then error2Args unit unit >> p else p)) (){-# NOINLINE error2Args #-}error2Args :: () -> () -> aerror2Args _ _ = error "here"Note that error2Args must be in a different module to buggy.Step 6: BisectingAt this point hvr stepped in and bisected all the changes between GHC 7.10 RC2 and RC3, determining that a large Typeable change introduced the bug in the original shake test case. However, using the minimal program, the bug was also present in GHC 7.10 RC2. That suggested the bug might have been around for a while.Step 7: Augmenting GHC's Lint CheckerGHC already has a pass in the compiler, enabled with -dcore-lint, which checks for dodgy constructs in the Core language. Enabling it didn't pick up this example (hence I used grep instead), so Joachim Breitner added such a check. He also added the example as a test case, so that if it ever breaks in future things it will be spotted immediately.Step 8: Diagnose and FixJoachim then continued to diagnose and fix the issue, the details of which can be found in the patch. The problem (as I understand it) is that GHC looks at the code:fun x = error "foo" xAnd concludes two facts.If fun is called with one argument then the code will raise an error. That's true, and allows the compiler to replace fun () () with fun ().After analysing all calls of fun it spots that fun is always called with two arguments, so it is free to change fun to be fun x y = error "foo" x y.By applying these two facts, we can make the transformation:case fun () () of {}-- apply the first rulecase fun () of {}-- inline fun after applying the second rulecase (\x y -> error "foo" x y) () of {}-- beta reduce:case (\y -> error "foo" () y) of {}Now we have caused invalid Core to be produced. While the two facts are each individually correct, applying the first fact causes the second fact to stop being true. Joachim fixed this by making the call argument count analysis stop at the first argument that guarantees an error.Step 9: The ImpactThe manifestation of the bug is quite interesting. Essentially GHC decides something is an error, but then fails to actually throw the error. As a result, any code the simplifier places after the error call will be eliminated, and that can remove a large chunk of the program. However, any code the simplifier doesn't manage to hoist next to the code will still get run, even though it should have been skipped due to an error. In essence, given exactly the wrong conditions to trigger the bug, you can write:main = do putStrLn "here1" ... error "foo" ... putStrLn "here2" ... putStrLn "here3"And end up with the program printing here1 followed by here3, without throwing an exception. In the case of my original Shake test it started to compile, should have stopped with an error but instead just skipped compiling altogether and went on to do the bits after compiling. A very weird manifestation.Disclaimer: I've eliminating many missteps of mine, which included pushing random patches to try and reduce on the Travis machine and installing a Linux VM. 2015-03-22T22:05:00Z Neil Mitchell noreply@blogger.com

Using Facebook's Flux architectural style for game development in Unity 3D

Planet Haskell - Sun, 03/29/2015 - 06:00
I decided to work again in an old game project. The game is named "Shotem" and the mechanic is quite simple: coins start falling from the sky and you need to "shot them" (got it?). Tap on a coin to shoot it, you gain score if you hit and you lose score if you miss the shot or if a coin falls off the screen (in case you didn't tap it). You have seven bullets to use, each shot (finger tap) consumes a bullet and you need to shake the mobile device to reload your bullets.The game is still a work in progress, but I added the following video in order to show that it actually works in real life:I'll write the history of the development process of this game. It started in a very naive form, then I converted it to Flux style and left it alone for three months. Now I'm coming back to it and had a pleasant surprise to read the code after forgetting about it. I think Flux style made it easy to continue the project were I left it. This post is 100% opinion based. Please, take a seat.The first version I coded was very straightforward. Each coin was a GameObject with rendering and game behavior logic. All game state were inside a Singleton and two other objects were responsible for creating coins and handling user taps. Not organized at all.I was interested in how to code the "reload by shaking" feature. As soon as I got it working, I lost my interest in the game mechanic itself. This happened quite fast actually, Unity 3D has a very nice class to use for dealing with the mobile device gyroscope: Input.gyro.At the same time, I got in touch with Facebook's Flux architectural style. I tried it in some web projects and had a nice feeling about it. It seemed easier to write, maintain and understand code written in Flux style than the code written in MVC fashion. So, I decided to rewrite the code of Shotem in Flux style.At first, it didn't seem to fit into Unity's way of doing things. But I worked it out and coded it anyway. It worked fine, then I left the code alone.Three months later I'm coming back to this project and I didn't remember that I tested Flux style in it. At first I thought: "oh no, I'll need to delete this project and start it over, why did I do it?" Then I did read the code and look at the project structure: I was amazed at how easy it was to get things back on track, I were able to get productive again in less than five minutes! What a pleasant surprise!Now, I feel that I should share this with the rest of the world. I appreciate feedback, so if you feel that using Flux style in game development is madness or if you feel like giving it a try too, leave a comment.From now on, I'll use some terms from Flux, e.g. Store, Dispatcher, Action. I won't explain what are their meanings, so feel free to take a little detour and read the official Facebook's Flux website to get a summary of it.I created a Dispatcher class to register the Stores, dispatch actions, track dependencies between Stores and ensure that the Actions do not cascade. The Dispatcher, in it's full glory, is here:The core game mechanic is encoded in three Stores: CoinStore, handling all coins in the game; GunStore, handling player's ammunition; ScoreStore, tracking user score.Player input may dispatch two Actions in the game: ShootAction and ReloadGunAction. To handle the physics of the game (falling coins), one Action is sent every FixedUpdate: PhysicsUpdateAction.The Stores handle each action according to simple rules:PhysicsUpdateAction is handled by CoinStore by spawning new coins, moving the coins in the screen and removing coins that are off the screen. ScoreStore waits for the CoinStore to finish and then updates the score by decrementing the amount of coins that were removed from CoinStore, because they have fallen off the screen. GunStore ignores this action.ShootAction is handled by GunStore by decrementing player's ammunition. CoinStore waits for the GunStore and ignores the action if no ammunition was used, otherwise it checks for overlapping coins in the shot area and removes them. ScoreStore waits for GunStore and CoinStore then increases the score by each coin removed or decreases the score in case an ammunition was used and no coin was removed.ReloadGunAction is handled by GunStore to reset the player's ammunition to seven. CoinStore and ScoreStore ignores this action.That's the whole game logic. Each Store is observable, the Views register themselves to receive update notifications. When the Store handles an Action that changes its state, it triggers a notification. I've created an abstract class Store to handle this common behavior:The listing below is the code of ScoreStore, the other Stores follow the same style:Setup code is done in a Singleton GameObject's Awake method, I called it StoreHub because I use this to get the reference to the Stores from other Views:ShotemActionGenerator is a helper class to create Actions and send them to Dispatcher, nothing fancy.The View classes are also simple, for example, the game may play three different sound effects when the GunStore is updated: when a bullet is shot, when user tries to shot without ammunition left and when the gun is reloaded:Another view shows the quantity of ammunition remaining, which are just children GameObjects with Renderers that I enable or disable based on the GunStore state:There is a View to show the score, one to show a tip to remind the player to reload the gun when it's empty, another to handle the renderers of each coin visible in the screen, etc. The entire game is made in the same solid base, or may I say "solid flux". Data always flows in a single direction without cascading, there is always an Action that enters the system and triggers something, nothing happens if no Action is dispatched.I don't know if this design can scale to a big game project, as the style as it is now depends on it running in a single core. But, none of my games are that intense, so I will try to finish this game with Flux. I guess that using Flux will also make it easier to create automated tests of the game mechanic, as it is self-contained. Maybe I'll post some follow up thoughts on it.Below is an overview image of the current flux of the game. I decided to call "Inception" the layer that generates the Actions, Flux do not give it a name.Thanks for your time,

Examples of contracts you should not sign

Planet Haskell - Sun, 03/29/2015 - 06:00
Shortly after I posted A public service announcement about contracts Steve Bogart asked me on on Twitter for examples of dealbreaker clauses. Some general types I thought of immediately were: Any nonspecific non-disclosure agreement with a horizon more than three years off, because after three years you are not going to remember what it was that you were not supposed to disclose. Any contract in which you give up your right to sue the other party if they were to cheat you. Most contracts in which you permanently relinquish your right to disparage or publicly criticize the other party. Any contract that leaves you on the hook for the other party's losses if the project is unsuccessful. Any contract that would require you to do something immoral or unethical. A couple of recent specific examples: Comcast is negotiating a contract with our homeowner's association to bring cable Internet to our village; the propsed agreement included a clause in which we promised not to buy Internet service from any other company for the next ten years. I refused to sign. The guy on our side who was negotiating the agreement was annoyed with me. If too many people refuse to sign, maybe Comcast will back out. “Do you think you're going to get FIOS in here in the next ten years?” he asked sarcastically. “No,” I said. “But I might move.” Or, you know, I might get sick of Comcast and want to go back to whatever I was using before. Or my satellite TV provider might start delivering satellite Internet. Or the municipal wireless might suddenly improve. Or Google might park a crazy Internet Balloon over my house. Or some company that doesn't exist yet might do something we can't even imagine. Google itself is barely ten years old! The iPhone is only eight! In 2013 I was on a job interview at company X and was asked to sign an NDA that enjoined me from disclosing anything I learned that day for the next ten years. I explained that I could not sign such an agreement because I would not be able to honor it. I insisted on changing it to three years, which is also too long, but I am not completely unwilling to compromise. It's now two years later and I have completely forgotten what we discussed that day; I might be violating the NDA right now for all I know. Had they insisted on ten years, would I have walked out? You bet I would. You don't let your mouth write checks that your ass can't cash.

A public service announcement about contracts

Planet Haskell - Sun, 03/29/2015 - 06:00
Every so often, when I am called upon to sign some contract or other, I have a conversation that goes like this: Me: I can't sign this contract; clause 14(a) gives you the right to chop off my hand. Them: Oh, the lawyers made us put that in. Don't worry about it; of course we would never exercise that clause. There is only one response you should make to this line of argument: Well, my lawyer says I can't agree to that, and since you say that you would never exercise that clause, I'm sure you will have no problem removing it from the contract. Because if the lawyers made them put in there, that is for a reason. And there is only one possible reason, which is that the lawyers do, in fact, envision that they might one day exercise that clause and chop off your hand. The other party may proceed further with the same argument: “Look, I have been in this business twenty years, and I swear to you that we have never chopped off anyone's hand.” You must remember the one response, and repeat it: Great! Since you say that you have never chopped off anyone's hand, then you will have no problem removing that clause from the contract. You must repeat this over and over until it works. The other party is lazy. They just want the contract signed. They don't want to deal with their lawyers. They may sincerely believe that they would never chop off anyone's hand. They are just looking for the easiest way forward. You must make them understand that there is no easier way forward than to remove the hand-chopping clause. They will say “The deadline is looming! If we don't get this contract executed soon it will be TOO LATE!” They are trying to blame you for the blown deadline. You should put the blame back where it belongs: As I've made quite clear, I can't sign this contract with the hand-chopping clause. If you want to get this executed soon, you must strike out that clause before it is TOO LATE. And if the other party would prefer to walk away from the deal rather than abandon their hand-chopping rights, what does that tell you about the value they put on the hand-chopping clause? They claim that they don't care about it and they have never exercised it, but they would prefer to give up on the whole project, rather than abandon hand-chopping? That is a situation that is well worth walking away from, and you can congratulate yourself on your clean escape. [ Addendum: Steve Bogart asked on Twitter for examples of unacceptable contract demands; I thought of so many that I put them in a separate article. ]
Syndicate content