This year, as every year since time immemorial, I participated in the ICFP contest as part of codingteam.

Preparation

As usual, before the contest started, I've managed to do some basic preparations.

I have created a team repository, set up a CI pipeline on GitHub Actions (that one didn't live long, though), and created a pre-flight check issue, for the team members to check their environment.

The Team

Before and immediately after the start of the event, I've invited several people and some asked to join, but the final set of active contributors (in alphabetical order) was:

• ForNeVeR,
• Foxtran,
• Gsomix,
• Minoru,
• portnov.

This year we've agreed to use Haskell as the main language (acknowledging that Foxtran will still write in Fortran regardless of any agreements; even if forced to use another language, he'll still write Fortran in said language).

The Task

Galaxy Language

This year's task was a quite interesting one. We've been given the specification of so-called ICFP expressions (we decided to call it "the Galaxy language").

This language represented a variant of typed lambda calculus with booleans, integers, strings, and of course lambdas, and a bunch of operators, but written in a quite unorthodox way. For example, the expression

B$ B$ L# L$ v# B. SB%,,/ S}Q/2,$_ IK

mean

((\v2 -> \v3 -> v2) ("Hello" . " World!")) 42

While operators such as B$ (function application) and $+ (addition) are easy to read, even strings and integers are encoded so that they are unreadable in the original language.

We've introduced our own notation that I'll use in this report. For example, the above expression would be written as

Apply
    ( Apply
        ( Lambda 2
            ( Lambda 3
                ( Var 2 )
            )
        )
        ( Concat
            ( Str "Hello" )
            ( Str " World!" )
        )
    )
    ( Number 42 )

But of course it wasn't all. We didn't have to just implement parser, evaluator, and emitter of the Galaxy language. We had to also solve several courses using this language.

Sending specific HTTP requests in the Galaxy language, we were able to scout a whole "site" of several pages, each represented by a Galaxy expression evaluating to a Markdown string. The pages contained the task description, the leaderboard, and the course descriptions. And each course was its own whole thing: a set of connected tasks that sometimes require to write programs in other custom languages and encoded in Galaxy. I will explain each course in the sections above.

The scoring was complex, but basically the team that gets the highest rank in each course wins.

Hello Course

The first course was called "hello" and the tasks were quite simple: read several pages from the "Galaxy HTTP" server (by sending Galaxy expressions evaluating to requests such as get index or get scoreboard), use the echo service (by sending a request evaluating to echo "something"), solve the basic language test (by evaluating an expression that used all the Galaxy operators).

Lambdaman Course

The first "real" course was devoted to solving the "lambdaman" tasks. Provided with a "labyrinth" map (in form of a Galaxy language expression, of course!), we needed to write a program that would navigate the map and eat all the dots. The map was a 2D grid with walls, dots, and a "lambdaman" character that could move in four directions. All the tasks were static and quite possible to solve even by hand, so the challenge was to provide a shortest Galaxy expression that successfully navigates a level. For example, for a level

###.#...
...L..##
.#######

the solution was UDLLLDURRRRRURR, written as Saaalalll~lllFllaa~laaaaaaa~ in Galaxy language.

As the solutions were scored in their Galaxy form, some tricks were possible to make them shorter (the obvious ideas were to implement random walker or some form of compression; it was valid to make a solution that executes for longer time, up to 1000000 steps, but has short written form in Galaxy language).

Spaceship Course

The second course provided a set of levels for a spaceship with inertial controls.

Each level had a set of points on 2d surface for the spaceship to visit, and we were able to control its thrust at every moment of time, thus indirectly affecting the velocity.

A solution for a particular level would be a string such as 236659, with each character being a number from 0 to 9, representing the thrust at each moment of time (acting as numbers on keypad in some games).

The score is based on the move number (notably, not their encoding in the Galaxy language, contrary to the previous course).

3D Course

This one was very interesting.

We were presented with a specification of so-called "3D programming language". The "program" is a set of numbers and instructions placed in a 2D grid, with third dimension being time. And there's a time-warp operator, allowing to send a number or an operator back in time, resetting the state of the program to some previous moment in time (but with additional things sent from the "future").

