April | 2014 | Existential Type
2 posts published by Robert Harper during April 2014| Existential Type
2 posts published by Robert Harper during April 2014| Existential Type
I recently thought of a nice way to structure a language for parallel programming around the concept of sequential composition. Think of parallelism as the default—evaluate everything in parallel unless the semantics of the situation precludes it: sums are posterior to summands, but the summands can be evaluated simultaneously. You need a way to express […]| Existential Type
It is well-known that constructivists renounce “proof by contradiction”, and that classicists scoff at the critique. “Those constructivists,” the criticism goes, “want to rule out proofs by contradiction. How absurd! Look, Pythagoras showed that the square root of two is irrational by deriving a contradiction from the assumption that it is rational. There is nothing wrong […]| Existential Type
PCLSRING is an operating system kernel design technique introduced in ITS for managing interruptions of long-running synchronous system calls. It was mentioned in an infamous diatribe by Dick Gabriel, and is described in loving detail by Allen Bawden in an article for the ages. Discussions of PCLSRING usually center on fundamental questions of systems design. Is the […]| Existential Type
I am building a web page devoted to the 2nd edition of Practical Foundations for Programming Languages, recently published by Cambridge University Press. Besides an errata, the web site features a commentary on the text explaining major design decisions and suggesting alternatives. I also plan to include additional exercises and to make sample solutions available to […]| Existential Type
A recent discussion of introductory computer science education led to the topic of teaching recursion. I was surprised to learn that students are being taught that recursion requires understanding something called a “stack” that is nowhere in evidence in their code. Few, if any, students master the concept, which is usually “covered” only briefly. Worst, they […]| Existential Type
Exception tracking is a well-known tar baby of type system design. After all, if expressions can have two sorts of result, why shouldn’t the type say something about them both? Languages such as CLU, FX, and Java, to name three, provide “throws” or “raises” clauses to the types of procedures that specify an upper bound […]| Existential Type
For decades my colleague, Guy Blelloch, and I have promoted a grand synthesis of the two “theories” of computer science, combinatorial theory and logical theory. It is only a small exaggeration to say that these two schools of thought work in isolation. The combinatorial theorists concern themselves with efficiency, based on hypothetical translations of high-level algorithms […]| Existential Type
So far I’ve ignored the back and forth on the Scottish referendum on secession from the United Kingdom, but this weekend I decided that it was past time for me to sort it out. For those of you who don’t know me, I’ll mention that I lived for 3.5 years in Scotland quite some time […]| Existential Type
Having just returned from the annual Oregon Programming Languages Summer School, at which I teach every year, I am once again very impressed with the impressive growth in the technical sophistication of the field and with its ability to attract brilliant young students whose enthusiasm and idealism are inspiring. Eugene was, as ever, an ideal […]| Existential Type
Everyone who has studied algorithms has wondered “why the hell is Bellman’s memorization technique called dynamic programming?”. I recently learned the answer from my colleague, …| Existential Type
I recently thought of a nice way to structure a language for parallel programming around the concept of sequential composition. Think of parallelism as the default—evaluate everything in parallel unless the semantics of the situation precludes it: sums are posterior to summands, but the summands can be evaluated simultaneously. You need a way to express the necessary dependencies without introducing any spurious ones.| Existential Type
A popular meme in the world of PL’s is that “Haskell has monads”, with the implication that this is a distinctive feature of the language, separate from all others. While it is t…| Existential Type
While reviewing some of the comments on my post about parallelism and concurrency, I noticed that the great fallacy about dynamic and static languages continues to hold people in its thrall. So, i…| Existential Type
