"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@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.