The most profound connection between logic and computation is a pun. The doctrine of Propositions as Types asserts that propositions correspond to types, proofs to programs, and simplification of proofs to evaluation of programs. The proof of a conjunction is a pair, the proof of a disjunction is a case expression, and the proof of an implication is a lambda expression. Proof by induction is just programming by recursion.

Dependently-typed programming languages, such as Agda, exploit this pun. To prove properties of programming languages in Agda, all we need do is program a description of those languages Agda. Finding an abstruse mathematical proof becomes as simple and as fun as hacking a program. This talk introduces *Programming Language Foundations in Agda*, a new textbook that is also an executable Agda script---and also explains the role Agda is playing in IOHK's new cryptocurrency.

We use types in programming, often without realizing how deeply rooted they are in the foundations of mathematics. There is a constant flow of ideas from type theory to programming (and back). We are familiar with algebraic data types; inductive types, like lists or trees; we've heard of dependent types and, in the future, we might encounter identity types and possibly get familiar with elements of homotopy type theory. I can't possibly talk about all of this, but I'll try to give you a little taste.

With the proliferation of blockchain designs, we see a proliferation of proposals for languages and systems to script the rules governing transactions on these blockchains, generally known as smart contract languages. Despite the name, these languages are usually fairly conventional programming languages used to impose constraints on the transactions permitted to transfer assets and manipulate data stored on the blockchain.

Given the high financial stakes and widely publicised exploits on first generation (Bitcoin) and second generation (Ethereum) blockchains, the third-generation Cardano blockchain places a strong emphasis on functional programming and formal methods. This includes a new approach to contract languages based on state-of-the art research in programming languages and the increased safety provided by functional programming. The benefits of functional programming go even further: instead of having to invent yet another custom language, we simply use Haskell for the job, we design a functional blockchain architecture, and we seamlessly combine on-chain and off-chain computations.

In this talk, I will outline how IOHK’s Plutus team combines programming language theory, functional programming in Haskell, and theorem-proving in Agda to develop a radically new approach to blockchain contract development. This work has resulted in the Plutus Platform, which uses meta-programming in Haskell for distributed contract applications operating on the Cardano blockchain.

PARTICIPANT PREPARATION:

Clone the repository at

https://github.com/plfa/plfa.github.io/

This is the textbook for the course.

Install Agda, the Agda standard library, and configure the plfa library. This can be done by following the instructions under the heading

Getting Started with PLFA

at

https://plfa.github.io/GettingStarted/

Outline:

This course is an introduction to formal methods in Agda, covering datatypes, recursion, structural induction, indexed datatypes, dependent functions, and induction over evidence; with focus on formal definitions of naturals, addition, and inequality, and their properties.

The textbook is freely available online:

• Programming Language Foundations in Agda
  plfa.inf.ed.ac.uk
  github.com/plfa/plfa.github.io/

The book has been used for teaching by me at:

• University of Edinburgh (Sep-Dec 2018)
• Pontifícia Universidade Católica do Rio de Janeiro (PUC-Rio) (Mar-Jul 2019)
• University of Padova (Jun 2019)

and by others at

• University of Vermont
• Google Seattle.

The book is described in a paper (of the same title) at the XXI
Brazilian Symposium on Formal Methods, 28--30 Nov 2018, which is
available here:

http://homepages.inf.ed.ac.uk/wadler/topics/agda.html#sbmf

The paper won the SBMF 2018 Best Paper Award, 1st Place.

In conjunction with YOW! Lambda Jam, Compose::Melbourne will be running an all-day Hang Out And Hack session, on Monday May 13 - the same day as Lambda Jam Introductory Workshops. Bring your laptop if you have one, learn and work on Functional Programming. We'll run "office hours" (people can request help on particular topics, or offer to help others); lightning talks; and generally we'll hang out and hack together.

This is a free event, open to the whole Functional Programming community, beginners or experts, whether or not you are attending the main Lambda Jam conference on 14th & 15th.

Unlike the paid Workshops, the free Hang Out And Hack will not be catered so attendees will need to make their own arrangements for food; there are a number of places within the venue and surrounds, or feel free to BYO.

Please register for your free Hang out and Hack ticket, so we can get an idea of numbers and plan activities appropriately.