This was fascinating but also quite confusing.

I'll just leave an example program that, receiving a number in spot A, calculates its factorial.

.  .  . . . 0 . . . .
.  .  A > . = . . . .
.  .  v 1 . . > . . .
.  .  . - . . . + S .
.  .  < . . . ^ . . .
-6 @ -1 v . . 1 > . .
.  3  . . . . . A * .
.  .  1 @ 6 . . < . .
.  .  . 3 . 0 @ 3 . .
.  .  . . . . 3 . . .

Here, @ is the time-warp operator, accepting dt, dx and dy as operands on the bottom and on the sides, and the thing that it will move on its top. Once activated (i.e. all the operands being provided), it will roll back the program execution back in time.

The total score of the course was calculated according to "the amount of space-time" occupied by the program (so we were optimizing the latest moment in time its execution reached, together with the spatial dimensions of the 2D grid used).

The tasks were also interesting and varied in complexity: from calculating a factorial or an absolute value of the input, to calculating an amount of unique positions for Lambdaman on a dynamically-provided level (encoded as a long number).

(The latter task we were unable to solve.)

Efficiency Course

This course wasn't about solving nested tasks in derived languages, but about the Galaxy language itself. Several quite complex Galaxy expressions were provided, and we had to just evaluate them (and it required advanced analysis and knowledge of several tools and approaches).

Several problems I cracked myself included:

• a program calculating Euler's totient function for a given number in a really inefficient way,
• a program performing a linear search for a number whose bits satisfy a particular boolean expression.

The former we were expected to investigate and found an efficient way to calculate, while the latter we resolved using a SAT solver.

The Events

In this section, I'll describe the task and the contest's events in chronological order. When talking about dates, I'll refer to them in my local time zone, UTC+2 during the event.

Day 0, 2024-06-28

The contest started at 14:00 in my time zone. We've gathered in a Telegram chat, opened the repo, and started reading the task specification and figuring it out together. In the meantime, I have registered a team on the contest website, to get the data access key (and Minoru did the same, so we've had to ask the contest organizers to delete the duplicate).

I started sending some requests to check how the server behaves. We were provided with an initial request (the one meaning get index in the Galaxy language, though we didn't know that yet), so I tried to modify it and check what the server will return (it was returning error messages talking about invalid commands and page names, but again — we didn't know that yet).

We quickly figured out that out request, as well as the server responses, were just string literals (a simplest kind of expression), so we started working on decoder for these literals first. Decoding is really simple (you just remap 94 ASCII characters to alternate codes and get a Galaxy string after adding the S prefix), but that already caused a fair amount of confusion. Akon32, who was only briefly present at this time (so I won't list him as a team member), was the first to figure out the decoding, and decided to use tr to do some automated decoding (since we knew that SB%,,/}Q/2,$_ was Hello, World in Galaxian). This gave some pretty convoluted results, and we were discussing that a bit while figuring out that the decoding schema is easier than what tr was giving to us.

At this point we also figured that Minoru has outdated Telegram client (you know, Debian stable), and wasn't able to see some of our messages. Thankfully, this wasn't a big problem, but I had to keep in mind to not use certain advanced message formatting capabilities (custom quotes) in my messages so that Minoru can still read them.

Eventually, we were able to decode the index page that told us:

Hello and welcome to the School of the Bound Variable!

Before taking a course, we suggest that you have a look around. You're now looking at the [index]. To practice your communication skills, you can use our [echo] service. Furthermore, to know how you and other students are doing, you can look at the [scoreboard].

After looking around, you may be admitted to your first courses, so make sure to check this page from time to time. In the meantime, if you want to practice more advanced communication skills, you may also take our [language_test].

This page has some basic directions, and we started to take a look around, as it suggested. Since we agreed on using Haskell, I started reading about HTTP clients in Haskell.

I was struggling with figuring out my path through Haskell's string types. There are five different types: String (that's just a linked list of Chars and thus is never used for anything serious), Data.Text and Data.ByteString (the latter two having lazy and strict variants) and a lot of conversion necessary to get from one to another. (And these types are seemingly without any system enforced by some piece of Haskell ecosystem, e.g. the HTTP tutorial I followed suggested us to use a lazy ByteString for the most purposes.) This wasn't a blocked, but a bit annoying for me. Though I used to it after some time.

