Last year Eric Wastl published a set of programming challenges as Advent of Code. I recently went through them, and just made my Python solutions available via GitLab. Feel free to have a look, but please refrain from contacting me with questions about it.

On a related note, Advent of Code 2016 seems to be happening.

Unfortunately I’m not able to share most of my university course work, due to our honor code. There are some exceptions, though. For instance, the last assignment in Patrik Jansson’s MSc/PhD course Advanced Functional Programming at Chalmers University of Technology is self-directed and open-ended. The general task is to “read, understand, evaluate and extend an advanced Haskell code base”, with the underlying goal of getting us students involved with an ongoing local research project, or in open-source development by contributing to one of the more popular Haskell package on Hackage.

In this article I will merely provide some background for the work we did, including relevant references. The information below should suffice to give an overview of this project.

Emil Axelsson, one of the authors of the Feldspar language [1], which is an embedded DSL for digital signal processing that is implemented in Haskell, gave a guest lecture on combining deep and shallow embeddings [2], and how this technique was used for the implementation of Feldspar.

In our project, my lab partner Niklas Logren and me collaborated with Markus Aronsson, a PhD Student in the Software Technology division in the Department of Computer Science and Engineering at Chalmers. Markus is currently working on a synchronous data flow extension to Feldspar, i.e. an extension to Feldspar that allows it to operate on streams. For details, please refer to the corresponding paper [3].

We implemented an FFT based on Cooley-Tukey. Our implementation is based on the FFT implementation that is outlined by Bjesse, Claessen and Sheeran in their paper on the hardware description language Lava [4]. Our entire code is available in my Github repository gregorulm/fft_feldspar. Markus Aronsson’s Feldspar extension is currently work-in-progress and not publicly available. Our FFT implementation, though, will be part of the eventual release.

References:

[1] E. Axelsson, K. Claessen, G. Devai, Z. Horvath, K. Keijzer, B. Lyckegard, A. Persson, M. Sheeran, J. Svenningsson, and A. Vajda. “Feldspar: A domain specific language for digital signal processing algorithms”. MEMOCODE 2010.

[2] J. Svenningsson and E. Axelsson. “Combining deep and shallow embedding for EDSL”. Trends in Functional Programming, LLNCS 2012.

[3] M. Aronsson, E. Axelsson, M. Sheeran. “Stream Processing for Embedded Domain Specific Languages”, (draft, submitted to IFL 2014).

[4] P. Bjesse, K. Claessen, M. Sheeran, S. Singh. “Lava: Hardware design in Haskell”, International Conference on Functional Programming, pp. 174–184, 1998.

In Bove and Dybjer’s Agda tutorial “Dependent Types at Work”, section 2.5 briefly introduces Gödel’s System T, which is based on the simply typed lambda calculus with booleans and natural numbers. They give Agda definitions of the primitives of System T, as well as the multiplication and addition operator, using those primitives. As an exercise to the reader, they ask for for further definitions like cut-off subtraction and a few Boolean operations.

Building abstractions by using this rather limited set of primitives turned out to be a pleasant diversion, so I went on and implemented further operations. But to start, here are the primitives of System T in Agda, as they were given by the authors. The six primitives of System T are true, false, zero, succ, if_then_else_, and natrec, i.e. recursion on natural numbers.

module SystemT where

data Bool : Set where
  true  : Bool
  false : Bool

data ℕ : Set where
  zero : ℕ
  succ : ℕ → ℕ

if_then_else_ : {C : Set} → Bool → C → C → C
if true  then x else y = x
if false then x else y = y

natrec : {C : Set} → C → (ℕ → C → C) → ℕ → C
natrec p h  zero    = p
natrec p h (succ n) = h n (natrec p h n)

Further, Bove and Dybjer give definitions for addition and multiplication:

_+_ : ℕ → ℕ → ℕ
_+_ n m = natrec m (λ x y → succ y) n

_*_ : ℕ → ℕ → ℕ
_*_ n m = natrec zero (λ x y → y + m) n

The subtraction operation requires the predecessor function. Note that the predecessor of zero is zero. Further note that since we are restricting ourselves to natural numbers, subtraction is defined as so-called cut-off subtraction. This means that computations that yield negative numbers when performed on integers yield zero instead. Concretely, 1 – 2 = 0 instead of -1 because we restrict ourselves to nonnegative integers.

pred : ℕ → ℕ
pred n = natrec n (λ x y → x) n

_-_ : ℕ → ℕ → ℕ
_-_ n m = natrec n (λ x y → (pred y)) m

This might look a bit hairy, so it’s probably helpful to walk through this function. First, subtract one from zero:

zero - (succ zero)
= natrec zero (λ x y → pred y) (succ zero)
= (λ x y → pred y) zero (natrec zero (λ x y → pred y) zero)
= (λ x y → pred y) zero  zero
= pred zero
= zero

Second, two minus one:

(succ (succ zero)) - (succ zero)
= natrec (succ (succ zero)) (λ x y → pred y) (succ zero)
= (λ x y → pred y) zero (natrec (succ (succ zero)) (λ x y → pred y) zero)
= (λ x y → pred y) zero (succ (succ zero))
= pred (succ (succ zero))
= succ zero

To do a bit more in System T, Boolean operators would be nice to have. Using “if_then_else_” the operators for not, and, or, and xor are straightforward to define:

