Functional Programming in Nottingham

There is also an FP lunch blog.

Participants

11th November - James McKinna was a guest a todays meeting, at which everyone first summarised what they had been doing during the last week, and James then showed how to program with red-black trees as a dependent type in Epigram (more details on FP blog).

28th October - Hank talked about the combinatorial completeness of the Church encoding of addition, multiplication, exponentiation and zero; further details are available as a literate Haskell script. Louise talked about description logic, and a problem concerning cheesy pizzas; further details on such logics are available in a book.

21st October - Jon talked about how to represent typed quantum circuits in Haskell, starting from untyped classical reversible circuits, in order to highlight the differences and similarities; more details on FP blog.

7th October - Conor talked about a multi-threaded unification algorithm which uses STM to avoid write conflicts. The code is available here.

16th September - Conor talked about the laws for idioms.

9th September - Thorsten talked about some connections between regular algebra and category theory.

2nd September - Everyone summarised what they had been doing over the Summer, and their upcoming travel plans.

22nd July - Zhaohui Luo was a guest at todays meeting, at which Conor talked about some recent work with Edwin Brady on adding annotations to a type system to make explicit the notion of some entities being `more static' than others; more details on epilogue.

15th July - Conor gave an overview of the Scottish Programming Languages Seminar in Edinburgh, and Thorsten talked about the suspected isomorphism between the types [[a]] and [Mayba a], which Wouter interpreted as "a list of lines is equivalent to a single line with explicit breaks". However, it turned out that the former type had to be modified to ([[a]],[a]); more details on FP blog.

8th July - Thorsten gave an overview of this years LICS conference in Chicago, and the associated Quantum Programming Languages workshop.

24th June - Pablo talked about the idea of an extensible version of a type-case construct in a language with subtyping.

17th June - Wouter talked about a categorical theory of patches in the DARCS version control system (more details on FP blog), and Thorsten gave an introduction to his recent work on viewing partiality as an effect (more details on FP blog).

10th June - Conor refined his previous question of whether three particular rules where sufficient to always win at newspaper sudoku without any backtracking, to the question of whether four particular rules were sufficient.

27th May - Graham presented a fusion problem, Conor talked about strategies for solving Su Doku, and Fermin considered about how to program printf and scanf using generalised algebraic datatypes.

29th April - Thorsten gave an overview of this years RTA and TLCA conferences in Japan, and Conor talked about the connection between idioms and the game of sudoku.

8th April - Fermin gave an overview of the recent links meeting in Edinburgh, and Thorsten gave the first half of a presentation on completness and normalisation for dummies.

11th March - Graham presented a compiler-correctness problem that he and Joel had not been able to solve: trying to verify a simple compiler based upon the use of relational semantics, as opposed to functional semantics. (Relations are appropriate because the language is non-deterministic.) The meeting managed to solve the problem using the notion of a bar operator.

4th March - Peter talked about dependently typed generic programming. It is possible using dependent types to write equality functions that give results in a more informative type than just Bool, we can construct as a result either a proof that the two are in fact the same thing or a proof that they are not. Another dependently typed trick is to use reflection to define the type of regualar types (with constructors mu, +, *, One, Zero...) and then the type of elements for a given regular type (in for mu, inl/inr for +, pairing for *, etc). By combining reflection and a more informative equality testing we can write a data-type generic equality test that is obviously correct from it's type.

25th February - Conor talked about the ‘glued’ representation of λ-terms used in the next version of Epigram. The idea is to pair a syntactic de Bruijn representation of terms with a semantic representation of their weak head-normal forms. This allows the consumer of a value more control over which computations are actually performed. It also makes it relatively simple to extend the calculus with defined function symbols, via a smart constructor for weak head-normal applications. Haskell source is available here.

28th January - Graham mentioned an interesting article about multi-core processors, Conor introduced epilogue, and there was a discussion about level of abstraction in programming.

21st January - Graham gave an overview of a recent talk in Oxford by Donald Knuth on the connection between sand piles (physics) and spanning trees (computing). Thorsten talked about the issue of expressively-complete combinators for reversible computation.

14th January - Conor talked about some ideas for the proof system layer of Epigram, in particular his latest attempt to extend type theory with holes in a way which is better structured and preserves more sharing. More of the picture can be found here

7th January - Thorsten gave a recap of his approach to viewing quantum computation as a generalisation of classical computation, and mentioned a number of problems that he and Jonathan are currently working on.

Meetings 2004

10th December - Joel gave an overview of Simon Peyton Jones' new approach to concurrency in Haskell, based upon a transaction monad.

19th November - Everyone summarised what they are currently working on.

12th November - Graham proposed a problem: how can dependent types be used to make explicit that a compiler from arithmetic expressions to stack-machine code never produces code that underflows the stack. Conor showed how to solve this problem in Epigram, and also presented some new ideas about how to prove compilers correct in the presense of jumps.

5th November - Henrik talked through his implementation of a modular interpreter for a language with various computational feature, including concurrency, output, mutable state, exceptions and interrupts. Concurrency was modelled using Koen Claessen's technique from a poor man's concurrency monad, with further features being added one at a time using monad transformers.

29th October - Graham gave an overview of recent work with Joel on the semantics of a minimal language with both exceptions and interrupts.

22nd October - Henrik gave a live demo of the HAT system for debugging Haskell programs. Further details and downloads are available here.

15th October - Henrik talked about how to present monadic computations to users at a high level, e.g. for debugging purposes. This is an open problem, and the purpose of this discussion was just to present the problem and solicit ideas for lines of attack. A more detailed summary is available here.

8th October - Everyone summarised what they are currently working on, Graham presented an autumnal problem on counting leaves, Conor presented the clinking glasses problem from Dagstuhl, and Palbo showed how to emulate algebraic datatypes in C++.

1st October - Henrik talked about some of the highlights from ICFP and the Haskell Workshop at Snowbird in Utah. He has copies of the proceedings for both events if anyone would like to borrow them.

24th July - Thorsten talked about codata: In a total language we have to distinguish data and codata. He explained codata using a mirror: while data is defined by a producer construct, i.e. the producer promises only to use the agreed constructors to construct data, codata is defined by a consumer contract, i.e. the consumer promises only to use pattern matching to analyze the codata. These principles give rise to recursion - corecursion and induction - coinduction. Coinductive reasoning can be explained using a coinductive definition of equality.

9th July - Thorsten talked about the comparison between the standard model of reversible computation and quantum computation with a quick introdution to the category used in QML and super-operators. He also mentioned how the use of strict linear logic can avoid the creation of garbage and therefore reduces decoherance of the quantum state, something which is desirable if you wish to gain full benefit from quantum parallelism. A paper on these subjects with Jon Grattage is due soon.

18th June - Pierre Casteran sent an email to the Coq-Club list describing a problem he is having with type equivalence. Conor explained that this problem relates to what Coq does with constraints it cannot immediately solve. In this case the two constraints posed need to be solved in the opposite order to that in which Coq tries to solve them. This approach was characterised as an over simplification and Epigram's solution illustrated by its use of 'yellow' problems.

28th May - Graham gave an overview of Olivier Danvy's work on transforming a simple interpreter for the lambda-calculus into the Krivine machine and the CEK machine. Thorsten presented his recent work with Jon on understanding quantum computations in terms of isomorphisms between products of relevant and non-relavant parts of the state space. Fermin talked about the problem of verifying a fusion result in the scrap your boilerplate approach to generic programming in Haskell.