Member since 2 years
Fraser works at Red Hat on the FreeIPA identity management system,
Dogtag Certificate System and related projects. He's interested in security,
cryptography and functional programming. Jalapeño aficionado.
Software Foundations Workshop
The Software Foundations syllabus first teaches theorem proving in Coq, without any prerequisites other than basic functional programming. It then gives a broad introduction to Programming Language Theory, completely formalised in Coq. Created by Benjamin Pierce and co-contributors at the University of Pennsylvania, it is freely available, and has been used in several university-level courses.
Programming Language Theory is of interest to anyone who values working software systems, because it gives us tools for understanding the precise meanings of our programs, and the properties of the languages we use to build our programs. And theorem proving is a powerful discipline for challenging our beliefs that we know what we’re doing.
Although Software Foundations is self-contained and suited to self-study, it is easy to be intimidated by such a lengthy course on a topic and using tools that might be considered academic. However, the presenters firmly believe that formalising PLT in Coq actually makes it much more accessible for programmers. Fair warning: it’s also addictive.
In this workshop, you’ll find a supportive and collaborative environment in which newcomers to theorem proving and PLT can begin to explore this discipline, and the more experienced can refine their knowledge. The presenters will demonstrate a selection of exercises and techniques throughout the workshop, including some from early parts of the course, to help people get started, and some from latter parts, as a taste of what’s to come.
Please come prepared…
To make the most of the time available at the workshop, you should bring a laptop with some software already installed. Head over to this address, where we will provide some resources to help you get set-up for the workshop:
Unified Parsing and Printing with Prisms
Parsers and pretty printers are commonly defined as separate values, however, the same essential information about how the structured data is represented in a stream must exist in both values. This is therefore a violation of the DRY principle – usually quite an obvious one (a cursory glance at any corresponding
ToJSONinstances suffices to support this fact).Various methods of unifying parsers and printers have been proposed, most notably Invertible Syntax Descriptions due to Rendel and Ostermann (several Haskell implementations of this approach exist).
In this talk, attendees will learn an alternative approach to unified parsers and printers based on a familiar abstraction: prisms. We begin with an abstract parser definition based on the
Constype class (part of the lens library). The underlying prism gives rise to the functions
uncons, whose type matches that of a “typical” functional parser, and
cons, the dual (a printer!) From there we will examine how the fresnel library1 uses these building blocks to implement a combinator library for building parser/printer prisms out of existing prisms and isos.
We will see how fresnel has been applied in an ASN.1/DER library to correctly handle some of DER’s “special” encoding requirements. Finally, I will discuss some shortcomings of prism-based parser/printers, including the lack of useful error reporting.
Performant Polymorphism: Rewrite Rules in Haskell
GHC usually does an excellent job of transforming well written Haskell code into efficient machine code, but sometimes “fast” is not “fast enough”. Common optimisation techniques when dealing with concrete data types often do not apply to polymorphic data and functions. A concise, generic algorithm may perform poorly for some types, but providing a faster version with a less polymorphic type sacrifices reusability and parametricity! What’s a principled programmer to do?
Fortunately GHC has got your back here, too. In this talk we will learn about GHC’s *rewrite rules* feature, which can be used for substituting alternative, better performing implementations of polymorphic functions at particular (less polymorphic) types, without changing the type signature that users see, preserving reuse and parametricity. We will see also how to define transformation rules that employ theorems (free or otherwise) to optimise programs.
We will also briefly examine how rules are applied by observing the firing of rules and changes effected in the produced Core (GHC’s fully desugared intermediate language), and see how to control the order of inlining and rewrite rules to achieve the desired outcome.
Finally, we’ll look at a real-world example of how rewrite rules are used in the ‘fresnel' library, a unified parser-printer combinator library based on the ‘Cons’ abstraction from the ‘lens’ library, to dramatically speed up printing for certain output types.
This will be a hands-on talk with live coding, benchmarking and profiling (no optimising without metrics!) and Core spelunking. Audience members familiar with Haskell should expect to learn some basics of Haskell benchmarking and profiling, gain an understanding of when and how to use rewrite rules in their own code, and walk out feeling comfortable (or less trepidatious, perhaps) about reading and analysing their programs’ Core.
Infinite Scroll: Lazy Lists in the Brick TUI Library
The Brick terminal UI library provides a rich library of widgets for building console applications in Haskell. These include a list widget, which uses a packed vector type under the hood: a major problem when working with lists that are very large or expensive to compute.
In this case study I will review, step by step, how I generalised Brick's list widget to admit different underlying container types and achieved lazy loading of list items. The presentation will address several topics including:
- The advantages of more general (polymorphic) code, including parametricity
- Ensuring adequate test coverage before refactoring or generalising
- Maintaining backwards compatibility
- Assessing and documenting asymptotic performance
- Using Brick list widget in a real-world application (purebred MUA) for lazy loading where I/O is involved
- How to evaluate a lazy structure in the background (and why you might want to)
- Can we really achieve infinite scroll, or is my presentation title just clickbait?
Code examples will abound, and live demonstrations will both justify the work that was done, and show the pleasing results. The presentation uses Haskell exclusively but principles and advice for generalising code apply to many languages.
Taming the C monster: Haskell FFI techniquesFraser TweedaleSoftware EngineerRed Hat
schedule 2 years agoSold Out!
Haskell has a powerful foreign function interface (FFI) for interfacing with C libraries. Haskell is a great language for building libraries and tools, but interoperability requirements or time constraints can make the FFI a compelling option.
Binding to a non-trivial C library presents several challenges including C idioms, memory management, error handling and more. This presentation will address a selection of these concerns, using hs-notmuch, a binding to the notmuch mail indexer, as a case study. We will discuss:
- FFI basics and tools to assist binding authors
- working with "double pointer"-style constructors
- working with iterators; how to do lazy iteration
- how to use Haskell's garbage collector to manage lifecycles of external objects, and "gotchas" encountered
- using types to enforce correct use of unsafe APIs
- performance considerations (including profiling results)
The presentation will conclude with a mention of some important FFI concepts that were not covered (e.g. callbacks) and a look at how hs-notmuch is being used in the Real World.
Developers familiar with C will get the most out of this talk (because there will be limited time to explain C idioms, memory management, etc). To varying degrees, most of the concepts and techniques discussed will apply to other languages' FFIs.
No more submissions exist.
No more submissions exist.