[Haskell] Fun in the Afternoon, London, 17th Feb (next Wednesday)

[Neil Mitchell]

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=standard+chartered+bank&hnear=London,+UK&ll=51.517796,-0.091581&spn=0.007023,0.01929&z=16&iwloc=A

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.