Bucharest FP

A functional programming group for those living and working in Bucharest

We gather monthly, watch someone talk about something they're passionate about and then continue the discussion in a pub

#023: Equational Reasoning in Programming

This meetup took place at the Eloquentix office, Tuesday, 21 June 2016 at 19:00. Find out when our next meetup is.

Equational Reasoning in Programming

Mihai Maruseac

Biography

Mihai Maruseac is a senior PhD candidate at University of Massachusetts Boston. His research focuses on privacy-­preserving publication and processing of location data, using techniques such as differential privacy and searchable encryption. He holds a Bachelor and a Master degree in Computer Science from University "POLITEHNICA" of Bucharest. His additional research interests include functional programming and artificial intelligence. He is the editor of "Haskell Communities and Activities Report", a biannual journal encompassing news in the Haskell ecosystem.

Abstract

Programs in the real world often accumulate technical debt — code that is shaped more by its history than its current purpose. Refactoring is one way to address that technical debt, making the code simpler, but not changing any meaningful behaviour.

One of Haskell's strengths as a practical language is that it's easy and safe to refactor code. It is often said that Haskell is "great for equational reasoning", although, perhaps, this is an opaque saying. This talk will walk through some examples of that will show how Haskell code can be inspected by hand and which will make the isomorphism between code execution and interpreting it by substitution become self evident. In other words, if one can substitute equals-for-equals then she can interpret a Haskell program on pen and paper only.

In mathematics, calculations are designed to simplify things. In contrast, in programming, calculations have different goals, more often that of transforming a simple and inefficient program into a more efficient but opaque version. The approach taken by Richard Bird in his functional pearls, is that of design by calculation: each solution is calculated from the problem statement using only the laws of functional programming. The Haskell community cares about semantics and laws. Referential transparency and the ability to replace equals by equals in all contexts allows us to do this kind of calculations to obtain efficient programs.