In the meantime, Minoru implemented a number decoded in Haskell, while Portnov did a quick HTTP script in Bash (thus introducing a concept of using the TOKEN.txt file that I've reused). Also, Portnov then implemented fileToGalaxy and fileToGalaxy commands, thus nailing the name "Galaxy" we used for the language (I, for one, would prefer to call it Cultic or something, but Galaxy it is).

If we believe his messages, Gsomix was brewing tea all this time (about 1.5 hours! Good tea!).

We've discovered all the course names after executing the get scoreboard request.

Minoru started implementing the AST module for the Galaxy language, while Portnov did a whole parser for it in Megaparsec (a Haskell parser combinator library). Gsomix decided to take a try on AST in F# (and threatened to call me several times, that was terrifying!), while also struggling with Haskell tooling on an AArch64 computer.

After performing some basic tasks from the Hello course (we didn't know that yet!), we have moved from 101st place to 55th. I have tried guessing how many tasks are there in the Hello course and how the scoring works, based on the behavior we observed.

I spent some time to push all the available pages to our repository, to have them available at hand at all times. Also, while listing all the pages, I found that some of them can't be decoded by the naïve approach our HTTP client used (because they were represented by full-blown Galaxy expressions, not just string literals). I have pushed these in their encoded form to the repository, so that we can decode them later.

Portnov and Foxtran started to solve Lambdaman tasks, while Minoru and Portnov were working on the Galaxy evaluator and corresponding encoder (to encode the stuff back).

We noted that several teams already started to solve tasks in the Efficiency course, while skipping the 3D course (as we learned later in the Spoilers document, they have used a "backdoor" the authors left for them — thankfully, it was also possible to get to the course legitimately).

We have learned to use echo service to print the results of arbitrary Galaxy expressions. So, since the language_test task was just a complex expression, we've tried abusing echo to get its result. Thankfully, the organizers have considered that people will try that, and it was refusing to print any results for the language test. We've had to improve our own evaluator to solve that task.

And at that moment GitHub decided our free credit for private repo's CI has come to the end, and it must spam my email with notifications about that. (Apparently, building Haskell programs takes quite a lot of time on CI if you don't keep any build caches between runs.)

Minoru delivered the evaluator, so we've tried to use it on several real-world tasks. Interestingly, it was telling about the "invalid application" on the language_test task, and I started investigation. I thought that there's a problem in our code and the error corresponds to some message in the Haskell evaluator, but actually that was a diagnostic message from the language test itself! It tried doing some basic calculations and check their results, env even print the helpful messages in case any of the calculations weren't correct according to the spec.

Thanks to help from Portnov, we've found out that there's a problem in how we handle recursive lambda definitions (we should "shadow" the variables in such case when they conflict, and we never did that). I told folks about what I know of de Brujin index, and they kept brainstorming in that direction for a while. And I tried to hack the language_test by decompiling it and reading the raw string fragments it contained (thankfully, the access code word wasn't included in its raw form, so I didn't succeed). Soon enough, Minoru finished the renumbering, and we were able to get the code legitimately. solve language_test 4w3s0m3 allowed us to move forward with completed Hello course.

Foxtran was solving Lambdaman tasks and writing some basic solvers for them in… wait, not in Fortran? He was using C++ and Python?! That's a surprise! But actually no, keep calm. He successfully wrote Fortran in C++ and Python. As expected. He was also drawing some graphs to figure out the solutions for Spaceship.

I wanted to write some basic TUI to solve Lambdaman tasks manually, so I decided to take a look at Brick, the Haskell terminal UI library. It turns out to be too complex, so after some reading I put that aside :(

In the evening, we finally opened the 3D course and started learning what is the whole "time-traveling programming" about.

And the day ended.

Day 1, 2024-06-29

Portnov was struggling with A* (in almost every competition, somebody from our team struggles with implementing A*) for Lambdaman, while providing some good solutions for tasks in the course.

In the morning, we were at 64'th place.

Minoru and Gsomix were discussing various approaches to the Spaceship course. It was clear that it represents a variation of the Travelling Salesman Problem, but the inertia complicates things a lot.

Minoru was profiling the A* algorithm and implemented some performance improvements, helping Portnov. Also, he discovered that it's possible to use RLE encoding to provide shorter solutions for Lambdaman tasks, and get more score this way (a fact we missed earlier).

Gsomix started manually solving tasks in the 3D course.

<Minoru>

Expectation: joyfully writing in Haskell.

Reality: joyfully writing Lisp in Haskell, then debugging tools for Lisp, and finally, slightly less joyfully, writing the solution of the problem in Lisp, and debugging it.

Portnov decided to translate Galaxy to Scheme for simpler evaluation: Scheme should have a better interpreter than the one we've just implemented on our own, right?

I started working on 3D simulator (one that will allow to debug 3D programs step by step) and writing the unit tests for various cases described in the 3D spec.

We have finally opened the Efficiency course. The course description told that there are a couple of auxiliary operators (not used elsewhere) that might help us, and Minoru cracked the first task down: replacing of call-byy-name to call-by-value is supposed to trim down the execution time. He immediately solved several more by just looking at them and figuring out what they try to calculate (in a quite inefficient way).

After that, Minoru joined me in 3D simulator implementation. The main parts he implemented were differential output (to see moving parts of the solution easier) and porting it all to a state monad, for easier programming. He also added equality operators for 3D, and various crash modes (the cases when the evaluation is expected to "crash" according to the spec).

At some point, for ease of test implementation, I decided to add something called "board normalization": after every move, we were rebasing the board into positive coordinates and removing the empty cells (so that boards different in position or in empty cells weren't considered as different), which caused some minor problems later.

Foxtran was implementing some novel sorting for the Spaceship course's solutions, and optimizing them quite fast.

Day 2, 2024-06-30

In the morning, we were at 59th place.

Gsomix solved the first bunch of task in the 3D course!

Minoru finished his part of work on the 3D simulator, so I took over and proceeded with the implementation.

We started occasionally using it, and discovered an annoying bug with the time warp operator messing up the viewport. Took me some time to fix it :)

To relax a bit, I've started working on the Efficiency tasks. The one I took included a Y combinator (and I was able to recognize it on the spot, huh!):

(Lambda 1
    (Apply
        (Lambda 2
            (Apply
                (Var 1)
                (Apply
                    (Var 2)
                    (Var 2)
                )
            )
        )
        (Lambda 2
            (Apply
                (Var 1)
                (Apply
                    (Var 2)
                    (Var 2)
                )
            )
        )
    )
)

Took me some time to refresh my memories on how to use it (thanks to Portnov for some hints!). I manually translated the function to Haskell, and then found that it executes a recursive function for some huge argument, and eventually decided to try calling same function for smaller arguments to see what results will it yield. The results were:

input : efficiency12
1 : 1
2 : 2
3 : 3
4 : 3
5 : 5
6 : 3
7 : 7
8 : 5
9 : 7
10 : 5
11 : 11
12 : 5
13 : 13
14 : 7
15 : 9
16 : 9
17 : 17
18 : 7
19 : 19
20 : 9
21 : 13
22 : 11
23 : 23
24 : 9
25 : 21
26 : 13
27 : 19
28 : 13
29 : 29
30 : 9

After some googling around and looking at OEIS, we found that it's essentially EulerPhi[x] + 1. It was an easy task to find its value for the argument it was trying to evaluate at the first place, and that was the answer.

After that, I took a look at a group of similar tasks that looked really huge and complex, but had similar patters.

Essentially, they were executing code like this:

for (long long x = 0; ; ++x) {
 if (reallyLongBooleanExpressionOnBitsOf(x)) {
  return x;
 }
}

The reallyLongBooleanExpressionOnBitsOf was different in two cases I considered, but eventually we've come to conclusion it's essentially a SAT problem. And the expression itself takes the form of

(bit[1] || bit[2] || !bit[3])
&& (bit[21] || bit[32] || !bit[11])

Here's the expression in its full glory:

(((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((!b17) || (!b14)) && ((!b13) || (!b8))) && (((!b18) || (b36)) || (b11))) && (!b38)) && ((!b19) || (b17))) && (((!b7) || (b15)) || (!b23))) && ((!b28) || (!b38))) && ((!b1) || (b18))) && (b14)) && (((!b36) || (b18)) || (!b5))) && ((b24) ||
 (!b22))) && (((!b16) || (b39)) || (b20))) && (((!b22) || (b34)) || (b23))) && ((!b29) || (!b27))) && (b14)) && (((!b36) || (b18)) || (b5))) && ((!b2) || (!b10))) && ((!b34) || (!b2))) && (((!b28) || (b38)) || (b21))) && ((!b26) || (!b9))) && ((b27) || (!b7))) && ((!b3) || (b38))) && ((b9) || (b25))) && (((b21) || (b13)) || (b14))) && (!b12)) && (((b35) || (b27)) || (
!b34))) && (((!b7) || (b15)) || (b23))) && (((!b6) || (b2)) || (!b39))) && (((b21) || (b13)) || (b14))) && (!b12)) && (((!b7) || (b15)) || (b23))) && (((!b18) || (b36)) || (b11))) && ((b9) || (!b25))) && ((!b19) || (!b17))) && ((!b7) || (!b15))) && (((!b2) || (b10)) || (!b22))) && ((!b15) || (b36))) && ((!b37) || (!b10))) && (((!b30) || (b12)) || (b13))) && ((!b32) ||
 (b18))) && (((!b13) || (b8)) || (!b28))) && ((b5) || (b15))) && (((b35) || (b27)) || (b34))) && ((!b18) || (!b36))) && ((!b4) || (b5))) && ((b9) || (b25))) && (((!b2) || (b10)) || (b22))) && (((b25) || (b36)) || (!b15))) && (((b21) || (b13)) || (!b14))) && (((b24) || (b22)) || (b37))) && ((b35) || (!b27))) && ((!b34) || (b2))) && (((!b33) || (b34)) || (!b36))) && ((!
b4) || (!b5))) && ((!b32) || (!b18))) && (((!b16) || (b39)) || (b20))) && (((!b29) || (b27)) || (b3))) && (((!b33) || (b34)) || (b36))) && (((b27) || (b7)) || (b28))) && (!b20)) && (((!b17) || (b14)) || (b38))) && (b39)) && (((!b2) || (b10)) || (b22))) && ((!b16) || (!b39))) && ((!b34) || (b2))) && ((!b32) || (b18))) && (((b24) || (b22)) || (!b37))) && ((!b26) || (b9)
)) && (((b35) || (b27)) || (b34))) && (((!b6) || (b2)) || (b39))) && ((!b10) || (b34))) && ((b5) || (b15))) && (((!b29) || (b27)) || (b3))) && ((!b10) || (!b34))) && ((!b31) || (b18))) && ((!b36) || (!b18))) && ((b25) || (!b36))) && (((!b29) || (b27)) || (!b3))) && (!b20)) && ((!b19) || (b17))) && ((!b8) || (b30))) && (((b27) || (b7)) || (b28))) && (((!b30) || (b12))
|| (!b13))) && (((!b23) || (b31)) || (b34))) && ((b11) || (b15))) && (((!b28) || (b38)) || (b21))) && (((!b13) || (b8)) || (b28))) && (!b38)) && ((!b3) || (!b38))) && (((!b36) || (b18)) || (b5))) && ((!b22) || (!b34))) && (((!b28) || (b38)) || (!b21))) && ((!b4) || (b5))) && (b39)) && (((b24) || (b22)) || (b37))) && ((!b1) || (b18))) && ((b11) || (b15))) && (((!b22) |
| (b34)) || (b23))) && ((!b30) || (!b12))) && ((!b33) || (!b34))) && ((!b31) || (b18))) && (((!b23) || (b31)) || (b34))) && (((b25) || (b36)) || (b15))) && ((!b37) || (b10))) && ((!b15) || (b36))) && (((!b6) || (b2)) || (b39))) && ((!b3) || (b38))) && ((!b6) || (!b2))) && (((!b23) || (b31)) || (!b34))) && (((!b33) || (b34)) || (b36))) && ((!b10) || (b34))) && (b0)) &&
 ((!b26) || (b9))) && (((!b22) || (b34)) || (!b23))) && (((!b17) || (b14)) || (!b38))) && (((!b18) || (b36)) || (!b11))) && (((b25) || (b36)) || (b15))) && ((b5) || (!b15))) && (((!b16) || (b39)) || (!b20))) && ((!b8) || (!b30))) && ((!b31) || (!b18))) && ((!b37) || (b10))) && ((!b8) || (b30))) && (((!b13) || (b8)) || (b28))) && (((!b17) || (b14)) || (b38))) && ((b11) || (!b15))) && ((!b15) || (!b36))) && ((b21) || (!b13))) && (((b27) || (b7)) || (!b28))) && (b0)) && ((!b23) || (!b31))) && ((!b1) || (!b18))) && (((!b30) || (b12)) || (b13))

