The constructive lift monad is the coinductive type $T(A) \equiv \nu\alpha.\; A + \alpha.$
The intuition is that an element of this type either tells you a value of type $A$, or tells you to compute some more and try again. Nontermination is modeled by the element which never returns a value, and always keeps telling you to compute some more.
Our goal is to construct a general fixed-point combinator $\mu(f : TA \to TA) : 1 \to TA$, which takes an $f$ and then produces a computation corresponding to the fixed point of $f$. To fix notation, we'll take the constructors to be:
$$
\begin{array}{lcl}
\mathsf{roll} & : & A + TA \to TA \\
\mathsf{unroll} & : & TA \to A + TA
\end{array}
$$
Since this is a coinductive type, we also have an unfold satisfying the following equation:
$$
\mathsf{unfold}(f : X \to A + X) : X \to TA \equiv \mathsf{roll} \circ (\mathit{id} + (\mathsf{unfold}\; f)) \circ f
$$
First, we will explicitly construct the bottom element, corresponding to the computation that runs forever, with the following definition:
$$
\bot : 1 \to TA \equiv \mathsf{unfold}(\mathsf{inr})
$$
This definition just keeps telling us to wait, over and over again. Now, we can define the fixed point operator:
$$
\begin{array}{l}
\mu(f : TA \to TA) : 1 \to TA \\
\mu(f) \equiv (\mathsf{unfold} (\mathsf{unroll} \circ f)) \circ \bot
\end{array}
$$
What this does is to pass bottom to $f$. If $f$ returns a value, then we're done. Otherwise, $f$ returns us another thunk, which we can pass back to $f$ again, and repeat.
Of course, this is exactly the intuition behind fixed points in domain theory. Lifting in domains is usually defined directly, and I don't know who invented the idea of defining it as a coinductive type. I do recall a 1999 paper by Martin Escardo which uses (a slight variant of) it, and he refers to it as a well-known construction in metric spaces, so probably the papers from the Dutch school of semantics are a good place to start the search. This construction has seen a renewed burst of interest in the last few years, since it offers a relatively convenient way to represent nonterminating functions in dependent type theory. It's also closely related to step-indexed models in operational semantics, since, given a terminating element of the lift monad, you can compute how many steps it takes to return a value.
It's stuff like this that makes me say I can't tell the difference between operational and denotational semantics any more.
Friday, June 17, 2011
Tuesday, May 31, 2011
ICFP 2011
I was just notified that the paper I wrote with Nick Benton, A Semantic Model of Graphical User Interfaces, was accepted to ICFP 2011!
This is my first paper at ICFP, so I'm quite excited. Also, I accidentally misread the submission guidelines and wrote a 10-page draft, instead of a 12-page draft. As a result, I have two whole pages to add examples, intuition, and motivation. This feels positively decadent. :)
This is my first paper at ICFP, so I'm quite excited. Also, I accidentally misread the submission guidelines and wrote a 10-page draft, instead of a 12-page draft. As a result, I have two whole pages to add examples, intuition, and motivation. This feels positively decadent. :)
Thursday, May 5, 2011
GUI Programming and MVC
This post was inspired by this post on William Cook's blog.
I've been thinking a lot about GUIs lately, and I think model-view-controller is a very good idea -- but one that existing languages do a poor job supporting. Smalltalk deserves credit for making these thoughts possible for Trygve Reenskaug to express, but it's been over 30 years; we really ought to have made it easy to express by now.
Now, the point of a controller is to take low-level events and turn them into high-level events. Note that "low-level" and "high-level" ought to be relative notions -- the toolkit might give us mouse and keyboard events, from which we write button widgets to turn them into click events, from which we write calculator button turns into application events (numbers and operations).
However, in reality new widgets tend to be extremely painful to write, since it usually involves mucking around with the guts of the event loop, and so people tend to stick with what the toolkit gives them. This way, they don't need to understand the deep implementation invariants of the GUI toolkit. As a result, they don't really build GUI abstractions, and so they don't need separate controllers. (A good example would be to think about how hard it would be to write a new text entry widget in your toolkit of choice.)
So I see the move from MVC to MV as a symptom of a problem. The C is there to let you build abstractions, but since it's really hard we don't. As a result new frameworks drop the C, and just grow by accretion -- the toolkit designers add some new widgets with each release, and everybody just uses them. I find this a little bit sad, honestly.
As you might guess from this blog, I find this quite an interesting problem. I think functional reactive programming offers a relatively convenient model (stream transducers) to write event processors with, but we have the problem that FRP systems tend towards the unusably inefficient. In some sense this is the opposite problem of MVC, which can be rather efficient, but can require very involved reasoning to get correct.
This basically leads to my current research program: can we compile functional reactive programming into model-view-controller code? Then you can combine the ease-of-use of FRP, with the relative efficiency[*] of the MVC design.
IMO, the system in our LICS paper is a good first step towards fixing this problem, but only a first step. It's quite efficient for many programs, but it's a bit too expressive: it's possible to write programs which leak rather a lot of memory without realizing it. Basically, the problem is that promoting streams across time requires buffering them, and it's possible to accidentally write programs which repeatedly buffer a stream at each tick, leading to unbounded memory use.
[*] As usual, "efficiency" is relative to the program architecture. MVC is a retained mode design, and if the UI is constantly changing a lot, you lose. For things like games, immediate mode GUIs seem like a better design to me. In the longer term, I'd like to try synthesizing these two designs, For example, even a live-document app like a spreadsheet or web page (the ideal cases for MVC) may want to embed video or 3D animations (which work better in immediate mode).
I've been thinking a lot about GUIs lately, and I think model-view-controller is a very good idea -- but one that existing languages do a poor job supporting. Smalltalk deserves credit for making these thoughts possible for Trygve Reenskaug to express, but it's been over 30 years; we really ought to have made it easy to express by now.
Now, the point of a controller is to take low-level events and turn them into high-level events. Note that "low-level" and "high-level" ought to be relative notions -- the toolkit might give us mouse and keyboard events, from which we write button widgets to turn them into click events, from which we write calculator button turns into application events (numbers and operations).
However, in reality new widgets tend to be extremely painful to write, since it usually involves mucking around with the guts of the event loop, and so people tend to stick with what the toolkit gives them. This way, they don't need to understand the deep implementation invariants of the GUI toolkit. As a result, they don't really build GUI abstractions, and so they don't need separate controllers. (A good example would be to think about how hard it would be to write a new text entry widget in your toolkit of choice.)
So I see the move from MVC to MV as a symptom of a problem. The C is there to let you build abstractions, but since it's really hard we don't. As a result new frameworks drop the C, and just grow by accretion -- the toolkit designers add some new widgets with each release, and everybody just uses them. I find this a little bit sad, honestly.
As you might guess from this blog, I find this quite an interesting problem. I think functional reactive programming offers a relatively convenient model (stream transducers) to write event processors with, but we have the problem that FRP systems tend towards the unusably inefficient. In some sense this is the opposite problem of MVC, which can be rather efficient, but can require very involved reasoning to get correct.
This basically leads to my current research program: can we compile functional reactive programming into model-view-controller code? Then you can combine the ease-of-use of FRP, with the relative efficiency[*] of the MVC design.
IMO, the system in our LICS paper is a good first step towards fixing this problem, but only a first step. It's quite efficient for many programs, but it's a bit too expressive: it's possible to write programs which leak rather a lot of memory without realizing it. Basically, the problem is that promoting streams across time requires buffering them, and it's possible to accidentally write programs which repeatedly buffer a stream at each tick, leading to unbounded memory use.
[*] As usual, "efficiency" is relative to the program architecture. MVC is a retained mode design, and if the UI is constantly changing a lot, you lose. For things like games, immediate mode GUIs seem like a better design to me. In the longer term, I'd like to try synthesizing these two designs, For example, even a live-document app like a spreadsheet or web page (the ideal cases for MVC) may want to embed video or 3D animations (which work better in immediate mode).
Tuesday, April 19, 2011
Models of Linear Logic: Length Spaces
One of the things I've wondered about is what the folk model of linear logic is. Basically, I've noticed that people use linear logic an awful lot, and they have very clear intuitions about the operational behavior they expect, but they are often not clear about what equational properties they expect to hold are.
Since asking that question, I've learned about a few models of linear logic, which are probably worth blogging about. Morally, I ought to start by showing how linear algebra is a model of linear logic, but I'll set that aside for now, and start with some examples that will be more familiar to computer scientists.
First, recall that the general model of simply-typed functional languages are cartesian closed categories, and that the naive model of functional programming is "sets and functions". That is, types are interpreted as sets, and terms are functions between sets, with the cartesian closed structure corresponding to function spaces on sets.
Next, recall that the general model of intuitionistic linear logic are symmetric monoidal closed categories. So the question to ask is, what are some natural symmetric monoidal closed category given by sets-with-structure and functions preserving that structure? There are actually many answers to this question, but one I like a lot I learned from a 1999 LICS paper by Martin Hofmann, and is called "length spaces". It is very simple, and I find it quite beautiful.
To understand the construction, let's first set out the problem: how can we write programs that respect some resource bounds? For example, we may wish to bound the memory usage of a language, so that every definable program is size-bounded: the output of a computation is no bigger than its input.
Now, let's proceed in a really simple-minded way. A length space is a pair $(A, \sigma_A)$, where $A$ is a set and $\sigma_A : A \to \N$ is a size function. Think of $A$ as the set of values in a type, and $\sigma_A$ as a function which tells you how big each element is. These pairs will be the objects of our category of length spaces.
Now, define a morphism $f : (A, \sigma) \to (B, \tau)$ to be a function on sets $A \to B$, with the property that $\forall a \in A.\; \tau(f\;a) \leq \sigma(a)$. That is, the size of the output is always less then or equal to the size of the input.
Here's the punchline: length spaces are a symmetric monoidal closed category.
Given two length spaces $(A, \sigma)$ and $(B, \tau)$, they have a monoidal product $(A, \sigma) \otimes (B, \tau) = (A \times B, \fun{(a,b)}{\sigma(a) + \tau(b)})$. The unit is $I = (\{*\}, \fun{*}{0})$, and the associators and unitors are inherited from the cartesian product. The intuition here is that strict pair, requires resources equal to the sum of the resources of the components.
The function space construction is pretty clever, too. The exponential $(B, \sigma) \multimap (C, \tau) = (B \to C, \fun{f}{\min\comprehend{a \in \N}{\forall b \in B.\;\tau(f\;b) \leq \sigma(b) + a}})$. The intuition here is that if you have a morphism $A \otimes B \to C$, when we curry it we want a morphism $A \to (B \multimap C)$. However, the returned function may have free variables in $A$, so the size of the value it can return should be bounded by the size of its input $b \in B$ plus the size of its environment.
We also have a cartesian product, corresponding to lazy pairs. We define $(A, \sigma) \times (B, \tau) = (A \times B, \fun{(a,b)}{\max(\sigma(a), \tau(b)})$. The intuition is that with a lazy pair, where we have the (linear) choice of either the first or second component, we can bound the space usage by maximum of the two alternatives.
Note how pretty this model is -- you can think about functions in a totally naive way, and that's fine. We just carry around a little extra data to model size information, and now we have a very pretty extensional model of an intensional property -- space usage. This also illustrates the general principle that increasing the observations you can do creates finer type distinctions.
Since asking that question, I've learned about a few models of linear logic, which are probably worth blogging about. Morally, I ought to start by showing how linear algebra is a model of linear logic, but I'll set that aside for now, and start with some examples that will be more familiar to computer scientists.
First, recall that the general model of simply-typed functional languages are cartesian closed categories, and that the naive model of functional programming is "sets and functions". That is, types are interpreted as sets, and terms are functions between sets, with the cartesian closed structure corresponding to function spaces on sets.
Next, recall that the general model of intuitionistic linear logic are symmetric monoidal closed categories. So the question to ask is, what are some natural symmetric monoidal closed category given by sets-with-structure and functions preserving that structure? There are actually many answers to this question, but one I like a lot I learned from a 1999 LICS paper by Martin Hofmann, and is called "length spaces". It is very simple, and I find it quite beautiful.
To understand the construction, let's first set out the problem: how can we write programs that respect some resource bounds? For example, we may wish to bound the memory usage of a language, so that every definable program is size-bounded: the output of a computation is no bigger than its input.
Now, let's proceed in a really simple-minded way. A length space is a pair $(A, \sigma_A)$, where $A$ is a set and $\sigma_A : A \to \N$ is a size function. Think of $A$ as the set of values in a type, and $\sigma_A$ as a function which tells you how big each element is. These pairs will be the objects of our category of length spaces.
Now, define a morphism $f : (A, \sigma) \to (B, \tau)$ to be a function on sets $A \to B$, with the property that $\forall a \in A.\; \tau(f\;a) \leq \sigma(a)$. That is, the size of the output is always less then or equal to the size of the input.
Here's the punchline: length spaces are a symmetric monoidal closed category.
Given two length spaces $(A, \sigma)$ and $(B, \tau)$, they have a monoidal product $(A, \sigma) \otimes (B, \tau) = (A \times B, \fun{(a,b)}{\sigma(a) + \tau(b)})$. The unit is $I = (\{*\}, \fun{*}{0})$, and the associators and unitors are inherited from the cartesian product. The intuition here is that strict pair, requires resources equal to the sum of the resources of the components.
The function space construction is pretty clever, too. The exponential $(B, \sigma) \multimap (C, \tau) = (B \to C, \fun{f}{\min\comprehend{a \in \N}{\forall b \in B.\;\tau(f\;b) \leq \sigma(b) + a}})$. The intuition here is that if you have a morphism $A \otimes B \to C$, when we curry it we want a morphism $A \to (B \multimap C)$. However, the returned function may have free variables in $A$, so the size of the value it can return should be bounded by the size of its input $b \in B$ plus the size of its environment.
We also have a cartesian product, corresponding to lazy pairs. We define $(A, \sigma) \times (B, \tau) = (A \times B, \fun{(a,b)}{\max(\sigma(a), \tau(b)})$. The intuition is that with a lazy pair, where we have the (linear) choice of either the first or second component, we can bound the space usage by maximum of the two alternatives.
Note how pretty this model is -- you can think about functions in a totally naive way, and that's fine. We just carry around a little extra data to model size information, and now we have a very pretty extensional model of an intensional property -- space usage. This also illustrates the general principle that increasing the observations you can do creates finer type distinctions.
Friday, March 25, 2011
A Semantic Model for GUI Programs
Our paper on ultrametric semantics will appear at LICS 2011!
We've got a new draft, too, on applying this to GUI programming. This turns out to be not entirely straightforward, since GUI widgets accept user input, and so the semantics of a GUI has to model that input. The usual way of modelling input is via a reader monad -- that is, we model computations as functions which accept input as an argument -- but in a GUI you can (for instance) write programs which dynamically create new buttons, and so create new input channels.
The thing we did -- which seems obvious to me, but which Nick says is unusual, and for which I would like references -- was to view things like buttons as giving you a set of values. Then you can say that creating a button is an operation in the nondeterminism monad (basically). Then you don't need to model state at all.
Since this is notionally a research blog, let me point out a bit of mathematics I really liked in this paper (not actually due to me). Since we were working in ultrametric spaces, we couldn't use powersets, obviously -- we needed power spaces. It turns out that the right notion of powerspace for a space $X$ is the collection of closed subsets of $X$, under the Hausdorff metric. Then when $X$ is a complete 1-bounded ultrametric space, then $\mathcal{P}(X)$ will be too.
This is all totally standard, but one thing that wasn't obvious to me is whether powerspace actually forms a monad! The multiplication for powerset (in sets) is $\mu : \mathcal{P}^2(A) \to \mathcal{P}(A) = \fun{U}{\{a \in A \;|\; \exists X \in U.\; a \in X\}}$ -- that is, $\mu(U) = \cup U$.
Since only finite unions of closed sets are closed, for powerspace the corresponding multiplication ought to be $\mu(U) = \mathrm{cl}(\cup U)$. However, it wasn't obvious to me whether this was a nonexpansive map or not. I learned the following super-slick proof from a paper of Steve Vickers, "Localic Completion of Generalized Metric Spaces II: Powerlocales". Despite the formidable title, it is a very readable paper.
Below is just the fragment of the proof for the lower half of the Hausdorff metric.
$$
\begin{array}{lcl}
d(U, V) \leq q & \iff & \forall X \in U, \exists Y \in V.\; d(X, Y) < q \\
& \iff & \forall X \in U, \exists Y \in V.\; \forall x \in X, \exists y \in Y.\; d(x,y) \leq q \\
& \Longrightarrow & \forall X \in U, \forall x \in X.\; \exists Y \in V, \exists y \in Y.\; d(x,y) \leq q \\
& \iff & \forall x \in \cup X, \exists y \in \cup V, d(x,y) \leq q \\
& \iff & d(\cup U, \cup V) \leq q \\
& \iff & d(\mathrm{cl}(\cup U), \mathrm{cl}(\cup V)) \leq q \\
& \iff & d(\mu(U), \mu(V)) \leq q \\
\end{array}
$$
That quantifier flip is clever, but what makes this proof beautiful to me is introducing the auxilliary $q$. My own attempts just drowned in quantifier alternations, but this splits things up at just the right point. I'm reminded of Dijkstra's observation that most mathematicians do not make enough use of logical equivalence in their proofs, and clearly I fall into this category.
We've got a new draft, too, on applying this to GUI programming. This turns out to be not entirely straightforward, since GUI widgets accept user input, and so the semantics of a GUI has to model that input. The usual way of modelling input is via a reader monad -- that is, we model computations as functions which accept input as an argument -- but in a GUI you can (for instance) write programs which dynamically create new buttons, and so create new input channels.
The thing we did -- which seems obvious to me, but which Nick says is unusual, and for which I would like references -- was to view things like buttons as giving you a set of values. Then you can say that creating a button is an operation in the nondeterminism monad (basically). Then you don't need to model state at all.
Since this is notionally a research blog, let me point out a bit of mathematics I really liked in this paper (not actually due to me). Since we were working in ultrametric spaces, we couldn't use powersets, obviously -- we needed power spaces. It turns out that the right notion of powerspace for a space $X$ is the collection of closed subsets of $X$, under the Hausdorff metric. Then when $X$ is a complete 1-bounded ultrametric space, then $\mathcal{P}(X)$ will be too.
This is all totally standard, but one thing that wasn't obvious to me is whether powerspace actually forms a monad! The multiplication for powerset (in sets) is $\mu : \mathcal{P}^2(A) \to \mathcal{P}(A) = \fun{U}{\{a \in A \;|\; \exists X \in U.\; a \in X\}}$ -- that is, $\mu(U) = \cup U$.
Since only finite unions of closed sets are closed, for powerspace the corresponding multiplication ought to be $\mu(U) = \mathrm{cl}(\cup U)$. However, it wasn't obvious to me whether this was a nonexpansive map or not. I learned the following super-slick proof from a paper of Steve Vickers, "Localic Completion of Generalized Metric Spaces II: Powerlocales". Despite the formidable title, it is a very readable paper.
Below is just the fragment of the proof for the lower half of the Hausdorff metric.
$$
\begin{array}{lcl}
d(U, V) \leq q & \iff & \forall X \in U, \exists Y \in V.\; d(X, Y) < q \\
& \iff & \forall X \in U, \exists Y \in V.\; \forall x \in X, \exists y \in Y.\; d(x,y) \leq q \\
& \Longrightarrow & \forall X \in U, \forall x \in X.\; \exists Y \in V, \exists y \in Y.\; d(x,y) \leq q \\
& \iff & \forall x \in \cup X, \exists y \in \cup V, d(x,y) \leq q \\
& \iff & d(\cup U, \cup V) \leq q \\
& \iff & d(\mathrm{cl}(\cup U), \mathrm{cl}(\cup V)) \leq q \\
& \iff & d(\mu(U), \mu(V)) \leq q \\
\end{array}
$$
That quantifier flip is clever, but what makes this proof beautiful to me is introducing the auxilliary $q$. My own attempts just drowned in quantifier alternations, but this splits things up at just the right point. I'm reminded of Dijkstra's observation that most mathematicians do not make enough use of logical equivalence in their proofs, and clearly I fall into this category.
Friday, January 14, 2011
Ultrametric Semantics of Reactive Programs
I've got a new draft paper out with Nick Benton, Ultrametric Semantics of Reactive Programs.
We answer some longstanding open questions in FRP, namely:
1. What are higher-order reactive functions at all? How do you interpret them, and what are their semantics?
2. How can we implement FRP in a reasonable way, without compromising on either the equational theory or the ability to fit into the mutable callback event loop world of MVC?
It's got a little something for everyone -- some very pretty proof theory, some nice denotational semantics, and a hardcore separation logic proof with a step-indexed logical relation.
We answer some longstanding open questions in FRP, namely:
1. What are higher-order reactive functions at all? How do you interpret them, and what are their semantics?
2. How can we implement FRP in a reasonable way, without compromising on either the equational theory or the ability to fit into the mutable callback event loop world of MVC?
It's got a little something for everyone -- some very pretty proof theory, some nice denotational semantics, and a hardcore separation logic proof with a step-indexed logical relation.
Friday, November 5, 2010
Research notes
I think I will keep some research notes online. I've tried installing MathJax, so this should not be too unreadable, either. Let me begin with the typing of the simply typed lambda calculus, as is traditional.
\[
\begin{array}{lcl}
A & ::= & 1 \bnfalt A \times B \bnfalt A \to B \\
e & ::= & () \bnfalt (e,e) \bnfalt \fst{e} \bnfalt \snd{e} \\
& | & x \bnfalt e\;e' \bnfalt \fun{x:A}{e}
\end{array}
\]
\[
\begin{array}{ll}
\rule{x:A \in \Gamma}
{\judge{\Gamma}{x}{A}} &
\rule{ }
{\judge{\Gamma}{()}{1}}
\\
& \\
\rule{\judge{\Gamma,x:A}{e}{B}}
{\judge{\Gamma}{\fun{x:A}{e}}{A \to B}} &
\rule{\judge{\Gamma}{e}{A \to B} & \judge{\Gamma}{e'}{A}}
{\judge{\Gamma}{e\;e'}{B}}
\\
& \\
\rule{\judge{\Gamma}{e}{A} & \judge{\Gamma}{e'}{B}}
{\judge{\Gamma}{(e,e')}{A \times B}}
\\
& \\
\rule{\judge{\Gamma}{e}{A \times B}}
{\judge{\Gamma}{\fst{e}}{A}} &
\rule{\judge{\Gamma}{e}{A \times B}}
{\judge{\Gamma}{\snd{e}}{B}}
\end{array}
\]
\[
\begin{array}{lcl}
A & ::= & 1 \bnfalt A \times B \bnfalt A \to B \\
e & ::= & () \bnfalt (e,e) \bnfalt \fst{e} \bnfalt \snd{e} \\
& | & x \bnfalt e\;e' \bnfalt \fun{x:A}{e}
\end{array}
\]
\[
\begin{array}{ll}
\rule{x:A \in \Gamma}
{\judge{\Gamma}{x}{A}} &
\rule{ }
{\judge{\Gamma}{()}{1}}
\\
& \\
\rule{\judge{\Gamma,x:A}{e}{B}}
{\judge{\Gamma}{\fun{x:A}{e}}{A \to B}} &
\rule{\judge{\Gamma}{e}{A \to B} & \judge{\Gamma}{e'}{A}}
{\judge{\Gamma}{e\;e'}{B}}
\\
& \\
\rule{\judge{\Gamma}{e}{A} & \judge{\Gamma}{e'}{B}}
{\judge{\Gamma}{(e,e')}{A \times B}}
\\
& \\
\rule{\judge{\Gamma}{e}{A \times B}}
{\judge{\Gamma}{\fst{e}}{A}} &
\rule{\judge{\Gamma}{e}{A \times B}}
{\judge{\Gamma}{\snd{e}}{B}}
\end{array}
\]
Subscribe to:
Posts (Atom)