[Haskell] Fun in the Afternoon, Cambridge, 26 November

[Simon Marlow]

"Fun in the Afternoon" is a termly seminar on functional programming and 
related topics, and the next one will be held at Microsoft Research, 
Cambridge (U.K.) on

   26 November

(that's just under three weeks away).

We have a great set of talks lined up - see program and abstracts below.

If you'd like to come along, please email msrcevnt at microsoft.com with 
your name and afilliation, preferably by 20 November.

Cheers,
	Simon

------------------------------------------
Fun in Cambridge, 26 November 2009

12:00 Lunch: Various local options
13:00 Andreas Rossberg, "F-ing Modules"
13:30 Ondrej Rypacek, "Distributive Laws in Programming Structures"
14:00 Break
14:30 Thorsten Altenkirch, "ΠΣ: Dependent Types Without the Sugar"
15:00 Robin Adams, "Canonical Logical Frameworks"
15:30 Break
16:00 Matthew Naylor, "Dynamic analysis in the Reduceron"
16:30 Thomas Schilling, "Slicing It"
17:30 Pub
18:30 Dinner


-----------------------------------------------------------------------------

Andreas Rossberg

F-ing Modules

Andreas Rossberg, Claudio Russo, Derek Dreyer

Abstract:

ML modules are a powerful language mechanism for decomposing programs
into reusable components.  They also have a reputation for being
complex, and dependent on fancy type theory that is mostly opaque to
non-experts.  While this reputation is certainly understandable, we
aim here to demonstrate that it is undeserved.  To do so, we give a
very simple elaboration semantics for a full-featured, higher-order ML-
like module language.  Our elaboration defines the meaning of module
expressions by a straightforward, compositional translation into
vanilla System F (the polymorphic lambda-calculus), under plain F
typing contexts.  We thereby show that modules are merely a particular
mode of use of System F.

Our module language supports the usual second-class modules, with SML-
style generative functors and local modules.  To demonstrate the
versatility of our approach, we further extend the language with the
ability to package modules as first-class values -- an almost trivial
extension, as it turns out.  (Our approach also scales to handle OCaml-
style applicative functor semantics, but the details are significantly
more subtle, so we will not present them here.)

Lastly, we report on our experience using the "locally nameless"
approach in order to mechanize the soundness of our elaboration
semantics in Coq.

-----------------------------------------------------------------------------

Ondrej Rypacek

Title: Distributive Laws in Programming Structures
Abstract:
Distributive laws in Computer Science are in general rules governing
the  transformation of one programming structure into another.  In
functional programming, they are parametrically polymorphic functions
with a characteristic type "swapping the order of two parameterized-type
constructors". Their importance has been noted but to date documented
only in several isolated cases and by diverse formal approaches such as
Backouhse & Hoogendijk's zips, Meertens' functor pullers or McBride's
idiomatic functors.
     In this talk, a formal approach to distributive laws in programming
structures will be presented, which discloses their simple nature, a
uniform approach to elementary constructions on them and their precise
relationship to similar notions elsewhere in Category Theory. Although
the approach rests formally on deep results from 2-Category Theory, the
presentation will be geometrical as much as possible, making use of the
wonderful three dimensional nature of 2-categories.

-----------------------------------------------------------------------------

Thorsten Altenkirch

ΠΣ: Dependent Types Without the Sugar

(Based on joint work with Nils Anders Danielsson, Andres Löh
  and Nicolas Oury)

The recent success of languages like Agda and Coq demonstrates the
potential of using dependent types for programming. These systems rely
on many high level features like datatype definitions, pattern
matching and implicit arguments to facilitate the use of the language.
However, these features complicate the metatheoretical study and are a
potential source of bugs.

To address these issues we introduce ΠΣ, a dependently typed
core language. It is small enough for metatheoretical study and the
typechecker is small enough to be formally verified. In this language
there is only one mechanism for recursion---used for types, functions
and infinite objects---and an explicit mechanism to control unfolding,
based on lifted types. Furthermore structural equality is used
consistently for values and types; this is achieved by a new notion of
α-equality for recursive definitions.

We show, by translating several high-level constructions, that
ΠΣ is suitable as a core language for dependently typed
programming. We also provide a formal description of the language and
its typing rules.

See also: our recent paper (with the same title)
	http://www.cs.nott.ac.uk/~txa/publ/pisigma-new.pdf
or/and download pisigma from hackage.

-----------------------------------------------------------------------------

Robin Adams

Title: Canonical Logical Frameworks


Abstract: A canonical logical framework, or lambda-free logical
framework, is a logical framework that deals only with objects in
beta-normal, eta-long form. The concept has been invented
independently three times over the last 15 years or so: by Aczel, with
the Type Framework TF; by Watkins et al, with the Canonical Logical
Framework, and by Plotkin, with DMBEL.

I shall show how all these frameworks can be fitted into a hierarchy
such that they extend one another conservatively. I shall also
demonstrate the main selling point of canonical LFs: certain results
can be proven more easily in a canonical LF, then 'lifted' - that is,
the same result proven for a traditional LF as an immediate corollary.

-----------------------------------------------------------------------------

Matthew Naylor

Title: Dynamic analysis in the Reduceron

The Reduceron is a graph-reduction machine implemented on a
field-programmable gate array (FPGA).  Last year, we reviewed the
machine and set out to improve its runtime performance by a factor of
six.  If achieved, the performance of leading PC and FPGA
implementations of graph-reduction would be on a par for a common
class of programs --- an unusual and intriguing state of affairs for
such a general-purpose processor.

In this talk, I will present our progress towards this goal, beginning
with an overview, and then focusing on two recently added features:
update avoidance and speculative evaluation of primitive redexes.
Both enjoy the accuracy and simplicity of dynamic analysis without
incurring the runtime overhead that often makes static analysis
perferable in a conventional setting.

This talk represents joint work-in-progress with Colin Runciman.

-----------------------------------------------------------------------------

Thomas Schilling

Title:  Slicing It

Abstract:

Haskell's type error messages are often not as helpful as they could be. 
  One fundamental problem is that they blame a single location while 
several other locations may fix the error as well.  A type error slice 
does not blame a single location, but a fragment of the failing program.

Previous work on type error slices requires reformulating type checking 
as a constraint solving problem.  This makes it very difficult to 
integrate support for type error slices into existing compilers.  In 
this talk I present how we can overcome this limitation by requiring 
only a very basic interface to the type checker.