Home

A Semantic Model for Graphical User Interfaces

Nick Benton and Neel Krishnaswami, ICFP'11, A Semantic Model for Graphical User Interfaces:

We give a denotational model for graphical user interface (GUI) programming using the Cartesian closed category of ultrametric spaces. [..] We capture the arbitrariness of user input [..] [by a nondeterminism] “powerspace” monad.

Algebras for the powerspace monad yield a model of intuitionistic linear logic, which we exploit in the definition of a mixed linear/non-linear domain-specific language for writing GUI programs. The non-linear part of the language is used for writing reactive stream-processing functions whilst the linear sublanguage naturally captures the generativity and usage constraints on the various linear objects in GUIs, such as the elements of a DOM or scene graph.

We have implemented this DSL as an extension to OCaml, and give examples demonstrating that programs in this style can be short and readable.

This is an application of their (more squiggly) LICS'11 submission, Ultrametric Semantics of Reactive Programs. In both these cases, I find appealing the fact the semantic model led to a type system and a language that was tricky to find.

By Ohad Kammar at 2011-09-10 20:25 | DSL | Fun | Functional | Paradigms | Semantics | Theory | other blogs | 16691 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Gossip

During Domains X, Benton suggested that the ultametric model may be replaced by a step-indexing model (e.g., Lars Birkedal et al.'s LICS'11 First Steps in Synthetic Guarded Domain Theory: Step-Indexing in the Topos of Trees).

Applied topos theory anyone?

By Ohad Kammar at Sat, 2011-09-10 20:34 | login or register to post comments

I'd really like to see this

I'd really like to see this happen. Personally I find step-indexing to be a much nicer tool to work with than ultrametric spaces.

By djahandarie at Sun, 2011-09-11 06:27 | login or register to post comments

I made a series of blog

In July, I made a series of blog posts including a step-indexed model of a slight variant of the system in our LICS paper. See

The last post uses a step-indexed logical relation to prove termination of the calculus (with conats instead of streams, but it all works the same).

As an aside, the neat thing about our stuff is that the steps aren't purely formal devices -- they correspond to trips through the event loop!

I've started thinking about semantics synthetically, in the topos of trees, and it's even easier than a step-indexed model, since you have a next type constructor you can use directly! The powerspace construction in our ICFP paper gets a lot simpler in the topos of trees, as well, since the powerset there is a real power set, unlike the powerspace in ultrametric spaces (it's more like a powerdomain, with the usual fiendish difficulties).

By neelk at Mon, 2011-09-12 07:13 | login or register to post comments

First link broken

Thanks.

By Z-Bo at Mon, 2011-09-12 15:14 | login or register to post comments

Also, our implementation

Also, our implementation story has changed a bit. We now compile to JavaScript rather than embed in ML -- getting graphics working reliably cross platform seemed like something we would rather let other people do. The price is that now we have to implement stuff like polymorphism and pattern matching, but frankly that's easier for pl researchers to do.

Expect a release shortly after ICFP -- there are still some docs to be written and some bugs to shake out, as well as an explanation of how we solved the memory leak problem of FRP.

By neelk at Mon, 2011-09-12 13:20 | login or register to post comments