> If you expect people to understand the theory, this is also a UI problem in a different way.
I don't really understand what you mean by "theory", you don't need to know /any/ PL theory to write Haskell and you certainly don't need to know mathematics. What specific ideas are you referring to that require advanced knowledge as a prerequisite for doing day-in-day-out programming tasks in Haskell?
Again, you have to be able to perform the same computation as the type inference algorithm - for any inference engine, any type system, any language, you can't use it if you don't know what it's going to do.
There are a lot of different ways of handling this problem in Haskell - some involve knowing the notations and results of the branch of math called "PL theory," some don't.
As UIs, they all have drawbacks - and we know this, because you and I both know all the ways Haskell is awesome and rocks. We also know what people say when they complain about Haskell. They're complaining about exactly this material - so why not take the customer at his word?
> for any inference engine, any type system, any language, you can't use it if you don't know what it's going to do.
My whole argument is that you don't need to know anything about the implementation of the inferencer to use it, you don't need to predict it's behavior anymore than you need to model the CPU instruction selection of the compiler in your head. Most of the time you can safely program at a level of abstraction that doesn't involve the implementation of the language, and in Haskell this "normal level" is well above the level that involves low-level things like the lambda calculus.
I think we're just an impasse, the meme that you need mathematics or PL theory to program in Haskell is one that puzzles me and I don't understand where it comes from. Best of luck on your project.
I'm not sure it's realistic to say someone could make a career in a programming language without being able to look at a function and deduce the static type of a value without asking the computer.
As I wrote elsewhere in the comments:
I don't know HM too well, but it seems to have more in common with the dataflow analysis algorithms in optimizers and verifiers -- which programmers don't usually have to understand -- than the basic unidirectional type inference that already serves pretty well to reduce redundancy in the source code.
I could imagine citing C++ as a counterargument -- no one understands the type system, but people use the language anyway -- but it's still not an abstraction you don't have to understand to use, like a CPU.