## Welcome to the FP Lunch archive

Part of the Foundations of Programming Group## Meetings 2005

(pre-blog)
*18th November* - James talked about user-defined recursion
schemes in Epigram.

*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.