SPLS

The Scottish Programming Languages Seminar is an informal meeting for the discussion of any aspect of programming languages. The next SPLS will take place on Wednesday 21 October 2015 at the University of Edinburgh.

Information and updates about the October edition of SPLS will be sent via the SPLS Mailing List.

If you plan on attending, please register here.

We gratefully acknowledge financial support from the Complex Systems Engineering theme of SICSA.

Confirmed Speakers

• Danel Ahman (University of Edinburgh) -- Dependent Types and Fibred Computational Effects
• Guillaume Allais (University of Strathclyde) -- Type and Scope Preserving Semantics
• James Chapman (University of Strathclyde) -- Relative Monads
• Aaron Crane (Cutbot) -- Writing immutable software in a mutable language
• Charles Grellois (University of Dundee) -- Linear logic, duality, and higher-order model-checking
• Shayan Najd (University of Edinburgh) -- Quoted Domain-Specific Languages, an Interesting Spot in the Design Space
• Roly Perera (University of Glasgow) -- Behavioural Prototypes
• Matúš Tejiščák (University of St Andrews) -- Erasure in dependently typed functional languages

Programme

The meeting will begin at 11AM and last until 17:30. There will be lunch, talks, coffee breaks, and a visit to a nearby pub.

10:30 - 11:00: Early Arrivals Coffee

11:00 - 12:30: Session 1

• 11:00 - 11:45: James Chapman -- Relative Monads

  Relative Monads are a naturally arising relaxation of the monads where the underlying functor need not be an endofunctor. I will describe relative monads and their surrounding theory, and give examples of their use in Agda and Haskell.

• 11:45 - 12:30: Aaron Crane -- Writing immutable software in a mutable language

  Languages like Haskell and Idris view immutability of data as a property of the language. Proponents of this approach point out advantages like the ease of reasoning about program behaviour, especially for data that is used across concurrency boundaries.
  
  This talk offers an alternative view of the world: that software designs can get huge benefit from relying on immutable data even when the implementation uses a language designed around mutable data. While this is not an entirely novel position, it is backed up here by a case study of a piece of real-world industrial software, written in Perl, that extracts rich information from web pages published by the Scottish and UK parliaments. Perl is a highly dynamic language; it strongly favours the flexibility and convenience offered by that approach over both theoretical purity and the ability to make static guarantees about program behaviour. This talk examines how the design of the Cutbot software makes the most of both mutable and immutable data — even in the absence of language support for guaranteeing immutability.

12:30 - 13:30: Lunch

13:30 - 14:30: Session 2

• 13:30 - 14:00: Shayan Najd -- Quoted Domain-Specific Languages, an Interesting Spot in the Design Space

We describe a new approach to implementing Domain-Specific Languages (DSLs), called Quoted DSLs (QDSLs), that is inspired by two old ideas: quotation (or more properly, quasi-quotation), from McCarthy’s Lisp of 1960, and the subformula principle of normal proofs, from Gentzen’s natural deduction of 1935. QDSLs reuse facilities provided for the host language, since host and quoted terms share the same syntax, type system, and normalisation rules. QDSL terms are normalised to a canonical form, inspired by the subformula principle, which guarantees that one can use higher- order types in the source while guaranteeing first-order types in the target, and enables using types to guide fusion. We test our ideas by re-implementing Feldspar, which was originally implemented as an Embedded DSL (EDSL), as a QDSL; and we compare the QDSL and EDSL variants.

• 14:00 - 14:30: Guillaume Allais -- Type and Scope Preserving Semantics

  We introduce a notion of type and scope preserving semantics generalising Goguen and McKinna’s approach to defining one traversal generic enough to be instantiated to renaming first and then substitution. Its careful distinction of environment and model values as well as its variation on a structure typical of a Kripke semantics make it capable of expressing renaming and substitution but also various forms of Normalisation by Evaluation as well as, perhaps moresurprisingly, monadic computations such as a printing function.
  
  We then demonstrate that expressing these algorithms in a common framework yields immediate benefits: we can deploy some logical relations generically over these instances and obtain for instance the fusion lemmas for renaming, substitution and normalisation by evaluation as simple corollaries of the appropriate fundamental lemma.

14:30 - 15:00: Coffee

15:00 - 16:00: Session 3