(believe me, it was not easy to distill this out from a 1800-line Lisp file!)

After writing a parser, a C++ code generator (of all things!), and playing with bits for a while and constructing input for MiniSAT, I was able to solve one of the tasks.

Another one turned out to be different, though: it had several possible solutions, and we had to choose the minimal of them. To do that, I was producing solutions from SAT, sending them to the task server to validate, and I was blocking the highest bits of the number each time the server told me the solution is invalid. This way, I was gradually moving towards the minimal solution.

Pro Tip™: to find a smaller solution in SAT (using CNF form), block the high bit one by one by adding clauses looking like this:

-X 0

(where X is a bit number you want to block). Each bit should get one new separate clause (do not mix them!). In my solution, the following was required:

-42 0
-47 0
-50 0

(I skipped several bits, e.g. 49, because there weren't any solutions without these bits.)

While I was struggling with that, Foxtran wrote some Haskell (was not easy, but he was mostly confused by the same things I was when I started Haskell this time). And the folks were successful in generating more solutions for Spaceship.

Day 3, 2024-07-01

Foxtran proceeded to work on some graphical representation for the Spaceship tasks, and was actively seeking and optimizing solutions for them.

Gsomix found a checkered notebook that helped him to improve the speed of solving the 3D tasks.

Minoru and Portnov found a way to solve the remaining Efficiency tasks using Z3 solver (it was impossible to solve those in SAT).

I have finally fixed the problem with diff in the 3D simulator and tried to optimize some of our solutions, but didn't succeed.

Folks prepared some additional solutions for Lambdaman and Spaceship tasks, we uploaded everything, and the contest ended.

Contest End

Read more interesting facts (mind the spoilers!) in the organizers' repository.

The Results

At the end of the contest, we've had the 37th place out of 356. You can find our code in the team repository. Other participants' reports, if any, will be linked from there. (I may update this section at a later point with the final contest results, when they are available.)

Conclusion

I liked the tasks of this year. And even more: I think I found peace of mind while programming in Haskell! I did not struggle as much as the previous years with unfamiliar syntax, ecosystem and all that. At some point, I decided that my purpose is not only to solve the contest tasks, but also learn Haskell and other interesting things (such as SAT), and thus my purpose is fulfilled.

The organization was quite good, the tasks were interesting and varied (so it was possible for different people to look at different tasks in parallel, without much overlap).

So, yeah, it all was great. Hope to see y'all next year!