Breadth first labelling

March 6th, 2009 by Graham

I talked about Jones and Gibbons’ breadth first labelling algorithm, which uses cyclic programming:

-- Binary trees with labels in the nodes:

data Tree a		   = Leaf | Node (Tree a) a (Tree a)

-- Breadth first labelling function that works by taking a
-- stream comprising the first label for each level as an
-- additional argument, and returning a stream comprising
-- the next label for each level as an additional result:

label'			  :: Tree a -> [Int] -> (Tree Int, [Int])
label' Leaf	    ns	   = (Leaf, ns)
label' (Node l x r) (n:ns) = (Node l' n r', n+1 : ns'')
                             where
                                (l',ns')  = label' l ns
				(r',ns'') = label' r ns'

-- The desired stream of labels itself can then be constructed
-- by feeding the result stream back as the argument stream:

label			  :: Tree a -> Tree Int
label t			   = t'
                             where
                                (t',ns) = label' t (1:ns)

Various related topics were then discussed, including Banach’s fixed point theorem (Thorsten), the construction of final co-algebras (Thorsten), and a queue-based algorithm due to Okasaki (Nisse)

Container eating

February 28th, 2009 by Hancock

I think some asked me to post a link to the slides I used
for my talk last Friday.
They’re at http://www.cs.nott.ac.uk/~pgh/cont-eating-talk.pdf
(There are some backup slides at the end I didn’t use.)

Eating: beyond streams

Abstract
`Eating’ is about writing programs that implement functions on final
coalgebras, typically stream types. The crucial thing is to do it in
a composable way, as with Unix-style piping.

I’ll quickly canter through stream eating, pointing out the use of
nested fixedpoints, and of universal properties to define things.
The main content of the talk is about eating `infinite’ objects that
inhabit the final coalgebras of container functors.

For a long time I was stuck on how to do this in a composable way;
a few days ago I cracked it, and would like to show you how.
You can regard it as a study in dependently typed programming,
in which quite a few interesting things emerge.

****
Finally, many thanks for a really fun three and a half years in
Nottingham. And for the Talisker and baccy!
xxx,
Hank

Djinn, monotonic

February 13th, 2009 by Conor

On my way to check the plumbing, I dropped in to see how people were doing and told a bit of a story about proof search in implicational logic. You may have encountered the problem before in the context of Roy Dyckhoff’s contraction-free sequent calculi, which Lennart Augustsson turned into Djinn. Here’s a Haskell rendering of the basic idea. An implicational formula is an atom or an implication.

data Fmla
  = Atom Atom
  | Fmla :-> Fmla

type Atom = String

Let’s write a checker to see if a Fmla follows from a bunch of hypotheses. Step one, introduce the hypotheses, reducing the problem to testing if an atom holds.

fmla :: [Fmla] -> Fmla -> Bool
fmla hs (h :-> g) = fmla (h : hs) g
fmla hs (Atom a) = atom hs a

Step two: scan the hypotheses, trying to derive the atom from each.

atom :: [Fmla] -> Atom -> Bool
atom hs a = try [] hs where
  try js [] = False
  try js (h : hs) = from h a (js ++ hs) || try (h : js) hs

Step three: test whether a given hypothesis (&lsqho;in the stoup’) delivers the atom.

from :: Fmla -> Atom -> [Fmla] -> Bool
from (Atom b) a hs = b == a
from (g :-> h) a hs = from h a hs && fmla hs g

That’s to say, to use an implicational hypothesis, show the premise holds and use the conclusion. But from which context should we show the premise? If you look carefully, you’ll see that atom passes in the whole of its context, bar the hypothesis in the stoup. That stops us getting in a loop when we try to deduce A from (A → A). We haven’t thrown away any theorems, because any proof which uses the same hypothesis twice on a path in the tree can be shortened to cut out the loop.

But is that enough to ensure termination? Sure is. How might we see that? The problem is quite nasty, because if we want to show

(A → B → C) → D, A → C |- D

backchaining actually increases the length of the context: we end up showing

A → C, A, B |- C

but even so, you might get the feeling that the problem is getting smaller somehow. And you’d be right: we got rid of a higher-order hypothesis but acquired more at lower order. We can make that clear with a wee bit of indexing.

Here are formulae, now in Agda:

data Fmla : Nat -> Set where
  atom : Atom -> {n : Nat} -> Fmla n
  _=>_ : {n : Nat} -> Fmla n -> Fmla (suc n) -> Fmla (suc n)

The index is a loose bound on the order (arrow-left-nestedness) of the formula. Never use tight bounds when loose bounds will do—it’s too much hassle keeping tight bounds accurate. Now we can collect formulae in buckets according to their order. Let’s use this handy structure

Tri : (Nat -> Set) -> Nat -> Set
Tri T zero     = One
Tri T (suc n)  = T n * Tri T n

which I’ve defined recursively today for ease of iso. To see why these are sort-of triangles, instantiate T to vectors. Also T = Fin·suc goes with a bang! But I digress… Vectors can be seen as degenerate triangles.

Vec : Set -> Nat -> Set
Vec X = Tri \ _ -> X

Now we can say what a bucket of formulae of a given order might be.

List : Set -> Set
List X = Sig Nat (Vec X)   -- Sig is the usual dependent pair type
Bucket : Nat -> Set
Bucket n = List (Fmla n)

And now a context is a triangle of buckets:

Ctxt : Nat -> Set
Ctxt = Tri Bucket

So our checker repeatedly makes higher-order buckets smaller, at the cost of making lower-order buckets larger, but that’s a perfectly respectable way to be monotonically decreasing.

Agda’s termination checker isn’t so good at spotting that this is what’s going on, but before we had Agda’s bag on the side, there was a language called Epigram which resorted to Type Theory as its language for explaining termination. Gasp!

It’s gone 5pm on Friday and I’m still in school. (Thorsten and Graham are away today: they’d never allow this!) I’m just going to link to this inscrutable lump of code and finish this post later.

Indexing a coinductive type on a trace

January 9th, 2009 by Nils Anders Danielsson

Consider the following simple language, represented as a coinductive data type in Agda:

codata Expr : Set where
  nop  : Expr → Expr
  send : Msg → Expr → Expr

An expression is an infinite sequence of no-ops and send instructions. Assume now that we want to index the Expr type on exactly the messages being sent. One might believe that the following definition is OK:

codata Expr : Colist Msg → Set where
  nop  : ∀ {ms} → Expr ms → Expr ms
  send : ∀ {ms ms′} (m : Msg) → Expr ms → ms′ ≈ m ∷ ms → Expr ms′

However, this definition has a problem; it does not actually enforce that all the messages in the index are being sent, as demonstrated by the expression incorrect:

incorrect : ∀ {ms} → Expr ms
incorrect ~ nop incorrect

In the meeting today we discussed various ways to address this problem.

(You may wonder why send is not given the type

∀ {ms} (m : Msg) → Expr ms → Expr (m ∷ ms).

The reason is that this can make it harder to construct values in the Expr family; the coinductive equality _≈_ is stronger than Agda’s built-in one.)

Update on PiSigma

December 15th, 2008 by Thorsten

Last Friday I gave an update on \Pi\Sigma a dependently typed core language which Nicolas Oury and I are working on. We wrote a paper (you can also play with it) earlier this year which didn’t make it into ICFP and have revised the language definition considerably. Basically we got rid of some features (namely constraints) which were – in our view – to clever for a core language.

\Pi\Sigma is a core language, hence the emphasis is on small leaving out lots of syntactic sugar which makes languages like Coq’s CIC, Agda, Epigram or Cayenne actually usable. The idea is that these features can be recovered by a syntactic translation (or elaboration as we say) as part of the compiler. Having a small core langauge is nice for compiler writers but also for theoretical analysis. The aim here is similar as Fc for Haskell but directed at dependent functional programming.

Unlike most of the DTP languages mentioned above, with the exception of Cayenne, \Pi\Sigma is partial, i.e. programs may fail to terminate. On the other hand it is full blown, which means that type-checking is partial too. We think this isn’t such a big issue for programming if the only reason for the type checker to diverge is that you have anon-terminating expression within a type. On the other hand it is an issue for using \Pi\Sigma for verification and it also rules out important optimisations. Hence we plan to define a total fragment but we think it is a good idea to specify the partial language first. Indeed, even when using Agda (or Epigram) we find it often more convenient to start developing in a non-total langauge and address the totality issue later (or never, depending on demand).

Here is a summary of the essential features of \Pi\Sigma

  • Very few type formers : \Pi types, \Sigma-types , Type:Type, finite types (enumerations) as sets of labels, lifted types for recursion and coinduction.
  • Depedently typed pattern matching can be derived using the primitive eliminator and equality
  • Full recursion via let rec (mutual) , used to define recursive types (like Nat) and recursive values. Recursion is controlled via lifted types and boxes.
  • Inductive families can be encoded using an extensional equality
  • Coinductive types and families can be encoded using lifted types, overcoming some issues present in Agda and CIC

Currently we are working on a new implementation and on a revised language definition. I’ll put this up as soon as it is in a reasonable state.

The new GHC API

December 8th, 2008 by Wouter

Last Friday we had Thomas Schilling visiting. He talked about his internship at MSR. He has been cleaning up the GHC API. I’ve uploaded an annotated copy of his slides.

Call-by-push-value

November 21st, 2008 by Wouter

I talked about my recent attempts to understand call-by-push-value, a typed lambda calculus that is very precise about when evaluation occurs.

The idea underlying CBPV is to distinguish the type of values and computations. You can think of a value as a fully evaluated Int, String, pair of values, etc. Functions, on the other hand, are computations abstracting over values. I’ve put together an overview of all the types, terms, typing judgements, and evaluation rules (forgive me, but I’d much rather edit large formulas in latex directly than WordPress)

My motivation for this is very different from Paul Levy’s: I’m dreaming of a language with enough laziness to be interesting, but with more predictable memory usage than Haskell. The next step is to figure out how to add (value) data, and (computational) codata, effects (no IO monad), and enough syntactic sugar that you don’t need to be explicit about every thunk/force. There’s a relationship with Conor’s ideas about Frank and the recent work about focussing and duality at CMU that I haven’t managed to nail it down.

The origin of species

November 19th, 2008 by Thorsten

The theory of species was originally conceived by Andre Joyal and is used to analyze combinatorial structures in terms of their generating functions. In my talk on Friday I showed how the theory of species can be developed from a functional programming perspective with a view towards using them to analyze datatypes. I am diverging a bit from the classical definitions in defining a generalisation of species which matches with a specialisation of the notion of a container.

A generalized species is given by a family A : \mathbb{N} \to \mathrm{Set}, the idea is that A\,n is the set of structures which have n positions. E.g. consider the species of leaf-labelled binary trees \mathrm{BT} : \mathbb{N}\to\mathrm{Set}: BT\,3is the set of the two binary trees, which have 3 leafs (insert picture here). Given a species A we assign a functor [\![A]\!] : \mathrm{Set} \to \mathrm{Set} by [\![A]\!]\,X = \Sigma n:\mathbb{N}.A n \times X^n. The definition corresponds to the generating function, but this is a function on the reals not on sets (see my recent posting on sets and numbers). Note that X^n is just n \to X where we identify a natural number with the set of numbers smaller than it (usually called Fin in dependently typed programming).

Category question: If species are the objects, what are the morphisms? Let’s define a category \mathbb{S}. Given species A,B:\mathbb{N}\to\mathrm{Set}, a morphism is given by a triple [math](f,g,h)[/math]:

  •  f : \Pi n:\mathbb{N}, A n \to \mathbb{N}
    Calculating the numbers of positions.
  •  g : \Pi n:\mathbb{N}, a: A n, B\,(f\,n)
    Calculating the new shape.
  •  h : \Pi n:\mathbb{N}, a: A n, (f n) \to n
    Assigning source positions to target positions.

I leave it as an exercise to define identity and composition of those morphisms.

The definition of morphisms hopefully becomes clear when we give their interpretation as natural transformations, i.e. to every species morphism (f,g,h) : \mathbb{S}\,A \,B we assign a natural transformation  [\![f,g,h]\!] : \Pi X:\mathrm{Set},[\![A]\!]\,X \to [\![B]\!]\,X:
 [\![f,g,h]\!]\,X\,(n,a,\mathbf{x}) = (f\,n\,a,g\,n\,a,\mathbf{x}\circ (h\,n\,a)).

Operations on species: Given species A, B : \mathbb{N}\to\mathrm{Set}:

  • Coproducts are easy:
    (A + B)\,n = A\,n + B\,n
  • Products are a bit more involved:
    (A \times B)\,n = \Sigma i,j:\mathrm{Nat},i+j=n \times A\,i\times B\,j
  • Composition is also interesting:
    (A \circ B)\,n = \Sigma m:\mathbb{N},f:m \to \mathbb{N},(\Sigma i:m,f\,i = n),A\,m \times \Pi i:m.B\,(f\,i)

Given a species A : \mathbb{N} \to \mathrm{Set} we can construct its initial algebra \mu A : \mathrm{Set}.

to be continued

Numbers vs Sets

November 7th, 2008 by Thorsten

To simplify: Mathematics has to do with numbers, while Computer Science is more concerned with types (let’s call them sets). On the level of the natural numbers there is a nice equivalence identfying a finite set with the number of its elements. The operations of addition and multiplication on numbers correspond to coproduct (or disjoint union) and (cartesian) product of sets. Indeed we even use the same symbols + and \times. Exponentiation b^a corresponds to function space a \to b, indeed category theoreticians use the exponential notation for the latter.

But then the ways part and the schism begins. For the Mathematicians the natural numbers are only half of the story (indeed a semiring) and they hasten to add the negative numbers. If we want to keep exponentiation, we can’t stop at the integers, we get the rational numbers 1/2 = 2^{-1}, algebraic reals \sqrt{2} = 2^{1/2} = 2^{2^{-1}} and even algebraic complex numbers i = (-1)^{1/2} = (-1)^{2^{-1}. The intuitive completion of these constructions are the complex numbers.

Negative sets don’t really make sense, we are more interested in infinite sets. E.g. we would like to have a fixpoint of successor: \mu X.1+X = \mathbb{N}. Combining this with exponentiation leeds to larger sets like \mathbb{N} \to \mathbb{N} or ordinal notations
\Omega = \mu X.1 + X + \mathbb{N}\to X. This time the intuitive completion are sets.

But the story may have a happy ending. Once we start to analyze operations on those spaces, a new analogy seems to emerge. E.g. differentiation is well known as an operation on complex functions, but as Conor McBride observed it also makes sense as an operation on functors, i.e. operations on sets. Not on all functors, but then differentiation doesn’t work on all functions either. The analogy carries further, and indeed we can use a variation of Taylor’s theorem to analyze datatypes. Hence, here we seem to have a new union, the glimpse of a generalized calculus applicable to operations in numbers and sets.

One of the areas where this analogy has been exploited is the theory of species, where ideas from calculus are exploited to prove theorems about the combinatorics of structures. To me much of the literature seems to be written from the perspective of Mathematicians who know numbers and try to use them to analyze sets. I’d prefer to do it the other way around, start with sets and see whether we can steal ideas from conventional calculus.

This is basically the introduction to a more technical talk about generalized species which I will post separately.

Is purity inefficient?

October 17th, 2008 by Nils Anders Danielsson

Last week we discussed whether pure languages are inherently less efficient than impure ones, and if that is an interesting question to ask.

In Pure versus impure Lisp Pippenger showed that, under certain assumptions, pure Lisp can be strictly less efficient than impure Lisp. However, as noted by Pippenger, his result assumes certain operational semantics for the two languages. The result was later shown to be inapplicable to a lazy pure language (using call-by-need) by Bird, Jones and de Moor.

So, what if we change the operational semantics? By using a smart (impure) implementation of functional (pure) references, due to Baker, one can ensure that, as long as the references are used single-threadedly, all accesses and updates take constant time. (See Section 2.3.1 of A Persistent Union-Find Data Structure for an explanation of Baker’s idea.) Furthermore the heap of a sequential, impure program (with a standard semantics) is always used single-threadedly. Hence, if we incorporate Baker’s idea into the operational semantics of a pure language, then impure sequential programs can always be translated into equivalent pure ones, which execute with only a constant overhead in time.

However, this translation does not really give us much; understanding the translated program is no easier than understanding the original one, for instance. The question I am really interested in is to what degree programs written in a pure (functional) style are less efficient than those which use an impure style. Unfortunately this question seems hard to formulate in a good way, because “pure style” and “impure style” are rather subjective notions. Furthermore one still has the problem of choosing suitable operational semantics. Finally, as pointed out by Thorsten Altenkirch, a programming language can support semantics-preserving program annotations which the programmer can use to guide the compiler; this in effect enables tweaking the operational semantics on a case-by-case basis.