Elixir is an extremely accessible functional programming language that is rapidly gaining popularity for good reason. With it's well curated, batteries-included tool chain, excellent documentation and it's sheer simplicity, not to mention its incredible 30+ year Erlang heritage.

The goal of this workshop is to get you a basic familiarity with Elixir and the tools you'll need to be effective working in the language. It will be aimed at programmers who don't know Elixir, and don't necessarily know any functional programming.

The workshop is organised around a set of exercises that should take you through the basics of the language. Once you've got to grips with the language and tools you'll be ready to build a real time game server. In this workshop you'll learn everything you need to start building amazing, production ready Elixir applications

Functional programming has become inevitable. New programming languages draw inspiration from the functional paradigm; old programming languages retrofit support for functional programming; and development teams change their coding style to adopt the best functional programming idioms. We are clearly experiencing a paradigm shift in our industry.

Due to its academic roots, functional programming sometimes seems unapproachable, with unfamiliar jargon, obscure concepts, and bewildering theories. It doesn’t have to be like that.

In this one-day series of lectures and hands-on workshops, we will translate the jargon, demystify the concepts, and put the theories into practice. There is nothing inherently difficult about functional programming. In fact, its main aim is to simplify programming and to make it more widely accessible. Functional programming is about being able to understand one function without the million lines of code it is a part of. It is about code reuse. It is about modularity and keeping code easy to change and refactor. These are all goals of good program design that every developer appreciates. Based on this common ground, we will explore functional programming together and see how it can help us to achieve these design goals. In fact, by learning the fundamentals of functional programming in Haskell, we can improve program design in mainstream languages, such as Javascript and C++, and even more so, in hybrid languages, such as Scala and Swift.

Throughout the day, we will explain the most commonly used functional programming terminology. You will learn the fundamentals of Haskell, one of the most popular functional programming languages. In the process, we will look at a lot of concrete code to understand what functional programming is all about and how to use it in your own programs. In the workshops, you will have plenty of opportunity to write code yourself, experiment, and ask questions. It’ll be fun!

Bring your laptop and your curiosity and by the end of the day, functional programming will be another tool in your toolbox, and you will be ready to enjoy the main YOW! Lambda Jam conference.

Everything you ever wanted to know about starting a functional programming conference from scratch and some things you didn't. We'll cover the great times, the stressful times and all of the behind-the-scenes. Learn how we brought people together, how we chose talks and how we managed to create a community atmosphere enjoyed by both beginners and sages alike.

In this talk I'm going to share key design decisions behind Haskell logging library called co-log.

This library combines multiple algebraic concepts in order to provide convenient and composable solution for the logging problem:

• Semigroup and Monoid
• Contravariant/Divisible/Decidable
• Comonads

I'm also going to show how we use this library in commercial Haskell projects.

A quine is a program that outputs its own source code, but can you create a 2 quine, a pair of programs that output each other with an A->B->A->B cycle? What about between different languages? Can you gzip your own source code? Is there a structured way to do this with theory? All these questions will be somewhat answered, in ways that will make your head hurt... math-a-magical demos and over 9000 layers of meta-ness await!

What do programming, quantum physics, chemistry, neuroscience, systems biology, natural language parsing, causality, network theory, game theory, dynamical systems and database theory have in common?

As functional programmers, we know how useful category theory can be for our work - or perhaps how abstruse and distant it can seem. What is less well known is that applying category theory to the real world is an exciting field of study that has really taken off in just the last few years. It turns out that we share something big with other fields and industries - we want to make big things out of little things without everything going to hell! The key is compositionality, the central idea of category theory.

This talk will introduce the emerging field of applied category theory, with the aims of:

• Giving attendees a broad overview of cutting-edge applications of category theory
• Building an understanding of a small number of the most important core concepts
• Getting attendees excited, inspired to learn more, and equipped to apply some basic concepts to their work

Functions in the lambda calculus rightly take single values as their arguments, and return single values as their results. Functions in machine code rightly take multiple values as their arguments (preferably in registers), and return multiple values (preferably in registers) as their results. For a compiler writer, dealing with this mismatch is a right headache. Arity information, which describes how many arguments each source level function "actually" takes wafts through ones codebase like an unpleasant odour, and after particular compiler stages subverts ones once loved source-level type signatures into unfortunate lies.

