One day, a disciple of another sect came to Xavier Leroy and said mockingly:
"The OCaml compiler seems very limited: why do you have to indicate when a function is recursive, cannot the compiler infer it?"
Xavier paused for a second, and replied patiently with the following story:
"One day, a disciple of another sect came to Xavier Leroy and said mockingly..."
A novice came to Jacques Garrigue and spoke nervously: "I don't get rank-2 polymorphism. What is it good for? When to use it? How can I understand it?". Jacques asked: "Do you want an answer to each question, or the answer to all your questions?." The novice was enlightened.
The venerable master Leroy was walking with his student. Wishing to start a discussion with his master, the apprentice said "Master, I've heard that all loops must be replaced with tail-recursive functions. Is that true?" Leroy looked commiseratively at his student and replied "Foolish pupil, many tail-recursive functions are merely inefficient loops."
The student spent the next few weeks replacing tail-recursive functions with explicit loops. He finally showed his code to master Leroy, seeking his approval. Leroy hit him with a stick. "When will you learn? Explicit loops are a poor man's tail-recursive functions." At that moment, the student became enlightened.
Anton had been studying the dining philosophers problem and was ecstatic when he presented a novel solution to Damien Doligez. The great master did not show the same enthusiasm, though: all he said was "the solution is not complete". Anton knew that Doligez had written a machine-checked proof of correctness for the concurrent GC he developed in the early 90s for Caml Light, and began to work. After struggling with Coq, he came back to Doligez.
"I have proved that my solution prevents starvation and livelock."
Again, Doligez replied: "the solution is not complete".
Anton retorted: "My correctness proof has been verified mechanically. Moreover, my simulations show that my method allows for a large degree of concurrency, and it's easy to implement efficiently. Surely the solution is complete now?"
The Zen master then explained: "You claim to have solved the dining philosophers problem, yet you haven't expounded where the spaghetti come from."
The great Zen master Pierre Weis came to a novice as he was struggling with compiler error messages. Seeing what he was doing, he uttered severely:
"You cannot just change a couple variance annotations without understanding what is going on and hope it will type."
Pierre proceeded to change a couple variance annotations, and left the instant he finished. The student ran the compiler. The code typed.
Anton was respected and appreciated by the fellow students. He was humble and hard-working, he finished his chores timely and was an applied student. When a disciple of another sect visited the temple, he volunteered to guide him. The ensuing conversation motivated Anton to ask his master permission to accompany the guest back home and learn more from his sources, whose words he reproduced.
"Whoever uttered those words I consider enlightened men.", said the master. "Go forth and come back when you have understood what those wise men have to say."
Anton returned two years later. He only spoke great things about what he had seen and heard, and tried his best to transfer that knowledge to his peers. Anton's behavior, however, became erratic. He plunged into deep meditation in the middle of conversations, could not help waking up late in the morning, and failed to do his chores in a timely manner. Anton himself could not explain the causes. Worried, his companions brought him before his master to inquire about his condition.
Upon hearing the symptoms, the master said:
"You must go back to your strict ways."