Inside 206-105

Existential Pontification and Generalized Abstract Digressions

Programming Languages

Ott ⇔ PLT Redex

Ott and PLT Redex are a pair of complimentary tools for the working semanticist. Ott is a tool for writing definitions of programming languages in a nice ASCII notation, which then can be typeset in LaTeX or used to generate definitions for a theorem prover (e.g. Coq). PLT Redex is a tool for specifying and […]

  • January 13, 2014

OPLSS lecture notes

I write in from sunny Oregon, where the sun floods into your room at seven in the morning and the Oregon Programming Languages Summer School is in session. So far, it’s been a blast—with lectures covering Coq, Agda, homotopy type theory, linear logic, logical relations—and we’ve still got another week to go! If you were […]

  • July 29, 2013

The single export pattern

From the files of the ECMAScript TC39 proceedings Single export refers to a design pattern where a module identifier is overloaded to also represent a function or type inside the module. As far as I can tell, the term “single export” is not particularly widely used outside the ECMAScript TC39 committee; however, the idea shows […]

  • March 31, 2013

The duality of weak maps and private symbols

From the files of the ECMAScript TC39 proceedings I want to talk about an interesting duality pointed out by Mark Miller between two otherwise different language features: weak maps and private symbols. Modulo implementation differences, they are the same thing! A weak map is an ordinary associative map, with the twist that if the key […]

  • March 19, 2013

What is a membrane?

If you hang out long enough with a certain crowd (in my case, it was the ECMAScript TC39 committee), you will probably hear the term membrane tossed around. And eventually, you will start to wonder, “Well, what is a membrane, anyway?” As is the case with many clever but simple ideas, membranes were first introduced […]

  • March 15, 2013

Generalizing the programmable semicolon

Caveat emptor: half-baked research ideas ahead. What is a monad? One answer is that it is a way of sequencing actions in a non-strict language, a way of saying “this should be executed before that.” But another answer is that it is programmable semicolon, a way of implementing custom side-effects when doing computation. These include […]

  • October 3, 2012

The Y Combinator and strict positivity

One of the most mind-bending features of the untyped lambda calculus is the fixed-point combinator, which is a function fix with the property that fix f == f (fix f). Writing these combinators requires nothing besides lambdas; one of the most famous of which is the Y combinator λf.(λx.f (x x)) (λx.f (x x)). Now, […]

  • September 12, 2012

Practical Foundations for Programming Languages (first impressions)

Robert Harper has (somewhat) recently released a pre-print of a book (PDF) that he has been working on, Practical Foundations for Programming Languages. I downloaded a copy when it initially came out, but I was guilty of putting off actually digging into the book’s 590-some pages. It was only until Harper successfully baited me with […]

  • August 15, 2012

Managing the server/client split in Ur/Web

The holy grail of web application development is a single language which runs on both the server side and the client side. The reasons for this are multifarious: a single language promotes reuse of components that no longer need to be reimplemented in two languages and allows for much more facile communication between the server […]

  • July 25, 2012

How Ur/Web records work and what it might mean for Haskell

Ur is a programming language, which among other things, has a rather interesting record system. Record systems are a topic of rather intense debate in the Haskell community, and I noticed that someone had remarked “[Ur/Web has a http://www.impredicative.com/ur/tutorial/tlc.html very advanced records system]. If someone could look at the UR implementation paper and attempt to […]

  • April 20, 2012