I've only really heard people complaining about Cabal. Surely we could all agree to use (and develop if necessary) some other tool? Why keep using Cabal? What should we use instead?
Edit: or just work to improve Cabal! That's probably the best option (yes, I know there are people working on it right now, but perhaps be more radical)
Edit 2: a lot of people seem upset about the title of this post! I can't change it, but I apologize. Not everybody hates Cabal - in fact it looks like the majority is okay with it. Honestly, this post wasn't intended to be a jab at Cabal, but to explore what its problems are, and possible solutions for those problems.submitted by Alyte
[link] [92 comments]
I've been given the opportunity to develop a small piece of code (with future expansion if it goes well) in any language of choice. This piece of code is meant to build a RESTful API within a microservice framework. Should I use Haskell for this and if so, what is the best way of integrating Haskell into the project? Keep in mind that I'm pretty new to Haskell myself and am trying to show to the hardcore Java developers that this is a real alternative. Frameworks and best practices would be appreciated as well.submitted by haskelldrone
[link] [77 comments]
A powerful feature of Haskell’s type system is that we can deduce properties of functions by looking only at their type. For example, a function of typef :: ∀a. a -> a
can only be the identity function: since it must return something of type a, for any type a, the only thing it can do is return the argument of type a that it was given (or crash). Similarly, a function of typef :: ∀a. a -> a -> a
can only do one of two things: either return the first argument, or return the second. This kind of reasoning is becoming more and more important with the increasing use of types such as this definition of a “lens”:type Lens s t a b = forall f. Functor f => (a -> f b) -> s -> f t
Since a lens is just a function of a particular type, the only thing we can conclude about such a function is whatever we can deduce from its type.
To reason about the properties of functions based only on their types we make use of the theory of parametricity, which tells how to derive a so-called “free theorem” from a type. This blog post is a tutorial on how to do this; it won’t explain why the theory works, only how it works. A Haskell practitioner’s guide to parametricity, if you will.
This is a two-part blog post. In part 1 (this post) we will cover the basics: constant types, functions and polymorphism (over types of kind *).
In part 2 (to be published shortly) we will deal with more advanced material: type constructor (types of kind * -> *), type classes, polymorphism over type constructors and type constructor classes.The Basics
The main theorem of parametricity is the following:if f :: t then f ℛ(t) f
When t is a closed type, ℛ(t) is a relation between two terms of type t (we shall see later that the type of ℛ is actually slightly more general). In words, parametricity states that any term f of type t is related to itself by ℛ(t). Don’t worry if this all looks incredibly abstract! We shall see lots and lots of examples.Constant types (types of kind *)
For any constant type C, the relation ℛ(C) is the identity relation. In other words,x ℛ(C) x' iff x ≡ x'
(We will use ≡ throughout to mean mathematical equality, to distinguish it from Haskell’s equality function (==).)
Let’s see an example. Suppose that x :: Int. Then parametricity tells us thatx ℛ(Int) x iff x ≡ x
I.e., it tells us that x is equal to itself. Not very insightful! Intuitively, this makes sense: if all we know about x is that it is an integer, we cannot tell anything about its value.
TOOLING. Many of the examples in this blog post (though sadly not all) can also be auto-derived by one of two tools. On the #haskell IRC channel we can ask lambdabot to derive free theorems for any types not involving type classes or type constructor classes. If you ask@free x :: Int
lambdabot will reply withx = x
(I recommend starting a private conversation with lambdabot so you avoid spamming the whole #haskell channel.)Alternatively, you can also try the online free theorem generator. This free theorem generator is a bit more precise than lambdabot (which takes some shortcuts sometimes), and supports type classes, but cannot work with type constructors (lambdabot can work with unknown type constructors but not with quantification over type constructors, unfortunately). Functions
For functions we map related arguments to related results:f ℛ(A -> B) f' iff forall x, x'. if x ℛ(A) x' then f x ℛ(B) f' x'
(The types of x and x' here depend on what precisely A is; see The type of ℛ, below.)
Example. Suppose f :: Int -> Bool. By parametricityf ℛ(Int -> Bool) f iff forall x :: Int, x' :: Int. if x ℛ(Int) x' then f x ℛ(Bool) f x' -- both Int and Bool are constant types iff forall x :: Int, x' :: Int. if x ≡ x' then f x ≡ f x' -- simplify iff f ≡ f
Again, not very informative. Parametricity doesn’t tell us anything about functions between constant types. Time to look at something more interesting!Polymorphism (over types of kind *)
The definition for polymorphic values isf ℛ(∀a. t) f' iff forall A, A', a :: A ⇔ A'. f@A ℛ(t) f'@A' -- where 'a' can occur free in t
That is, whenever we pick two types A and A', and some relation a between A and A', the function f@A obtained by instantiating the type variable by A must be related to the function f'@A' obtained by instantiating the type variable by A'. In what follows we will write explicit type instantiation like this only if the type is not clear from the context; specifically, we will omit it when we supply arguments to the function.
The type of ℛ.
∀ab. a -> b -> a is an example of a closed type: all type variables are bound by a universal quantifier. An open type is a type with free type variables such as ∀b. a -> b -> a or even a -> b -> a. (Note that this distinction is harder to see in Haskell where universal quantifiers are often implicit. We will not follow that convention in this article.)
We said in the introduction that if t is a closed type, ℛ(t) relates two terms of type t. As we saw, in order to be able to give a meaning to open types we need a mapping from any free variable a to a relation a :: A ⇔ A'. In this article we somewhat informally maintain this mapping simply by using the same name for the type variable and the relation.Given two relations a :: A ⇔ A' and b :: B ⇔ B', ℛ(a -> b -> a) relates terms of type A -> B -> A with terms of type A' -> B' -> A'. It is important to realize that ℛ can therefore relate terms of different types. (For a more precise treatment, see my Coq formalization of a part of this blog post.)
The interpretation of ℛ for a free type variable a is defined in terms of the corresponding relation:x ℛ(a) x' -- the type variable iff (x, x') ∈ a -- the relation Example: ∀a. a -> a
Let’s consider a number of examples, starting with an f :: ∀a. a -> a:f ℛ(∀a. a -> a) f -- parametricity iff forall A, A', a :: A ⇔ A'. f@A ℛ(a -> a) f@A' -- definition for function types iff forall A, A', a :: A ⇔ A', x :: A, x' :: A'. if x ℛ(a) x' then f x ℛ(a) f x'
It might not be immediately evident from the last line what this actually allows us to conclude about f, so let’s look at this a little closer. A function g is a special kind of relation, relating any argument x to g x; since the property holds for any kind of relation a : A ⇔ A', it must also hold for a function a⃯ :: A -> A':forall x, x'. if x ℛ(a⃯) x' then f x ℛ(a⃯) f x' -- x ℛ(a⃯) x' iff a⃯ x ≡ x' iff forall x :: A, x' :: A'. if a⃯ x ≡ x' then a⃯ (f x) ≡ f x' -- simplify iff forall x :: A, a⃯ (f x) ≡ f (a⃯ x)
We can apply this result to show that any f :: ∀a. a -> a must be the identity function: picking a⃯ = const x, we get const x (f x) ≡ f (const x x), i.e. x ≡ f x, as required.NOTE. We are doing fast and loose reasoning in this tutorial and will completely ignore any totality issues. See Automatically Generating Counterexamples to Naive Free Theorems, or the associated web interface, for some insights about what wrong conclusions we can draw by ignoring totality. Example: ∀a. a -> a -> a
Intuitively, there are only two things a function f :: ∀a. a -> a -> a can do: it can either return its first argument, or it can return its second argument. What does parametricity tell us? Let’s see:f ℛ(∀a. a -> a -> a) f iff forall A, A', a :: A ⇔ A'. f@A ℛ(a -> a -> a) f@A' -- applying the rule for functions twice iff forall A, A', a :: A ⇔ A', x :: A, x' :: A', y :: A, y' :: A'. if x ℛ(a) x', y ℛ(a) y' then f x y ℛ(a) f x' y'
Let’s again specialize the last line to pick a function a⃯ :: A -> A' for the relation a:forall x :: A, x' :: A', y :: A, y' :: A'. if x ℛ(a⃯) x', y ℛ(a⃯) y' then f x y ℛ(a⃯) f x' y' -- a⃯ is a function iff forall x :: A, y :: A. if a⃯ x ≡ x' and a⃯ y ≡ y' then a⃯ (f x y) ≡ f x' y' -- simplify iff a⃯ (f x y) = f (a⃯ x) (a⃯ y)
So parametricity allows us to “push in” or “distribute” a⃯ over f. The fact that f must either return its first or its second argument follows from parametricity, but not in a completely obvious way; see the reddit thread How to use free theorems.Example: ∀ab. a -> b
Other than undefined (which we are ignoring), there can be no function f :: ∀ab. a -> b. Let’s suppose that one did exist; what does parametricity tell us?f ℛ(∀ab. a -> b) f -- applying the rule for universal quantification, twice iff forall A, A', B, B', a :: A ⇔ A', b :: B ⇔ B'. f@A,B ℛ(a -> b) f@A',B' -- applying the rule for functions iff forall A, A', B, B', a :: A ⇔ A', b :: B ⇔ B', x :: A, x' :: A'. if x ℛ(a) x' then f x ℛ(b) f x'
Picking two functions a⃯ :: A -> A' and b⃯ :: B -> B' for a and b, we getb⃯ . f = f . a⃯
It’s not too difficult to derive contradiction from this (remember that you can pick any two functions a⃯ and b⃯ between any types of your choosing). Hence, such a function cannot exist.Example: ∀ab. (a -> b) -> a -> b
The only thing a function of this type can do is apply the supplied function to the supplied argument (alternatively, if you prefer, this must be the identity function). Let’s spell this example out in a bit of detail because it is our first example of a higher order function.f ℛ(∀ab. (a -> b) -> a -> b) f -- apply rule for polymorphism, twice iff forall A, A', B, B', a :: A ⇔ A', b :: B ⇔ B'. f@A,B ℛ((a -> b) -> a -> b) f@A',B' -- apply rule for functions, twice iff forall A, A', B, B', a :: A ⇔ A', b :: B ⇔ B'. forall g :: A -> B, g' :: A' -> B', x :: A, x' :: A'. if g ℛ(a -> b) g' and x ℛ(a) x' then f g x ℛ(b) f g' x'
Let’s expand what that premise g ℛ(a -> b) g' means:g ℛ(a -> b) g' iff forall y :: A, y' :: A'. if y ℛ(a) y' then g y ℛ(b) g' y'
For the special case that we pick functions a⃯ :: A -> A' and b⃯ :: B -> B' for a and b, that premise collapses toforall y :: A, y' :: A'. if y ℛ(a⃯) y' then g y ℛ(b⃯) g' y' -- a⃯ and b⃯ are functions iff forall y :: A, y' :: A'. if a⃯ y ≡ y' then b⃯ (g y) ≡ g' y' -- simplify iff forall y :: A. b⃯ (g y) ≡ g' (a⃯ y) -- simplify (extensionality) iff b⃯ . g ≡ g' . a⃯
So that the free theorem for f :: ∀ab. (a -> b) -> a -> b becomesif b⃯ . g ≡ g' . a⃯ then b⃯ . f g ≡ f g' . a⃯
Picking b⃯ = const g, g' = g, and a⃯ = id (verify that the premise holds) we get that indeed g ≡ f g, as expected.
Useful shortcut. This pattern is worth remembering:g ℛ(a⃯ -> b⃯) g' iff b⃯ . g ≡ g' . a⃯ whenever a⃯ and b⃯ are function(al relation)s. Example: ∀ab. (∀c. c -> String) -> a -> b -> String
A function f :: ∀ab. (∀c. c -> String) -> a -> b -> String is not only higher order, but has a rank-2 type: it insists that the function it is given is itself polymorphic. This makes it possible to write, for examplef g x y = g x ++ g y
Note that since x and y have different types, it is important that g is polymorphic. What is the free theorem for f?f ℛ(∀ab. (∀c. c -> String) -> a -> b -> String) f -- apply rule for polymorphism, twice iff forall A, A', B, B', a :: A ⇔ A', b :: B ⇔ B'. f ℛ((∀c. c -> String) -> a -> b -> String) f -- apply rule for functions three times, and simplify ℛ(String) to (≡) iff forall A, A', B, B', a :: A ⇔ A', b :: B ⇔ B'. forall g :: ∀c. c -> String, g' :: ∀c. c -> String. forall x :: A, x' :: A', y :: B, y' :: B'. if g ℛ(∀c. c -> String) g', x ℛ(a) x', y ℛ(b) y' then f g x y ≡ f g' x' y'
Specializing this theorem to functions a⃯ :: A -> A' and b⃯ :: B -> B' we getforall A, A', B, B', a⃯ :: A -> A', b⃯ :: B -> B'. forall g :: ∀c. c -> String, g' :: ∀c. c -> String. forall x :: A, y :: B. if g ℛ(∀c. c -> String) g' then f g x y ≡ f g' (a⃯ x) (b⃯ y)
But that is somewhat surprising, because it seems to say that the values of x and y cannot matter at all! What is going on? Expanding the first premise:g ℛ(∀c. c -> String) g' iff forall C, C', c :: C ⇔ C', g ℛ(c -> String) g' iff forall C, C', c :: C ⇔ C', z :: C, z' :: C'. if z ℛ(c) z' then g z = g' z'
Let’s stop for a moment to ponder what this requirement for g and g' really says: given any relation c, and any elements z and z' that are related by c—in other words, for any z and z' at all—we must have that g z and g' z' give us equal results. This means that g and g' must be constant functions, and the same constant function at that. As a consequence, for any function f of the above type, f g must itself be constant in x and y. In part two we will see a more useful variation which uses the Show type class.
Incidentally, note that this quantification over an arbitrary relation c is a premise to the free theorem, not a conclusion; hence we cannot simply choose to consider only functions c.
TOOLING. Indeed, if you enter(forall c. c -> String) -> a -> b -> String in the online free theorem generator you will see that it first gives the free theorem using relations only, and then says it will reduce all “permissible” relation variables to functions; in this example, that is all relations except for c; lambdabot doesn’t make this distinction and always reduces relations to functions, which is not correct. To be continued
In part 2 (to be published shortly) we will cover type constructors, type classes and type constructor classes. Meanwhile, here are some links to papers on the subject if you want to read more.
- Theorems for free! by Philip Wadler is the seminal paper on the topic. It doesn’t however cover general type classes, higher types, or type constructors.
- Type-safe cast does no harm: Syntactic parametricity for Fω and beyond by Dimitrios Vytiniotis and Stephanie Weirich is a more theoretical paper about free theorems in a calculus with higher rank types and representation types.
I have a new academic/professional website: http://cl.indiana.edu/~wren/!
There are still a few unfinished areas (e.g., my publications page), but hopefully I'll be finished with them shortly. The new site it built with Hakyll instead of my old Google-Summer-of-Code static website generator. I'm still learning how to implement my old workflow in Hakyll, and if I get the chance I'll write a few posts on how I've set things up. Reading through other folks' posts on how they use Hakyll have been very helpful, and I'd like to give back to the community. I've already issued a pull request for adding two new combinators for defining template fields.
In the meantime, if you notice any broken links from my old blog posts, please let me know.
The Commercial Haskell SIG members want to help people adopt Haskell. What would help? Data beats speculation, so FP Complete recently emailed surveys to over 16000 people interested in Haskell. The questions were aimed at identifying needs rather than celebrating past successes, and at helping applied users rather than researchers.
Over 1240 people sent detailed replies, spending over 250 person-hours to provide their answers.
This rich data set includes extensive information on Haskell user needs. We are open-sourcing the entire anonymized data set, downloadable by clicking here [.zip]. There are numeric ratings and extensive textual comments. Feel free to analyze the data -- or just read the summaries -- and share your most helpful and actionable conclusions with the community. We will too.First Results
Although we have completed only basic analysis, here are some of our first findings -- those so clear that they show up on even the most basic examination of the aggregate data.
- Satisfaction with the language, the compiler, and the community are high.
- Among non-students, 58% would recommend Haskell for a project at their workplace, but only 26% actually use it at work -- partly due to colleagues unfamiliar with Haskell who see it as requiring skills that are hard to obtain, or who need to see more success stories. Would improvement to colleagues' perceptions make a difference in the team's choice of Haskell for a project? 33% of respondents rated this "crucial" and another 26% said it would be "important", while only 16% said it would be a "slight help" or no help.
- Package management with cabal is the single worst aspect of using Haskell. Asked if improvements to package management would make a difference to their future choice of Haskell for a project, 38% said it would be "crucial" and a further 29% said it would be "important". Comments connected cabal with words like hell, pain, awful, sucks, frustrating, and hideous. Only this topic showed such grave dissatisfaction.
- Documentation improvements are a very high priority. For example, users need more concrete tutorials and templates showing them exactly what kinds of problems Haskell is good at solving, and exactly how to implement such programs completely. 65% of respondents said improvements to documentation and learning resources would be crucial or important, and a further 23% said they would be helpful. However, comments did not begin to approach the level of concern seen with cabal.
- Skills are a priority. Users need to see that people with Haskell skills are readily available, and that Haskell skills are quite feasible to learn. A majority of respondents said an improvement in availability of skilled personnel would make an important or crucial difference to them, and many also expressed concern about their or colleagues' abilities to learn the needed concepts and skills.
We have started deeper statistical analysis of the data, and we hope that some readers of this post will perform -- and share -- even better analyses than we can. New issues may become clearer by clustering or segmenting users, or through other statistical techniques. Also, we may find more clarity about needs through deeper study of textual responses. Follow-up studies are also a possibility.
We propose that the community, given this large and detailed data set, should set some of its priorities in a data-driven manner focused on user-expressed needs. This effort should be complementary to the ongoing research on issues of historic Haskell strength such as language design and runtime architecture.Areas for Further Work
We request that useful findings or insights derived from the open-sourced data set be shared with the community, including attribution of the source of the data and the methods of analysis used.
The data collected strongly invites clustering or segmentation, so as to identify needs of different sub-populations. FP Complete has already begun one such study.
The data collected includes extensive textual remarks which should be studied by knowledgeable people for insights. Automated text analysis methods may also be applicable.
Cost-benefit analysis seems worthwhile: based on identified needs, what improvements would help the most people, to the greatest degree, at the least cost and/or the least delay? A method to match volunteer contributors with identified high-payoff projects also seems worthwhile.
It would be useful to merge the data from versions 0.1 and 0.2 with version 1.0 of the survey, since 1.0 includes only 71% of the total answers received. Differences between the questions and scales make this a nontrivial, but still realistic, goal.
If important new hypotheses require testing, or if further detail is needed, we intend to conduct follow-up research at some future date among users who volunteered their email addresses for follow-up questions.
A future repeat survey could determine which improvement efforts are successful.Methodology Notes
This was not a survey of the general public, but of a population motivated to provide feedback on Haskell. Invitees included 16165 non-opted-out email addresses gathered from FP Complete's website, in randomized order. Due to privacy considerations this list will not be published, but FP Complete was able to use it to contact these users since the survey was directly related to their demonstrated interest in Haskell. The high quality of the list is reflected in the extremely high response rate (7.7%), the low bounce rate (1.9%), and the low unsubscribe rate (also 1.9%).
Surveys were conducted using SurveyGizmo.com, with an email inviting each participant to click a link to a four-page Web-based survey. Survey form 0.1 invitations went to 1999 users of whom 190 completed the survey. Survey form 0.2, incorporating some edits, went to 2000 users of whom 170 completed the survey. Survey form 1.0, incorporating further edits, went to 12166 users of whom 894 completed the survey.
Form 0.2 incorporated edits to eliminate questions yielding little information about how to help users, either because satisfaction was very high (the language itself, the compiler, the community) or because two questions were redundant. Also, new questions inspired by textual responses to form 0.1 were included.
Form 1.0 incorporated further such edits. Also, the rating scale was changed to ask about helping the user's (and team's) future choice of Haskell rather than current usefulness/difficulty. The ratings questions were displayed under the heading "Would improvements help you and your group to choose Haskell for your future work?"
Responses were processed anonymously, but users were given the option to fill in their email address if they would accept follow-up questions, and the option to name their company/organization. Users were informed that the survey results, without these fields, would be shared with the community.Acknowledgments
We are grateful to the many, many people who spent their valuable time and expertise completing and returning their survey forms. Thanks to Dr. Tristan Webb and Ms. Noelle McCool-Smiley, both of FP Complete, for their material help in formulating and conducting the survey. Thanks to FP Complete's corporate customers for providing the revenues that allow us to fund this and other community projects. Thanks to the Commercial Haskell SIG for providing the motivation behind this project. Thanks to the many volunteers who've spent absolutely huge amounts of time and expertise making Haskell as good as it is today, and who continue to make improvements like those requested by the survey participants. Thanks to the companies that allow some of their staff to spend company time making such contributions to the common good. Special thanks to the late Professor Paul Hudak; may we all strive to live up to his example.