Dear functional programmers, Standard Chartered Bank in London will be hosting the next Fun In The Afternoon event on Wednesday the 17th of February. The program of talks, with abstracts, is at the bottom of this email. Everyone is welcome! If you would like to come, please email me (ndmitchell -AT- gmail -DOT- com) with your name and affiliation by the 15th of Feb (late registrations will probably be accommodated, but we do need to print out name badges). Address: 1 Basinghall Avenue, London EC2V 5DD http://maps.google.co.uk/maps?q=standard+chartered+bank&ie=UTF8&hl=en&hq=sta... Moorgate is the nearest tube station, but London Liverpool Street train/tube station and Bank tube station are easily walkable. Time: The event starts at 1:10pm and finishes at 4:30pm. As traditional, there will be beer/food afterwards. Schedule: 12:00-1:10, arrive at Standard Chartered. We'll find lunch somewhere nearby. Tell the reception you are attending "Fun in the Afternoon". If you have any difficulties getting there, or can't find anyone when you arrive, phone me on 07876 126 574 1:10-1:15, Introduction 1:15-2:00, Invited talk, TBC 2:00-2:15, break 2:15-2:45, Zhaohui Luo, On Subtyping for Type Theories with Canonical Objects 2:45-3:15, George Giorgidze, Declarative Hybrid Modelling and Simulation in Haskell 3:15-3:30, break 3:30-4:00, Dominic Orchard, Haskell Type Constraints Unleashed 4:00-4:30, Malcolm Wallace, Pointless fusion for pointwise application 4:30-6:00, Pub 6:00, Dinner Abstracts: == Zhaohui Luo, On Subtyping for Type Theories with Canonical Objects Two different notions of subtyping have been studied in the literature: subsumptive subtyping that employs the subsumption rule and coercive subtyping that uses implicit coercions. They are suitable for different kinds of type systems: subsumptive subtyping for type assignment systems such as the polymorphic calculi in programming languages and coercive subtyping for the type theories with canonical objects such as Martin-Lof's type theory implemented in proof assistants. In this talk, we explain that subsumptive subtyping is incompatible with the idea of canonical object and cannot be employed to reflect, for example, structural subtyping for inductive types in a type theory with canonical objects. Coercive subtyping, on the other hand, can be used in such type theories to deal with structural and non-structural subtyping relations satisfactorily and has interesting and useful applications. If time permits, we shall show how the formal relationship between these two notions of subtyping can be studied by demonstrating how a type system of dependent types with subsumptive subtyping can be transformed faithfully into one with coercive subtyping. == George Giorgidze, Declarative Hybrid Modelling and Simulation in Haskell Mathematical modelling and simulation of physical systems plays an important role in design, implementation and analysis of systems in numerous areas of science and engineering, e.g., electrical engineering, astronomy, particle physics, biology, climatology, automotive industry and finance (to mention just few). To cope with ever increasing size and complexity of real-world systems, a number of declarative domain specific languages (DSLs) have been developed for mathematical modelling and simulation. In the first half of the talk, I will give a brief overview of the state-of-the-art languages for modelling and simulation and identify their shortcomings with respect to reusability, composability and hybrid (mixed discrete and continuous time) simulation. Next, I will introduce a Haskell-embedded DSL for declarative modelling and simulation that addresses some of these shortcomings. The DSL features first-class implicitly formulated equational constrains allowing for higher-order modelling and simulation of highly structurally dynamic, hybrid systems that goes beyond what current languages can simulate. In particular, it allows repeated generation and just-in-time (JIT) compilation of updated equational constrains during the simulation, depending on the results thus far. The embedding approach that we use should be of general interest and usable in other domains as well. In the second half of the talk, I will describe the embedding approach in detail. I will show how to use mixed-level (combination of deep and shallow) embedding and LLVM JIT compiler to implement an iteratively staged DSL (characterised by repeated program generation, compilation and execution) efficiently in a host language that does not provide built-in multi-stage programming capabilities. == Dominic Orchard, Haskell Type Constraints Unleashed The popular Glasgow Haskell Compiler extends the Haskell 98 type system with several powerful features, leading to an expressive language of type terms. In contrast, constraints over types have received much less attention, creating an imbalance in the expressivity of the type system. We rectify the imbalance, transferring familiar type-level constructs, synonyms and families, to the language of constraints, providing a symmetrical set of features at the type-level and constraint-level. In this talk, the new features, constraint synonyms and constraint families, will be introduced along with examples of their increased expressivity for improving the utility of polymorphic EDSLs in Haskell, amongst other examples. == Malcolm Wallace, Pointless fusion for pointwise application Take a common real-world application: the visualisation of large-scale multi-dimensional scientific data held in arrays. Typical processing involves both structural transformations of the data (e.g. slice, downsample, transpose), and numerical calculation, the latter often involving pointwise arithmetic over transformed arrays. With extremely large datasets, it becomes ever more important to process them with space-efficiency in mind, as well as speed. We will show two kinds of fusion that can automatically eliminate temporary intermediate arrays. An appropriate choice of array representation can make structural transformations extremely cheap, whilst avoiding copying. This talk will however focus mostly on the second kind of fusion: to coalesce numerical array expressions into a single traversal of the inputs, generating a single output. Calculating a fused operation is akin to calculating the points-free version of the entire expression. We speculate that the resultant code will be suitable for highly-parallel multi-core and GPU targets.