Here's an easy but useful extract from the thousand-plus user Haskell needs survey.
Using only the v1.0 result set (71% of total respondents) I filtered for only the users who met the following criteria:
- My organization currently uses Haskell in its work = no
- I would recommend Haskell for a project at my workplace = agree or strongly agree
- Current occupation = developer or manager
- More Haskell success stories would make a big difference in our Haskell adoption = agree or strongly agree
Of the 168 matching respondents, on More Haskell success stories would make a big difference in our Haskell adoption (if yes, please elaborate: what are the success stories that would really help?) 72 entered these comments. I hope they inspire you to write up and publish a success story.
- Python and Haskell side-by-side - Transitions from Python to Haskell - GeoSpatial examples
- Application of Haskell in a specific business domain.
- Companies succeeding at large scale with easy deployment (docker?)
- Examples of implementation, integration, speed and ease of development and of course tutorials!
- Examples of several production web apps and APIs
- Examples of telecommunication applications developed in Haskell
- Examples of web paltform for customers.
- Facebook's recent announcement of using Haskell on a rewrite of Sigma is a great example.
- Frontend development
- Haskell in numerical computing Haskell in developing ERP systems
- Haskell in the Enterprise
- High scale Adtech
- Hopefully, large, industrial scale systems, like Sigma, Haxl at Facebook
- I'd like to hear about developer productivity in Haskell and defect counts.
- In the general web apps side.
- Knowing that large companies use it in Industry.
- Mobile and tablet app stories.
- Only as far as it convinced people to learn it.
- Real world systems in rule engines and how haskell makes life simpler there
- Seeing telecom-specific Haskell news could really help
- Success stories around converting dynamically typed web apps to Haskell could help.
- Successful adoption by teams mostly attuned to Java.
- Time to market
- Uncertainty loves company.
- We need more stories that show a strong benefit to training several engineers to use Haskell
- Web apps
- Web related information.
- Yes, absolutely, I always get asked "What is Haskell being used for?".
- lot's more adoption would help developers feeling they should learn
- real world examples in our area "machine construction /graphic industry" should help
- For us to buy into a new language it's good if others in our field are using it successfully. As operations engineers we lean heavily on other open-source projects so having more open-source projects written in Haskell in our field is likely to greatly increase adoption for new projects.
- Both complex software systems in production (there are some examples in finance, but not enough of them) and software products.
- People are always nervous about technology choices, success stories and publicly shared experience always helps
- Any good enterprise use case. Usage of Scala at twitter helped build confidence in Scala. We need something similar. A big enterprise backing makes it easier to convince management and peers.
- We are a fee for servic company so would like to see significantly lower development and deployment costs, helping us be more competitive compared to PHP or other dynamic language developers. Developing cross platform FRP apps on iOS and Android similar to what Facebook are doing with React Native.
- Would need to be showing significantly increased productivity and reliability over C#, which is doing well for us at the moment.
- large scale developement (multi year project ) - high maintanability / evolutive software - parrallel / cloud computing
- No doubt. The same happened with Ruby back in the beginning of Rails. Success stories moved the technology forwards exponentially.
- Go proponents love "we rewrote our Ruby server in Go and now it runs ten times faster with a third the memory and blah blah blah." Or Twitter's Scala stuff. We need something like that. "Social" proof from large companies makes great leverage.
- I blogged about a Haskell success story for my Android app that received a lot of attention and support from the Reddit community. It was a small use case, but it's clear to me that the community is looking for more stories like this.
- One of the big reasons we settled on Python (and Go to a little extent) is that there are a huge number of libraries and tools written in Python that we can make use of. The company is very much on the side of "it's not a differentiator, so we don't want to develop it in-house". There are many awesome Haskell libraries (such as Aeson) that would meet these needs, but seeing web companies successfully using Haskell in production (and talking about how it eases the development process) would really help to convince people of the effectiveness of Haskell (the learning curve is steep, but well worth it).
- Some more confidence in production Haskell deployments and automated testing pipelines would lower the barrier for corporations to accept Haskell. Some larger performance-sensitive web applications using Haskell will also help its perception.
- Success stories in a wide spectrum of industries would be more useful than (say) the finance industry only.
- Specially stories reflecting how easy is to adapt an existing system to new requirements and changes in agile development and TDD.
- Success stories were actually part of what made me take a serious second look at Haskell. I would love to see more success stories from a variety of industries.
- I'd like to see a success story with the tooling, in particular with IDEs :) It is just impossible to sell a "serious" language without it.
- Comparisons of same or equivalent developer or team of developers doing equivalent tasks. Ease of extendability/scalability. Efficiencies in life-cycle of code base maintenance (if any) would be interesting (some people say less code means less bugs, does it really apply?) Does Haskell help agile development? How so? Does Haskell help boost productivity throughout life-cycle of software? How so, any hard data available? How does Haskell integrate with other languages for whole stack development? Does it even belong in a development stack?
- Haskell touts performance/concurrency, so any success stories regarding Haskell project working at very large scales would be valuable.
- Honestly, examples of Haskell, used with strong library/framework support, to build something non-trivial that was commercially successful. I'm sure you guys recognize this, but Haskell's hardest selling point is that its major successes have been in academia.
- A complex and succesful web application using haskell for something other than haskell related stuff would really help.
- Honestly, just a list of like 100 case studies where purity or rich types or functional programming avoided some bug. We are talking about the same bugs in Java, again and again. null pointer exceptions, thread safety, etc.
- I work in banking. If more success stories were known that Haskell works in finances it would go a long way towards spreading it.
- Success stories of big companies (Google, etc), since they can influence the most when it comes to technologies. Once Haskell gets popular, it would make a big difference for my workplace to adopt it or not
- Stories about increase in development speed and cost of development. Stories in the Big Data area.
- I think the stories that would help the most are stories of well known companies successfully moving some services to Haskell (like Facebook, Google, Microsoft, ...)
- Having clients exposed to haskell would surely help. Demonstrating the benefits, especially in the long run, is something to be considered
- I really like Haskell, but I'm an exception to the rule. Most of the other developers I know and/or work with eschew functional programming because they find it too counter-intuitive (i.e., they're set in their imperative ways). As such, I'm not sure how much "success stories" will help sway them.
- I think some big libraries in the style of scikit learn, panda or nltk in Haskell would be a big big plus for us as we use this tools a lot to complement or own tools but we don't have the man power to develop this kind of libraries ourselves.
- Haskell on embedded devices (like handhelds), or sucess stories focusing on quick developer transitions. The problem is really Haskell's reputation of difficulty.
- Fast adoption by company personnel without background using haskell that become productive in a short time
- Hard to find a good example of haskell in any non-obscure industry. An example related to financial data processing would make a huge impact.
- Insights and stories about how using Haskell resulted in fewer bugs, better performance, and faster iteration.
- Yes! The biggest complaint from my bosses (scientists, non-programmers) is that they have never heard of Haskell.
- Examples will include how Haskell helped a non-embedded project (not necessarily web or finance domains) compared to another language in a well known firm.
- Major companies or OSS projects using Haskell, proving that it is more than an academic language and can be used productively in a professional environment.
- When YouTube got popular, everyone started using Python. When Twitter got big, everyone flocked to Ruby On Rails. The Haskell community doesn't really have a big, visible (and, importantly, 'cool') success story like that.
- Specific projects discussed in depth as an example would be of use. Wishy washy a company used this one time does not help
- Not only successful projects built in Haskell, but projects that have no problems finding people happy to work with Haskell and maintain legacy code base.
- Anything that indicates libraries we need would be maintained and not abandoned would be a huge plus.
- I thing more stories showing the bussiness value of switching to Haskell that will be highlighting reduces cost of maintenance, faster prototyping etc. I think we have enough stories to convince developers to use Haskell for hobby projects but we need to convince company to at least try to switch to Haskell.
- In the sector of mechanical engineering it would help to have success stories from this sector. A story which showed that code quality was increased and time to market reduced in the area of PLCs would be handy.
- Success stories from huge companies such as Facebook (Haxl, the Sigma rewrite, etc), financial institutions, governmental institutions. My company handles multi-billion dollar projects that span years to decades, but it also handles projects that can take around six months from start to finish (these are usually customized web projects). Interest in microservices is growing, for which Haskell seems a very nice fit.
[link] [23 comments]
I usually Google to find documentation on Hackage, and I have 10-20 Hackage tabs open at a time. This is pretty slow, but I haven't found anything better.
How do other people browse documentation?submitted by anon_c
[link] [19 comments]
Here is the code https://bpaste.net/show/ea9c9b525b1d
I asked about this in IRC, where some one told me that it was not possible, but can make it work using some 'clever tricks'. I worked on it some more and made this,
which works as expected. I asked about these again in the IRC when someone else told me that it does not obey the Monad laws. so cannot work with composition. He also suggested changing the type signature and add a new function.
showReturn :: (Show a) => a -> Writer a showReturn x = Writer ("I got: " ++ show x) x
So I tried doing this http://lpaste.net/133284 , but didn't work. I couldn't ask the guy because he got disconnected..
Can you tell me if what I originally inteded to do with https://bpaste.net/show/ea9c9b525b1d is possible with actual Monads. The guy from irc also told me that one can make the second version, https://bpaste.net/show/717d1572d053, to work with do notation using overloading 'do'. How is this done?
Thank you.submitted by yet-i
[link] [2 comments]
Hey Guys, I've been going through Learn You a Haskell, and to challenge myself, I've been trying to implement every function the author uses/talks about that he never explicitly says how to write. However, this has been taking quite a while, especially with the modules chapter, and I was wondering if there are diminishing returns to this approach. Should I keep on doing this and reap the benefits later, or just read through and move quicker to actual projects/harder stuff?submitted by uncountableB
[link] [11 comments]
The newer languages gaining popularity have cool names: Swift, Scala, Go, Rust, Elixir.
If Haskell were named something fun like Rad or Beem all the cool kids would use it.submitted by srbufi
[link] [10 comments]
Hey. I've been working on this for a short while so I thought I'd share. It's currently nowhere near usable but if you're feeling adventerous, you might like giving it a shot.
There's a shortish blog post about it here http://lukahorvat.github.io/programming/2015/05/24/haskellforms/
You might need the F# redistributable (maybe try this link: https://www.microsoft.com/en-us/download/details.aspx?id=44941) I'm not sure because I don't have a PC without VS handy.
Oh, btw. The way I test it is by running cabal repl, then startHost False (you'll be asked if you want to debug with VS, I'm not sure what happens if you don't have it), then main.submitted by Darwin226
[link] [8 comments]
I've made a script that asks the user a questionnaire and stores the results in a csv file. Just meant for self-monitoring.
I'd appreciate any all all feedback. In particular, I'm looking for better ways of...
- storing the questions themselves (currently individual functions in Questions.hs)
- creating the instances FromNamedRecord, FromRecord, ToRecord, etc for Answer
- asking the questions in the function ask
In general I want to use the named records, and have a header in the csv file, but I haven't been able to figure out to do it. I think it's very tedious to write the header manually/explicitely, I'd like to be able to have one automatically generated from the record defintion of Answer (same thing I'd want for the instances mentioned above). How can this be acheived?submitted by jarlg
[link] [2 comments]
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.