We consider a classic “paradox” where a simple inductive proof seems to clash with intuition. Though the proof makes clear that the naive intuition is wrong, it’s hard to pinpoint exactly where the intuition’s logical error is. After discussing the paradox at some length with my family, we came up with an angle of attack that gives an intuitive framework that matches the math and makes clearer why the naive intuition is wrong.
The situation is as follows. Dragons are a perfectly honest and rational species with color vision and either red or blue eyes. One hundred red-eyed dragons are on an island and are sworn to a two-part pact:
- they will not communicate with each other, look at reflections, or otherwise directly find out what color eyes they have, and
- if they can logically deduce some day that they have red eyes, then they will leave the island that night.
The dragons live for years on the island, each of them seeing ninety-nine red-eyed dragons but none of them able to logically deduce that they too have red eyes. One day, a perfectly honest visitor comes to the island, announces that at least one of the dragons has red eyes, and leaves.
If you haven’t heard this before, try to figure out before continuing: what happens?
This post is the third in a series about Dwimiykwim, a Scheme-like language that infers “obvious” dataflow created by Daniel Shaar and I for as a final project for a class. Here I’ll talk about the original motivation for Dwimiykwim, which can be summarized as “whining about typing” (pun not merely intended but essential to the brevity of the summary). While it’s not essential to understand this post, if you’re looking for a description of Dwimiykwim itself, read Episode II, because this post doesn’t even go there.
The chain of ideas that eventually led to Dwimiykwim started with a small annoyance: the arbitrariness of argument order. In Haskell,
map has type
(a -> b) -> [a] -> [b]: it takes a function from
b are any types), then takes a list of
as, and returns a list of
bs, namely the results of applying the given function to each element of the given list. We typically think of
map as a function of two arguments, one a function and the other a list. Haskell, however, has only one-argument functions and uses currying to get the effect of multiple arguments.
The practical implication of currying is that we can partially apply functions by giving only the first few arguments. In this case, we could write
map f for the function that takes in a list and returns
f mapped over that list. However, it’s a bit messier to write the function that, for some fixed list
xs, takes in a function and returns that function mapped over
xs: we have to write
\f -> map f xs.
You can (correctly) call me picky, but this mild clunkiness troubles me deeply.
This post is the second in a series about Dwimiykwim, a Scheme-like language that infers “obvious” dataflow created by Daniel Shaar and I for as a final project for a class. Here I’ll introduce the language itself and go into a few of the more interesting implementation details. For a brief summary of the problem Dwimiykwim tries to solve, see Episode I. Future posts will further discuss the motivation behind Dwimiykwim and walk through a full version of the evaluator example from Episode I.
Dwimiykwim is a superset of a basic subset of Scheme. It adds three features on top of ordinary Scheme:
- madlab procedures, which are procedures that can take their arguments in any order and figure out which argument is which by specifying for each argument a predicate it must satisfy;
- argument inference, which, given a subset of a madlab’s arguments, figures out at runtime what additional arguments to pass;
- and a tag system, which allows any value to be tagged with and tested for any number of symbolic tags without changing the value’s interface (for the most part).
I’ll explain each of these in turn, mostly by giving small examples. If you don’t know Scheme or another Lisp dialect, now’s a good time to skim through this. Once you’ve done that, brace yourselves: parentheses are coming!
Consider the problem of evaluating arithmetic s-expressions like
(* (- 3 5) 4), which would be written \((3-5) \times 4\) in ordinary (infix) notation. A recursive program would do more or less the following.
To evaluate an expression,
if it's a number,
else if it's a binary operation application,
evaluate the left operand,
evaluate the right operand,
figure out what the operation is,
and apply it to the results.
There are lots of details to fill in if we want to get a computer to understand this sketch, but many programmers would be able to turn it into exactly the program I had in mind when I wrote it. There are (at least) two sorts of inferences that bridge the gap between the sketch and a real program:
- “substantial” inferences concerning word definition, such what we mean by
- and “obvious” inferences concerning pronoun resolution, such as what we mean by
I spend an enough-to-consider-grad-school amount of time programming and thinking about programming, and it seemed a little wrong for that to be the case without having any sort of website. By far the easiest way to change this was provided by scripts.mit.edu, so at about 5 o’clock one evening, I ran
ziv@mass-toolpike:~$ add scripts
Welcome to scripts.mit.edu. Which service would you like to use?
1 Begin a Quick-Start autoinstall (wikis, blogs, etc.)
2 Enable the web scripts service
3 Enable the cron scripts service
4 Enable the mail scripts service
5 Sign up for a sql.mit.edu account
Please enter a number 1-5: 1
and, a few minutes later, was the proud admin of this very WordPress blog.