¬ : Bool → Bool
¬ b = if b then false else true

_∧_ : Bool → Bool → Bool
a ∧ b = if a then b else false

_∨_ : Bool → Bool → Bool
a ∨ b = if a then true else b

_⊕_ : Bool → Bool → Bool
a ⊕ b = if a then (¬ b) else b

An equality check for boolean values follows naturally:

equalityBool : Bool → Bool → Bool
equalityBool a b = if a then (a ∧ b) else (¬ (a ∧ b))

On the other hand, I found the definition of equality for natural numbers tricky. The function ‘zero?’ is therefore not defined using the perviously mentioned primitives of System T. I’ll have to look further into lambda calculus. As it is, ‘zero?’ is a small blemish of this implementation of System T.

zero? : ℕ → Bool
zero? zero = true
zero? _    = false

positive? : ℕ → Bool
positive? n = ¬ (zero? n)  -- there are no negative numbers

equalityNat : ℕ → ℕ → Bool
equalityNat a b = (zero? (a - b)) ∧ (zero? (b - a))

Lastly, here are comparison operators for natural numbers:

_>_ : ℕ → ℕ → Bool
a > b = positive? (a - b)

_<_ : ℕ → ℕ → Bool
a < b = positive? (b - a)

_≥_ : ℕ → ℕ → Bool
a ≥ b = (a > b) ∨ (equalityNat a b)

_≤_ : ℕ → ℕ → Bool
a ≤ b = (a < b) ∨ (equalityNat a b)

All of this looks pretty clean. I let Agda evaluate a few expressions, which all worked fine.

When students encounter higher-order functions in functional programming, they are normally exposed to the following three first: map, filter, and fold. The higher-order functions map and filter are intuitively accessible. With the former you apply a function to each element of a list, while the latter retains only elements for which a given predicate is true. One might want to implement those functions in Haskell as follows:

map :: (a -> b) -> [a] -> [b]
map _ []     = []
map f (x:xs) = f x : map f xs

filter :: (a -> Bool) -> [a] -> [a]
filter _ [] = []
filter p (x:xs)
  | p x       = x : filter p xs
  | otherwise = filter p xs

On the other hand, fold is somewhat more confusing. As I’ve found, the treatment of this topic on the Haskell wiki is not overly accessible to novices, while the explanation given in Learn You A Haskell is, like pretty much everything in it, too cute for its own good.

There are two cases of fold, namely foldr and foldl, with ‘r’l and ‘l’ describing right-associativity and left-associativity, respectively. One possible definition of foldr is:

foldr :: (a -> b -> b) -> b -> [a] -> b
foldr _ z []     = z
foldr f z (x:xs) = f x (foldr f z xs)

‘z’ is the last element of the list you’re applying the function to. I sometimes hear people refer to this as the “identity element”, but this is not necessarily correct. ‘z’ can be the identity element. For instance, if you want to multiply all values in a list of integers, you would chose the integer 1 to take the place of ‘z’. However, nothing is keeping you from picking any other integer.

To illustrate foldr with an example, let’s evaluate the following function call:

foldr (*) 1 [1,2,3]
(*) 1 (foldr (*) 1 [2,3])
(*) 1 ((*) 2  (foldr (*) 1 [3]))
(*) 1 ((*) 2  ((*) 3 (foldr (*) 1 [])))
(*) 1 ((*) 2  ((*) 3 1))
(*) 1 ((*) 2  3)
(*) 1 6
6

To make this evaluation more digestible from the fourth line onwards, it could also be written as:

1 * (2 * (3 * 1))
1 * (2 * 3)
1 * 6
6

This example shows the application of the function to each element in the list. Maybe this reminds you of how lists are constructed using the cons operator, i.e. (1 : (2 : (3 : []))) is represented, after adding syntactic sugar, as [1, 2, 3].

In fact, a list can be constructed using a fold. So, if you were in a silly mood, you could create a function that takes a list, runs it through fold, and returns the same list:

listId :: [a] -> [a]
listId xs = foldr (:) [] xs

Of course, ‘xs’ can be omitted on both sides of this equation. If you now call this function with the argument [1, 2, 3], you’ll get (1 : (2 : (3 : []))) in return, which is [1, 2, 3].

Let’s now look at foldl, which is fold with left-associativity. One possible definition is as follows.

foldl :: (a -> b -> a) -> a -> [b] -> a
foldl _ z []     = z
foldl f z (x:xs) = foldl f (f z x) xs

Evaluating the same expression as given above, with foldr, results in:

foldl (*) 1 [1,2,3]
foldl (*) ((*) 1 1) [2, 3]
foldl (*) ((*) ((*) 1 1) 2) [3]
foldl (*) ((*) ((*) ((*) 1 1) 2) 3) []
((*) ((*) ((*) 1 1) 2) 3)
((*) ((*) 1 2) 3)
((*) 2 3)
6

You can probably see why defining a ‘listId’ function with foldl results in an error.

Also note that foldl and foldr only give the same result if the binary operator f is associative. Just consider what happens when you’re using an operator that isn’t, for instance:

> foldr (/) 1 [1,2,3]
> 1.5
>
> foldl (/) 1 [1,2,3]
> 0.16666666666666666

The first function call evaluates to (1 / (2 / (3 / 1))), and the second to (((1 / 2) / 3) / 1).