Semantic interfaces
Graphical applications tend to focus on concrete representations of
their user interfaces, restricting accessibility, extensibility, and
interoperability, while GUI toolkits make even that rather hard to do
well (see "Cross-platform GUI Toolkit Trainwreck", "Gui development is
broken", as well as GTK, Pongo, xlib, Xft, FreeType, HarfBuzz,
"State of Text Rendering (2012)").
Some people stick to unixy tools, which reduce everything to text
streams, but it's still much better in those aspects; others abuse web
technologies or Emacs, which allow for different kinds of compromises;
yet others experiment with semantic and/or declarative interfaces, about
which this note is.
Approaches
The general approach is to describe both input and output in a way that
leaves some freedom to implementations – that is, focusing on semantics,
or on the model, possibly providing some hints for concrete interfaces.
Examples of those, as well as of related or potentially useful for it
technologies, are below.
- HTML
-
While it's a rather bad example in how it is used in practice, and
rather restrictive by design, HTML tries to rely on semantic markup,
can be accompanied by RDFa, and CSS can be seen as a representation
recommendation. And it's the most widely used one.
- XMPP Data Forms
- XForms
- Form descriptions targeting thin clients.
- Fresnel
-
An RDF display vocabulary, which provides hints on how to present
RDF data.
- Semantic forms
- RDF-based form generators.
- Plain RDF
- Other combinations of XML, XSLT, RDF, CSS
-
Generic RDF browsers and editors can be used as well, XML with
associated XSLT can suggest representations.
- SCXML
-
A generic FSM description language, apparently intended for voice
interfaces. Seems handy, though those can be embedded into
types/propositions as well (e.g., Idris ST).
- Declarative GUI libraries
-
There is a variety of libraries that try to achieve usable declarative
GUIs. A recent paper on the topic is Declarative GUIs: Simple,
Consistent, and Verified, which also focuses on state machines and
relies on dependent types, and there's more in the "Related Work"
section. Being libraries, usually they are language-dependent, but
they still seem nicer than more common approaches. Common GUI
libraries, such as GTK, also support XML-based UI definitions
(e.g., GtkBuilder).
- swagger2 with Swagger UI (and perhaps servant-swagger)
- Coalpit
- Python Fire
-
Haskell (and Python; didn't check it, but looks similar) packages
generating interfaces out of types: JSON with OpenAPI in case of
Swagger, command-line options and DSV with usage strings in case of
Coalpit. These allow to easily expose complex structures (and
functions operating on those) to other programs and users, and can
potentially be extended to use RDF, presentation hints, and so on, and
would get considerably more descriptive with dependent types.
- My toy/prototype project
-
Doesn't even have a proper name, but still serves as an example:
semantic and textual UI descriptions are read as input and rendered,
user actions produce output.
- DBMS interfaces
-
While most of the web applications seem to be little more than
eye-candy and restrictive interfaces to databases, and there are
generic interfaces to those, perhaps this is worth mentioning. Those
are primarily about storage and retrieval, but business logic can be
implemented in a DBMS as well.
- Sequent calculus
- Other proof calculi
-
A handy way to deal with propositions in general, and may be useful
for zooming user interfaces.
The mentioned projects can be grouped into those focusing on fuzzy
description logic, on intuitionistic logic, and the less generic,
extensible, and/or semantic ones, which don't focus on a formal logic.
Unsurprisingly, propositions are helpful to carry semantics.
An interface outline
Aiming exchange of propositions in different kinds of logic, perhaps UI
should mostly deal with sequent calculus, while the program it
communicates with would handle inference rules, read user-composed
sequents, compose new ones. A loose analogy can be made with sequent
calculus corresponding to a terminal, logic – to a shell, program – to
streams of propositions (though probably in most cases it would be more
handy to define custom inference rules in a program itself, perhaps
plugging some kind of logic as a library), escape sequences – to
rendering hints.
There are nice opportunities for UI zomming with sequent
calculus or other proof calculi, and the system may be rather
simple/minimal and generic with it. But a bit of
experimentation is needed to see how usable it would be, and
it may be just a fun thing to play with.