Summer School on Generic and Effectful Programming
Embedded Domain-Specific Languages in Idris
Edwin Brady (University of St Andrews)Idris is a general purpose functional programming language with full dependent types, building on state-of-the-art techniques in programming language research. Dependent types allow types to be predicated on any value - in this way, required properties of a program can be captured in the type system, and verified by a type checker. This includes functional properties (i.e. whether the program gives the correct answer) and extra-functional properties (i.e. whether the program runs within specified resource constraints).
In these lectures, I will describe Idris, and how it can be used to implement Embedded Domain-Specific Languages (EDSLs). Idris has several features intended to support EDSL development, including syntax extensions, overloadable binders and implicit conversions. I will describe how these features, along with dependent types, can be used to capture important functional and extra-functional properties of programs, how resources such as file handles and network protocols may be managed through EDSLs, and finally describe a generic framework for programming and reasoning about side-effects, implemented as an EDSL.
Worst-case Efficient Generic Functional Programming on Bulk Data
Fritz Henglein (University of Copenhagen)Lecture 1: Generic discrimination. We show how radix-based techniques for searching, partitioning, and sorting can be made generic by compositional specification of orders and equivalence relations. This yields worst-case time optimal (linear time for partitioning and sorting, O(k) time for lookup of keys of size k) without leaking implementation information, improving on both comparison-based and hashing-based techniques.
Lecture 2: Generic multiset processing. We show how to build a generic querying framework for in-memory database programming with worst-case efficient generalized selections, projections, equi-joins, grouping and sorting.
Lecture 3: From multisets to infinite-dimensional linear algebra. We generalize multisets to have fuzzy and negative multiplicities, with applications to efficient computation on finite probability distributions. We observe a connection with infinite-dimensional modules and employ dynamic algebraic simplification based on (multi)linear algebra to arrive at surprisingly efficient execution of functions operating on and joining multiple bulk-data inputs.
Note. All lectures will emphasize the basic ideas rather than their formal and complete rendition; they will be illustrated by executable code, including small applications (rendered in basic Haskell 98, extended only with generalized algebraic data types). Some category-theoretic terminology will be used, but mostly for illustration of programming ideas and some Latin roots of English. A firm grasp of statically typed functional programming is required; a vague recollection of linear algebra is useful, but not strictly needed (it’ll likely look quite different anyway). The lectures will contain open problems for further research; some of their contents is as yet unpublished.
Applying Type-level and Generic Programming in Haskell
Andres Löh (Well-Typed)Haskell's type-level programming facilities have evolved substantially over the past few years. As a result, generic programming in Haskell is easier and more powerful than it has ever been before. We have a rich type-level language for writing down static information about our programs, and can write type-level programs to compute run-time programs that are type-safe by construction.
While type-level programming in Haskell may not be as elegant and simple as it is in a dependently typed language, the advantage is that we have access to a huge amount of real-world code and libraries and can easily apply generic programming techniques to real-life problems.
This course consists of:
a quick introduction to type-level programming in Haskell, in particular looking at concepts such as GADTs, type families, data kinds and kind polymorphism,
a look at how type-level programming features can be used to design libraries for generic programming in Haskell,
a discussion of a few concrete generic programming examples that make use of these libraries and techniques, taken e.g. from the areas of web programming and databases.
Datatypes of Datatypes
Conor McBride (University of Strathclyde)Dependently typed programming environments like Coq, Agda and Idris allow types to be computed. As a consequence, systems of datatypes can be given by interpreting values in a datatype of datatype descriptions (a universe) as the very datatypes those values describe. With datatype descriptions as first class objects, we can start to consider computational relationships between them. Statements such as "lists are natural numbers annotated by elements" and "vectors are lists indexed by their length" become more than ideas: we can realise them mechanically. In these lectures, I shall investigate a possible future in which programming languages deliver datatypes via a universe, and the varieties of generic construction which arise when we do.
Indexing of types becomes a new axis along which we can vary their design. Where today's dependently types languages let us declare isolated points in that design space (e.g., lists, lists of a given length, lists of distinct elements, ordered lists, and so on), tomorrow's will allow us to organise that design space effectively and productively. Working in Agda (but Idris programmers are welcome to offer simultaneous translation), I will show how to build the machinery which makes this future possible and consider ways in which we might exploit it. The gory details of the universe encoding will thus be somewhat conspicuous, so let us think also about how we might work more tidily.
Lecture topics will include the following: "levitation" (self-encoding systems of datatypes), "ornaments" (formalizing refinement and annotations between datatypes), "derivatives" (applying differential calculus to datatype descriptions with a spatial interpretation), and "design" (imagining how programming languages and environments might evolve).
Compile-time Meta-programming for the Information-rich World
Don Syme (Microsoft Research)Computer programs are developed and execute in the context of an immensely rich and growing digital universe. Compile-time meta-programming is emerging as a key technique to mediate between the programmer and the complexity of the information-rich world. In these lectures (3 hours total), we will explore these themes together. Examples will draw primarily from the F# Type Provider mechanism and how it is used to interface to a range of different information systems, but we will also look at the programming languages Ur, Idris, Template Haskell which incorporate related concepts which bring together generic programming and compile-time-metaprogramming. We will also look at how dynamically typed languages approach this problem.
Containers for Effects and Contexts
Tarmo Uustalu (Tallinn University of Technology)My course will be about containers (aka polynomial functors) as a representation for a wide class of datatypes, emphasizing their use for analyzing computational effects and contexts modelled as monads and comonads. We will especially look at some special classes of monads and comonads, and compatible compositions/distributive laws of monads and comonads, applied to various state-machine and cellular-automaton like notions of computation. You will see lots of monoids, groups, semirings etc.