• 15:00 - 15:30: Danel Ahman -- Dependent Types and Fibred Computational Effects

In this talk I will discuss the interplay between two important topics in programming language research: dependent types and computational effects; by defining a small dependently-typed language, combining the features of Martin-Löf type theory and computational languages such as Call-By-Push-Value and the Enriched Effect Calculus. Our language has both value types and terms and computation types and terms, with the value and computation types only allowed to depend on values. A novel aspect of our language is the use of computational sigma-types to account for type-dependency in the sequential composition of computations.

The design of our language is inspired by a class of categorical models we call fibred adjunction models. These naturally combine i) comprehension categories arising from the semantics of dependent types; and ii) adjunctions arising from the semantics of computational effects. We also discuss a variety of examples, some arising from EM-algebras of monads, some from other decompositions of monads into adjunctions and some from considering general recursion as a computational effect.

Finally, we also comment on some ongoing work on understanding parametrized adjunctions and parametrized computational effects in this fibred setting. In particular, we show how the clear distinction between values and computations sheds new light on how to model parametrized computational effects where the result parameters need to depend on the values returned by the program, for example, to model the possible failure of opening a file.

(Joint work with Neil Ghani and Gordon Plotkin.)

• 15:30 - 16:00: Matúš Tejiščák -- Erasure in dependently typed functional languages

In dependently typed languages, we often express algorithms in ways more amenable to reasoning. We program with views, turn inductive types into indexed families, carefully craft definitions to ensure correctness by construction. However, this means that our programs compute with more data -- views, proofs, indices -- and they may end up asymptotically slower if these extra structures are too big asymptotically, even if they shouldn't affect the behaviour of the program at runtime.

In this talk, I will show how Idris recognises and erases this runtime-irrelevant data before reaching the code generation stage. Then I will describe an improved, type-based erasure scheme, which adds features like erasure from higher-order functions or a form of erasure polymorphism.

16:00 - 16:30: Coffee

16:30 - 17:30: Session 4

• 16:30 - 17:00: Charles Grellois -- Linear logic, duality, and higher-order model-checking

  A common approach in verification, model-checking consists in computing whether a given formula holds on an abstract model of interest -- typically, on a tree of actions representing the set of executions of a program. Over such a tree, a common procedure is to execute an automaton which checks whether an associated formula is satisfied.
  
  The model-checking of functional programs requires a careful treatment of higher-order recursive computation, which is a major hurdle to the traditional abstraction of programs as finite graphs, and thus to a decidability result. This led to the use of semantic methods, notably in Ong's decidability proof (2006).
  
  In this talk, we explain how linear logic leads to a new insight into the higher-order model-checking problem, notably as it discloses very naturally the dual behavior of the program and of its automata-theoretic specification. From this observation, we extend models of linear logic to obtain a purely semantic account of Ong's result: a given property over the set of executions of the program is satisfied if and only if the semantic interaction of the program with the automaton encoding the property of interest contains the initial state of the automaton.
  
  This is joint work with my PhD advisor Paul-André Melliès.

• 17:00 - 17:30: Roly Perera -- Behavioural Prototypes

I'll demo a simple language of concurrent objects which explores the design space between type systems and continuous testing. In our language, finite-state programs are checked automatically for multiparty compatibility. This property of communicating automata, taken from the session types literature but here applied to terms rather than types, guarantees that no state-related errors arise during execution: no object gets stuck because it was sent the wrong message, and every message is processed.

The usual object-oriented notion of subtyping is also interpreted at the level of terms rather than types. An abstraction takes the form of a prototypical implementation against which another program can be automatically tested for behavioural conformance. Any program can act as an abstraction, and conversely every abstraction is a concrete program that can be executed.

(Joint work with Simon Gay.)

Venue and Travel

SPLS will take place at the Informatics Forum, 10 Crichton Street, Edinburgh. The entrance is opposite that of Appleton Tower; the rooms used for the seminar and lunches will be signposted.

Further information about travelling to the Informatics Forum can be found on the School of Informatics web site.

Organisers

The organisers are Simon Fowler (simon.fowler -at- ed.ac.uk), Sam Lindley (sam.lindley -at- ed.ac.uk), and James McKinna (james.mckinna -at- ed.ac.uk).