Archive for March, 2006

Uniqueness Logic

Friday, March 24th, 2006 by Wouter

I talked about the firsty twenty odd pages of Dana Harrington’s thesis, which Hank had kindly pointed out to me. Uniqueness logic is used by Clean to write fast functional programs and model safe IO. The core idea is to keep track of which values are unique, i.e. can be represented by a single cell of memory that is never copied or thrown away. To accomplish this, uniqueness logic distinguishes between unique and non-unique values in their type. A type A is considered unique; it’s non-unique counterpart is denoted by A^\ast.

The following sequents describe the most important rules (excuse the crummy latex):

$\frac{}{A \vdash A}$
$\frac{\Gamma \vdash A}{\Gamma \vdash A^{\ast}}$
$\frac{\Gamma, A \vdash B^\ast}{\Gamma, A^\ast \vdash B^{\ast}}$
$\frac{\Gamma \vdash A \quad \Delta \vdash B}{\Gamma, \Delta \vdash A \otimes B}$
$\frac{\Gamma, A, B \vdash C}{\Gamma, A \otimes B \vdash C}$
$\frac{\Gamma \vdash A \quad \Delta, B \vdash C}{\Gamma, \Delta, A  \multimap B \vdash C}$
$\frac{\Gamma, A \vdash B}{\Gamma \vdash A \multimap B}$

together with weakening and contraction of non-unique values:

$\frac{\Gamma \vdash A}{\Gamma, B^\ast \vdash A}$
$\frac{\Gamma, A^\ast, A^\ast \vdash B}{\Gamma, A^\ast \vdash B}$

Crucially, any unique type can be coerced to its non-unique counterpart. The same can only happen on the left of the turnstyle if the result is guaranteed to be non-unique. There is an interesting duality here with linear logic, where the ! has the following rules:

$\frac{\Gamma, A \vdash B}{\Gamma, !A \vdash B}$
$\frac{!\Gamma \vdash A}{!\Gamma \vdash !A}$

Thorsten remarked that where the rules for uniqueness type introduction and elimination form a monad, the linear types form a comonad.

Pipes & Switches

Monday, March 20th, 2006 by Thorsten

Recently I introduced a functional model of Stream IO – this can be generalized to allow any type of input and output and we can define a pipe operator (>>>>) to combine processes. The resulting type of traces (see Traces.hs for the Haskell code) is at the same time a monad (in the return type) and an arrow over coproducts in the input and output types. I consider this as a promising formalism to integrate data-flow (pipes) and control-flow (switches). However, my attempt of a law relating pipes and switches was doomed as it was quickly noticed by the attentive FP lunch audience. I believe I now know how to fix it but this is for another time (I should actually prove my laws and not just type-check them… :-)

This is inspired Henrik’s work on Yampa (which introduces the notion of a switch), Varmo and Tarmo’s paper on dataflow programming and is based on discussions with Varmo and Tarmo on a cold February day in Tartu. A good reference for arrows is Ross Paterson’s paper. I am using coproduct arrows here, which correspond to Arrows without first but with left (as in ArrowChoice).

Normalisation for Typed Combinatory Logic

Tuesday, March 14th, 2006 by James Chapman

I presented a normalisation proof for typed combinatory logic via normalisation by evaluation/reduction-free normalisation/normalisation by intuitionistic model construction. Whilst this is certainly not news it represents a clear and simple example of the technique. It is very natural to consider a type theory such as Epigram’s as the metalanguage and therein lies some of the appeal. More detail to follow.

GTK2hs special

Friday, March 3rd, 2006 by Thorsten

Today we had Duncan Coutts (Oxford) and Axel Simon (Kent) to tell us all about GTK Haskell a GUI library for Haskell. Here are Duncan’s slides. More details of the demos are available from the gtk2hs blog.