Notes on Computing

Church encoding products and coproducts

March 13, 2015

In a previous post I gave an example of how to represent algebraic data types using church encoding. In this post I’ll pick up the thread and show how this technique can be used to mimic any type.

Continue reading

Designing a library for printing recursive data structures

February 16, 2015

I have more than once found myself in need of a function for pretty-printing some recursive data type; Be it a prefix search tree, an abstract syntax tree for a domain specific language, XML or something else. Getting tired of having to implement the same type of logic over and again I decided to generalize the pattern. In the following sections I discuss the design of a tiny library for addressing this problem. It’s not a particularly challenging task but provides a good opportunity to touch on a few different concepts in functional programming. Examples include deep and shallow embeddings, monoids and equational reasoning. The implementation is given in F#.

Continue reading

Building services on top of immutable data structures

February 6, 2015

Using immutable data structures enables equational reasoning and assures that update operations are atomic. However, purely immutable interfaces are not always feasible. For instance a RESTful service typically needs to propagate the effects of update operations to other clients. In this post I describe a strategy for constructing mutable service interfaces on top of purely immutable data structures. I’m using F# to exemplify.

Continue reading

Church encoding and existentially quantified types in F#

February 4, 2015

Can you imagine an F# compiler that doesn’t understand discriminated unions (aka algebraic data types)? For sure not an attractive scenario but perhaps just not as horrifying as you might expect. For example consider how the familiar option type is defined in F#:

Continue reading
Prev