sebfisch

Total Parser Combinators

Nils Anders Danielsson presented a paper in which he implemented parser combinators in Agda together with correctness and termination proofs. An important trick is to use a phantom type as parameter to the parser type which describes whether a parser accepts the empty word.

I wonder how cumbersome it would be to use a similar trick for our regexp matcher. In the paper we describe informally how to build infinite regular expressions such that matching still terminates and it should be possible to express this in the type system too.

Personally, I found his paper interesting to read, because it is a good introduction to Agda and how to use this language to prove properties of real programs. I am certainly inclined to consider Agda myself when I need to do some formal reasoning with my code.

Another interesting aspect of the paper is the discussion of expressivity. To show that every decidable language over a finite alphabet can be described using his recognizers (a preliminary version of the developed parsers), Nils provides a function that translates a decision function for such a language into a recognizer. A similar construction is also possible for regular expressions:

import Text.RegExp

decide :: ([Bool] -> Bool) -> RegExp Bool
decide f | f []      = eps `alt` r
         | otherwise = r
 where r = alt (sym False `seq_` decide (f . (False:)))
               (sym True `seq_` decide (f . (True:)))

I briefly thought about whether it is possible to extend this construction to decidable languages like

{ nn | n > 0 }

with an infinite alphabet by using a custom semiring. My conclusion was: maybe.

Every Bit Counts

Dimitrios Vytiniotis presented a functional pearl on encoding typed data by means of question/answer games. The codes generated by proper games have the nice property that no bit is redundant and, basically, every bit sequence corresponds to an encoded value.

I wonder whether standard, derived, encodings of Data.Binary for algebraic data types have this property as I think it is straightforward to generate a proper question/answer game from a (regular) algebraic data type. I also wonder whether one could go the other way round and generate data types from games, which would probably require dependent types.

As an example for a more complex question/answer game, the paper presents an encoding of typed lambda terms, that is, a compact binary encoding of programs. IIRC, people have long struggled to express typed pograms with dependent types so it would be nice if a (dependent) data type for typed programs could be generated automatically from the game shown in the paper.

Controlflow vs. Dataflow

Jurriaan Hage presented an approach to analyze controlflow which looks similar to dataflow as presented at ICFP 2008. I never managed to analyze dataflow statically, so this paper was a pleasant surprise. I wonder what differences there are between our notion of dataflow and theirs of controlflow if compared carefully.

TeachScheme

Matthias Felleisen gave a Keynote on teaching functional programming that I saw with mixed feelings. On one hand the approach seems to work really well and How to Design Programs is an invaluable resource for learning how to program. On the other hand I recognized a tension between diversity and uniformity in Matthias’s talk.

He started with a quote from an earlier ICFP (like 10 years ago, or more)

Functional programing is typed, lazy, and pure.

and disagreed, stating that functional programming can also be untyped, eagerly evaluated, or even incorporate side effects. He considered diversity an important aspect of functional programming. Then he went on explaining a method for teaching functional programming that does not support diversity but prescribes a uniform recipe. There are surely good reasons for a uniform recipe. Most importantly, it is easy to learn. But the contrast to the beginning of the talk which cherished diversity was interesting at least.

Later Matthias went on to explain that he let his students implement games to make his classes more fun. I can imagine that learning to program only by uniform recipes can be boring. But are games the right answer to this problem? What if students would learn that programming is not only about following recipes but also about creative thinking? What if programming would not only be taught as engeneering but also as an art? It would be less boring for sure.