Also, for clarity: the *box type* is the type `α list` (or as we might just say, the `list` type operator); the *boxed type* is some specific instantiation of the free type variable `α`. We'll often write boxed types as a box containing what the free
type variable instantiates to. So if our box type is `α list`, and `α` instantiates to the specific type `int`, we would write:
-<u>int</u>
+<code><u>int</u></code>
for the type of a boxed `int`.
A lot of what we'll be doing concerns types that are called *Kleisli arrows*. Don't worry about why they're called that, or if you like go read some Category Theory. All we need to know is that these are functions whose type has the form:
-P -> <u>Q</u>
+<code>P -> <u>Q</u></code>
That is, they are functions from values of one type `P` to a boxed type `Q`, for some choice of type expressions `P` and `Q`.
For instance, the following are Kleisli arrows:
-int -> <u>bool</u>
+<code>int -> <u>bool</u></code>
-int list -> <u>int list</u>
+<code>int list -> <u>int list</u></code>
In the first, `P` has become `int` and `Q` has become `bool`. (The boxed type <code><u>Q</u></code> is <code><u>bool</u></code>).
Note that the left-hand schema `P` is permitted to itself be a boxed type. That is, where
if `α list` is our box type, we can write the second arrow as
-<u>int</u> -> <u>Q</u>
+<code><u>int</u> -> <u>Q</u></code>
As semanticists, you are no doubt familiar with the debates between those who insist that propositions are sets of worlds and those who insist they are context change potentials. We hope to show you, in coming weeks, that propositions are (certain sorts of) Kleisli arrows. But this doesn't really compete with the other proposals; it is a generalization of them. Both of the other proposed structures can be construed as specific Kleisli arrows.