FP Lunch

Liyang and myself are currently trying to formally verify an implementation of a simplified version of the core language of STM Haskell, in order to have a precise understanding of the basic mechanisms for implementing transactions. We consider a small concurrent language that includes an atomic primitive, and give this language an operational semantics. We then define a compiler for the language, which produces code for a virtual machine that implements the notion of transaction logs, and give this machine an operational semantics. The game then is the obvious one: establish a compiler correctness theorem that links the two semantics. In the meeting I gave a brief introduction to the notion of transactions, and posed an interesting problem: what is the appropriate notion of equality to be used when a transaction attempts to comit? We will say more about compiler correctness in the future, once this is finished.

I rambled interminably about the slippery tar pit that is equality in Type Theory, dicussing the various enviable and execrable aspects of both Intensional and Extensional variants. More or less, the intensional story gives you a definitional equality which is computable, given a suitable notion of partial evaluation, but the propositional equality is annoyingly weak: in particular, extensionality for functions does not hold. Extensional type theory fixes this by making the definitional equality reflect the propositional equality, but in some ways the cure is worse than the disease: the definitional equality is no longer computable, typechecking is undecidable, and well-typed programs may be utter nonsense in the presence of assumptions. Thorsten and I propose a remedy, Observational Type Theory, in which the reflection happens in the other direction: the non-computational definitional equality rules are reflected as the typing rules for equality proofs; the structural equality constructor for λ just expresses extensionality. We get all the provable equations of Extensional Type Theory, and if we’ve played our cards right, we get all the defintional equations of Intensional Type Theory. It’s a win-win situation.

Thorsten and I have been working on distinguishing non-isomorphic types. Along the way, we encountered some interesting connections with monadic parser combinators.

Traditionally, monadic parser combinator have a type:

Given a sequence of input symbols, the parser returns a finite powerset of possible leftovers. These parsers don’t return the information parsed, but merely recognize whether a given string is in the language.

Such parser combinators can actually be run:

by simply checking whether all the input has been consumed, i.e. the empty string is in the resulting powerset.

Context-free types over an index set consist of a and a parameter . Furthermore, context-free types are closed under products, coproducts and least fixed points. We consider such types isomorphic if their well-known functorial semantics are naturally isomorphic. They clearly resemble context-free grammars. Interestingly, the same monadic parser combinators can be used to distinguish non-isomorphic types.

Instead of parsing input strings, we have to be a bit more careful. As the product commutes and the coproduct is not idempotent, we move from sequences to multisets. We represent a multiset as follows:

Such multisets form a monad, a fortiori, they are an instance of MonadPlus. The old-school monadic parser combinators also work for multisets. We get parser combinators of the following type:

Using these parser combinators we can now count the number of inhabitants of a given type. As two non-isomorphic types will have a different number of inhabitants for some input, we have a structured manner to search for disparities.

If you’re particularly interested have a peek at the implementation and the paper Thorsten and I are working on.

Neil said:

Today I spoke about iterative and completely iterative monads. These
monads constitute terms which are the solutions of equations of the
form

for some functor . The monad is the smallest monad which contains unique solutions for all such equations. The rational monad
is the smallest monad which contains solutions of such equations where is finite.

An open question is to understand the monad of solutions to equations defining not just terms but operators such as

We call these algebraic terms. Getting freeness properties for such
classes of terms is the key to using the coproduct of monads to
combining such iterative theories

For references see the work of Milius and some of my own.

Stefan Milius, Completely iterative algebras and completely iterative
monads, Information and Computation, v.196 n.1, p.1-41, January 10,
2005. An old preprint.

Ghani, N and Lüth, C and de Marchi, Solving Algebraic Equations using Coalgebra, Journal of Theoretical Informatics and Applications, 2003.

Neil Ghani and Tarmo Uustalu, Coproducts of Ideal Monads, Journal of Theoretical Informatics and Applications, 2004.