Salt is a new compiler intermediate language that embraces uncurriedness as a first class condition, and whose type signatures speak the truth about arity. Functions are functions still, but their types are honest about the fact that no one really evaluates lambda expressions using capture avoiding substitution. The GHC core language tried to tell a similar story using unboxed tuples, but it didn't quite work. The C language stayed out in the sun for too long wondering what a void returning lambda abstraction really returned, and when we all came back to find it, the only thing left was Salt.

The Yoneda lemma is not the first thing to learn in category theory, but sooner or later it appears in studying the field. Unfortunately, there is quite a gap between the intuitive idea, "tell me your friends, and I will know who you are" , and its precise formulation. This talk aims to bridge this gap by introducing algebraic results in the middle, namely Cayley's theorem for groups and its generalization to semigroups. These are elementary enough, but at the same time they exhibit the conceptual step of representability, and the idea of studying all different things in a familiar form.

The conventional wisdom in functional programming communities is that lambda calculus was "discovered". Extending the logic of the statement to its extreme, we might propose that an alien would recognize lambda calculus as a computational model. But would we be able to recognize an alien lambda calculus?

This talk is part gedankenexperiment, part speculative fiction, part practical advice on compiler design. We begin by imagining ourselves to be creatures in a universe which is very different from the one we're in, except the notion of consciousness and intelligence are preserved from our current universe. From there, we shall explore the physics and alternate philosophies that would yield an alien lambda calculus.

Of course, being from an alien conception, there are some questions that must be answered - in the name of practicality, is there perhaps even a weak notion of a functor from the alien lambda calculus to that of the one we know today? Is there anything from the alien lambda calculus that we may yield and put into practice? And what is this pesky business with state? Isn't the point of functional programming to hide states from the programmer by abstracting over them? Or was it to make clear the states? And what of names? Isn't lambda purely anonymous?

Many real-world lots-of-business-value-providing systems use a relational database. (Even more of them should!) Often, that database is used as a dumb data store – nothing more, logically, than an ACID-compliant coordinator of multiple flat files (tables). We send it basic queries – sometimes even joining multiple tables in one query! – inserts, updates and deletes. But nothing that might strain its little brain. Often, this is a mistake: a modern relational database is the most sophisticated data-munging tool in our toolkit!

We should consider doing more work in the database itself. But that's not easy to code well. How can we make our more complex SQL code easier to reason about, more reliable, and more testable? How can we make the overall system simpler?

These are questions that in not-the-database contexts, we solve with functional programming techniques. Without expecting SQL to out-lambda Haskell, are there techniques that we can borrow from functional programming and apply to improving our SQL?

Apache Spark is one of the most popular data processing frameworks in the world, and is widely used in the enterprise. Its popularity is due in no small part to its adoption of the functional paradigm: it demonstrates the advantages of purity, higher-order functions and laziness to simplify the processing of large datasets. Haskell excels at all of those things; so it is only natural to think that Haskell would be a good fit for distributed data processing. Tweag.io's Sparkle and Soostone's Hadron are a few examples in the Haskell ecosystem.

'distributed-dataset'[1] is a framework written in Haskell designed to efficiently process large amount of data. With the StaticPointers extension of GHC Haskell, we are able to distribute a computation across different machines; and using the technique described by Matei et al[2] that led to Apache Spark, we can express and execute large scale data transforms using a pretty DSL.

In this talk, I am going to give a brief introduction to the library, and then move on to explaining the key implementation ideas and the advantages that Haskell offers to distributed data processing.

[1]: https://github.com/utdemir/distributed-dataset

[2]: "Resilient Distributed Datasets: A Fault-Tolerant Abstraction for In-Memory Cluster Computing" by Matei Zaharia, et al.

This talk looks at how functional programming has been used in tertiary education, and how it could be used in the future.
In 1985, Abelson and Sussman's course Structure and Interpretation of Computer Programs made enduring contributions to the art of educating programmers. How to Design Programs later refined some of these ideas, with a new emphasis on decomposing problems and designing solutions. I argue further improvements could be made. In particular, by using a typed functional programming language like Haskell.

This talk will suggest approaches and recommend resources that could be used in the modern education of undergraduate programmers. Such recommendations are also applicable to industry programmers looking to learn functional programming or organisations looking to develop internal training material.