Technische Universitat Dresden
4pm Tuesday, 21st of April, 2009
Room 4.31/4.33, Informatics Forum
The task of bidirectionalisation is to come up, for a given "get" function that takes a source (document or value) to a view, with a "put" function that takes an updated view and the original source back to an updated source, governed by certain consistency conditions relating the two functions. All earlier approaches to this view-update problem have been syntactic in nature. We present a semantic approach instead.
The idea is to use a general-purpose language, Haskell, and write a higher-order function that takes (polymorphic) "get" functions as arguments and returns appropriate "put" functions. All this on the level of semantic values, without being willing, or even able, to inspect the definition of "get", and thus liberated from syntactic restraints. The desired consistency conditions can be established using a type-based reasoning technique known as "free theorems".