I have been bouldering on-and-off for a few years now. The first few
times I heard about bouldering, it seemed very unappealing to me. But,
forced by slight social pressure, I tried bouldering back in 2012.
And it was really fun! So, fun it did not even feel like exercising,
or at least not how I have previously experienced it. I would be
completely focused on the problem, not just trying to endure another set
or another lap around some track. Alas, I quickly stopped as life got
more busy…
Ten years go by. Life happens, and while I stay somewhat active with
hiking, I missed bouldering. But somehow I get started again. A group
from work is going, and I join. We climb every Friday, no exceptions.
Just what I needed to get back on the wall. It feels like starting
completely over, of course. I no longer rember what grades I climbed
back in 2012, but I remember making a bit of progress. But this time it
takes me a couple of sessions just to send a 5.
7A is the lowest grade with black tags in
my gym. The black tagged problems look fun, but thus far they have all
seemed impossibly hard.
After the first year or so, more busy life stuff happened, and I have
been struggling to get a climbing session in every week. But still, I
make some progress. Gradually, my forearms have been growing, and my
technique has improved. I do not consider myself a good climber, by any
stretch of imagination. None the less, I reached an important (for me)
milestone today:
I sent my first 7A!
A very modest achievement in the grand scheme of things. Many people
can climb a 7A. Even many people who have trained a lot less bouldering
than I have. Bouldering is not a source of pride for me. To me, sending
a 7A signifies the fact that I havent given up on training. Despite life
being busy, I keep going to the gym. For fun and for health!
TYPES 2026
Skyline of Lindholmen where TYPES 2026
was held. [Zoom in! 🔍
]
This week was TYPES 2026. As usual, TYPES was a nice conference, with
lots of likeminded people gathered to discuss type theory. I thought the
talks this year held a good level, especially the invited talks. And I
got to exchange ideas with new and old friends in the community. Zhili presented our joint work on higher kinded
containers.
I stayed in a hotel next to Karlatornet, which is the phallic tower
you see above. I quite enjoyed Gothenburg this time around, but did not
do much sight-seeing, except for dining excursions and a visit to Backa
Boulder. This year’s conference I felt was better paced than previous
years, where I have felt that there have been just too many talks, and
too busy programme.
There is something I haven’t mentioned here. But it is something I
have poured a lot of my spare time into the last year. There will be a
series on this website about it, someday… But for now, I will just leave
this video here.
There are still artifacts, still not super smooth. Still temp assets.
But there is light, there are shadows, and it was written in Haskell
(and GLSL), and there are no polygon meshes at runtime.
The modern-looking Firefox does not arouse joy in my heart. So, I
decided to apply a bit of styling to it, using
userChrome.css and Firefox Color. The
userChrome.css I set globally for all my machines via Home
Manager, while I have been picking the colours individually for all
machines, to match their individual colour themes. On my laptop, I went
with a beige variant:
As you can see, this screenshot was taken while I was looking into
what has been done about programming quantum computers using functional
programming languages. The left hand side of the window is occupied by
Tree
Style Tab – one of my absolute favourite Firefox extensions. The
font is EB Garamond Small Caps. One thing to note though, Tree Style Tab
is not affected by userChrome.css directly, but has its own
CSS styling in the advanced settings.
Crows might be my favourite bird. They look cool, they are smart and
they are much more polite than, say, pigeons or seagulls. Having noticed
that they all disappear from my neighbourhood at dusk, I found out that
they do communal
roosting at night. Isn’t that something?
NixOS has become my main operating
system as of late. I tried Nix, the package manager, a long time ago and
liked the concept! However, I was reminded about it existence a couple
of years ago, and since then I have gradually ported my machines to
NixOS, one by one. Currently, only the server you are receiving this
website from remains on OpenBSD. I might migrate it too, but that would
be a bigger project, as it is a machine I share with other family
members, and OpenBSD is just such a great server OS!
NixOS
The main thing which draws me to NixOS is the reproducibility and
automation. I flake all my
projects these days. That way my dependencies stay put, and I easily get
a consistent development experience no matter which machine I sit down
to code on.
Home
Manager is another draw. I used to have a repo with all my config
file and then manually symlink the files into the right location to
update them between machines. This worked very well, but was a hassle to
set up everytime I installed a new machine. Home Manager is a systematic
solution where you write your config in Nix and it builds the config
files and places them in the correct location! Many many programs have
built in support, and if the particular program you want to configure
does not have built-in support you can write your own, or just specify
the config verbatim.
I had a bit of an adventure installing NixOS my work laptop durign
Easter. I had not brought any USB stick to the cabin, so I was forced to
look for an unconventional solution. I quickly disregarded nixos-infect because
that shit should be illegal (I mean that in the most
complementary sense!). On the other hand the kexec seemed more
geared towards installing from a different machine. So I went the manual
route of loopbacking the normal installation ISO image from Grub:
It was a bit fiddly, but I got it working! I even remembered to copy
the image to RAM upon boot, so that it did not self-destruct during the
installation ☺
Been a while since I played on my synth. But it never disappoints. I
play for myself, and I can just lose myself in the sounds. This time I
ended up just playing into an effect module, and enjoying the fruits of
feedback:
Late night synth
This is of course not a “real” track, just a bit of (unlistenable)
improvisation. But, I really enjoyed the detuning of the delay
effect.
We are now a couple of weeks into the functional programming course,
and thus far we have covered untyped λ-calculus, simply typed λ-calculus
and algebraic types, functors and today we started on monads. The course
is fast paced, and we have some of the lectures at 8AM, which the
students and I both find a bit early. But for those early lectures I
bring a water boiler, Yorkshire tea, and crackers for everyone!
It is time for another round of my course INF221, “Advanced
Functional Programming”. The course has a lot of great topics, like
Software Transactional Memory, monad transformers, dependent types and
algebaric effects. Hope we have an interested crew of students this
year!
First lecture is tomorrow, and I am wondering how I will do my
lecturing. I hate the laptop the university provides for me, but I am
unsure if my HDMI converter for my iPhone play’s ball with the projector
in the assigned room. I love lecturing from the phone though.
Totally not creepy poster for the course!
This characteristic, uncanny valley, weird shit is one of few redeeming
quality of AI “art”.
Water, get back!
No water this week. Bergen is usually not a cold place – it
is mostly just wet and chilly. Even in winter the temperature rarely
stays below 0°C for long. But the last week and a half we have been in
the two-digit minus, and the water in our apartment completely froze
while we were in the cabin. I think the pipes are fairly new, and they
put too little insulation on them when they installed them. Because they
froze last year as well.
In the weekend it thawed a bit outside, and tonight we have water
flowing again. Looking forward to get some clothes washed and being able
to use the dishwasher!
Yesterday I spent some time getting an atom feed for this
diary. I had been deliberating for a long time how to do this, since
the entries are simply headers in the Markdown files. But I decided the
easiet would be to create a custom Pandoc Writer. The
site’s HTML is already generated using Pandoc, and so no additional
tooling was needed. Just a Lua-script and a new mkfile target. Since the
Atom generator was not an indepent package, I could have a very bespoke
script, without worrying of making it work for any other purpose than my
own. The only feature I added was an attribute for excluding entries
from syndication:
## 2026-01-04, Sunday {#2026-01-04 syndicated=false}
This entry would not appear in the feed.
There is something to be said of bespoke systems. We all love
abstraction, and general solutions. But the power of programming is that
one can make tailored solutions. We need the general tools, but we
should also make the general tools programmable, so that we can extend
them and adapt them to our purpose. Pandoc is such a great general tool.
With filters and custom readers and writers is is perfect for systems
that grow.
I am very happy about the result. I will also create an atom feed for
the rest of the pages on the site. But in that feed the default would be
for them to be unsyndicated, and syndicated=true in the
metadata header would publish them.
Git and large binaries
Another quality of life thing I did was to remove all large binary
files from the website repository. This used to waste around 15GB in
every working copy of the site. There is now a git ignored
media/ directory in my workdir, which has the same tree
structure as site-src/, but which is synced to a separate
central server location using rsync. The synchronisation is
hooked to git push and a commited manifest of hashes
connects commits to the state of the media files, ensuring that I can
deploy from any workstation without accedentally publishing the wrong
version of a binary file. So, any time I do mk deploy the
currently commited manifest is verified against the files pushed.
To test the website locally, there is a staging area, where I link in
the media files mentioned in the deployment index. Thus, I get an
accurate testing server on the workstation, before doing any actual
deployment.
All in all, I hope the improvement made over the holidays should make
working on the site a much smoother experience.
Wonderful times here at the cabin. Snow and good weather. I also
brought my computer so that I can work a bit. Yesterday I nixed the
development environment for my website, and reworked the
mkfile which builds and deploys it. I also separated out
the media files out of the git repo, so that they are no longer kept in
it.
Celebrating New Year at the cabin! Looking forward to the new year,
hoping it will be a good one!
Fireworks long since lost their magic for me, even though I still
walk outside to view them at the midnight stroke. It just seems like one
of these things which do not actually make sense once you think about
it. Yes, pretty colours and bangs are nice, but no doubt tomorrow we
shall read about all the eye injuries, the fires started, and the scared
to death animals.
Quite a lot fireworks around the cabin
this year. [Zoom in
🔍]
Found some old sketches I made many years ago in The Stockholm Logic
Seminar. At that time, the seminar was held in room 16 of building 5
at Kräftriket. Peter LeFanu Lumsdaine held the seminar, but I not sure
exact which one this was, maybe 2015 or 2016. Judging by the blackboard
content it had something to do with the semantics of type theory. I was
paying attention to the talk, but also just doodling away on my note
book. The result was a set of small sketches of the people listening, as
well as the speaker himself.
My original sketches were crude, so I will not be uploading those,
but I gave them to an LLM and asked it to clean them up slightly. I felt
they somewhat captured the characters in the room. I miss those days,
and I miss Erik in particular. My time as a PhD student at Stockholm
University was a good one!
Peter LeFanu Lumsdaine giving a talk at
The Stockholm Logic Seminar [Zoom in 🔍]Per Martin-Löf listening attentively. He
always ask insightful questions during talks. [Zoom in 🔍]Erik Palmgren organised the seminar in
those days. [Zoom in
🔍]Jacopo Emmenegger was a PhD student in
Stockholm at the same time as me. [Zoom in 🔍]
Elisabeth and I went hiking in Kvanndalen. The terrain was slightly
more challenging than we expected, but the reward was stunning views and
beautiful surroundings. At times we really had to cling to the sides of
valley above steep gorges. We camped roughly in the middle of the
valley, just slightly further down than the farthest one can see on the
picture below. We originally planned hiking around and back to
Haukelisæter again, but our slow progress the first day meant we opted
to walk down to Bleskestad, just above Roalkvam, and get my father to
pick us up.
Spending the (long) weekend in Vågsli at my parents cabin. Perhaps
the last weekend before the snow. I was here a couple of weeks ago, and
then it was snowing. But the snow melted again.
Over the winter, I have been refining a Haskell library of functions
for doing Applicative Logic. The idea is that a lot of functions
involving booleans can be generalised to work on any Applicative Functor
(possibly applied to Monoids), through the isomorphism
Bool ≃ Maybe () – where Maybe is the
applicative functor and () is the monad.
Been to HoTT-UF 2024 in
Leuven, Belgium. Which was really nice! Both Thorsten Altenkirch and his
PhD student, Stefania Damato, were giving container-themed talks, which
has rejuvenated my interest in containers. Thorsten and I discussed
higher-order containers after his talk, and we both had ideas for how to
it.
So, tonight I found myself trying in vain to start the car, with the
boot full of shit. Literally, shit. I was on my way to empty the
aforementioned Porta Potty and apparently the battery was flat.
Luckily, the place to empty is just a
15-minute stroll from here! [Zoom in
🔍]
Today was the first lecture of my new course, INF221: Advanced Functional
Programming. The little room which had been assigned to us was
packed, but hopefully we will get a bigger room.
Today our long awaited bathroom renovation starts. In a few days time
we will have to do our business out on the balcony in a Porta Potty. At
least we will have a view towards Ulriken as we take a shit.
Lille-julaften (“Little Christmas Eve”) here in Norway. As usual, I
am visiting my parents over the holiday, along with the rest of the
family. This year’s new arrival, my sister’s daughter, is getting to
know her cousins. In the evening we played the Dune boardgame, which is
so much fun! Especially the battles are nerve-wrecking!
The spice must flow on Arrakis! But so
too must the caffeinated drinks, keeping us sharp in intrigues that last
into the wee hours. [Zoom in
🔍]
Had an evening by myself. Spent most of it deep into my synth,
exploring sounds and melodies. At some point I felt like I was having a
party:
The sound is sub par since I was just recording it through my iPhone
7. And I made no recordings, but sometimes the point is just to play for
my own enjoyment.
Starting to see the end of the term approaching. Less than a month
until my students have their final exam. For me “to see a date
approaching” is quite literal. I see dates very clearly in my mind. They
are distributed counter-clockwise on a roundish landscape which
represents the year. As the year progresses my vantage point in this
landscape moves so that I always see things from today’s date. Thus, the
coming dates are approaching. There is also a kind of covering-space
effect where the actual dates over many years cover the same landscape.
In a path-lifting kind of way, I can see forward into the future, say
next march, or backwards to the past, say to the previous march.
Went bouldering after work with a group of co-workers. It’s been a
busy week, so it was good to just go do something physical. Climbing is
a good way to exercise because it is just fun enough that you don’t
notice that you are exercising. Each bouldering route is like a puzzle.
Of course there is skill and physical form involved, but your
thinking-brain is also involved. You need to figure out how to position
your various limbs and move them in order for the route to be
possible
I am starting to get the hang of MidJourney now. And it is exciting!
I like discovering what my prompts turn into. I don’t know anything
about Brownsville, but I like the result which the word “Brownsville”
prompted below!
«Dancing on the streets of Brownsville»,
medium: MidJourney [Zoom in
🔍]
Back at work for almost two weeks already. Mostly preparing for
teaching functional programming.
Generative art
I have discovered MidJourney, one of these machine
learning image generation tools where you write a prompt and it
generates an image. It is really fun! Of course it has its strengths and
weaknesses. But, more than with other “AI things”, I feel like this has
real, human value. Also, the community around MidJourney is
exciting.
A mindflayer, adapted to a D&D
champaign set in a fantasy dessert world. [Zoom in 🔍]
Generative art is nothing new. The core of generative art is that you
write an algorithm which generates the art, rather than “performing it”
yourself. Often you incorporate some source of randomness into the
process, so that you can get a number of variations on the same theme.
The algorithm can also take some user input, which affects the result in
some way.
In the case where you wrote the algorithm, the result is clearly
art you have made. But even if you are merely using someone
else’s algorithm, you might claim that the result is art you have
made, if one or a combination of the follow two cases hold:
Your input to the algorithm enabled your artistic expression.
Your selection of this output from many randomly generated outputs
enabled your artistic expression.
Musical example
Here is a simple example from music of the second case: In modular
synthesis you make music by connecting modules together to form a
synthesiser.
Often the notes played is determined by a sequencer module, instead
of using a keyboard. Some sequencers allow you to program in a sequence
of notes played manually, but there is a sequencer called “Turing
Machine”1 which generates random sequences of
notes.
The crucial thing about the Turing Machine is that it will play
random notes until you lock it. Once the sequence is locked it will keep
playing the last generated sequence until you unlock it. So, to produce
a cool bassline for your track, you connect the Turing machine to the
bass modules, and listen to its random playing until you find something
you like. Then you lock it in, and that’s it! Clearly it is your
bassline because you chose it among all the ones generated by the
Turing Machine.
Here is a track where Mutable Instruments’ Marbles, another
module like the Turing Machine2, is used to decide the
melody played:
Foot Stomp
The theme you hear repeat a few times throughout track was chosen by
just letting Marbles “roll the dice” until a catchy melody came out.
Then I was free to focus on other parts, such was how to make the most
bad-ass distorted sound to play that melody with.
BTW, that distorted sound is a harmonic oscillator (sum of related
sine waves) modulating a through-zero FM oscillator. Controlling the
distribution of sines gives absolutely interesting shifts in timbre!
DALL-E, MidJourney and others
Currently, there are several competing prompted-image-generators. But
the idea is that you give a short prompt such as “The invention of pizza
by god, Italian renaissance painting”, and the program spits out:
A critical moment in time, forever
captured by this renaissance painting. [Zoom in 🔍]
In MidJourney the output is actually four images, and then you can
iterate, making variations on each of them. This means that both the
first and the second point above apply. The user provides both input to
the algorithm, and selects from a supply of randomly generated
output.
In both ways this enables the user to express themselves
artistically. And this is the value I see in this: it enables
more people to express themselves creatively using computer
graphics. For instance, I will use MidJourney when creating
concept art for my D&D sessions. The dessert mind flayer above is
way better drawn that I would have been able to if I sat down in Krita
or Blender.
Now, I don’t think MidJourney or DALL-E are any threat to actually
skilled artists. A human artist actually understands what they are
drawing, and can be relied upon in a completely different way. The
pictures generated by MidJourney usually have very recognizable
artefacts. And most importantly, the control you have when generating
the picture is very tenuous. You might have a perfect idea in your head,
but the algorithm is not a mind reader, so the picture coming out is
usually completely different. Sometimes that’s OK, and a cool feature.
But for most of the kind of work you pay an artist for, it would be
completely useless.
Also, artists often produce 3D models, which can be rendered in
different settings and reposed. This has very high utility compared to
the lump of pixels from MidJourney.
No relation to the mathematical model of computation,
except for the name.↩︎
Marbles has the advantage of being able to do
non-destructive variations, where you randomize the notes for a time
then return to the previously locked tune.↩︎
This week we returned from a vacation trip to Stockholm. The SAS
pilots are on strike, because SAS broke the contract they made to rehire
pilots after the COVID-19 pandemic crisis was over. Our plane to
Stockholm was scheduled 13:25, and the strike was due to start 12:00.
But it turned out, that while it is a SAS route, SAS was not actually
flying the plane – CityJet was. So, we got both there an back again
despite the strike.
Synthy times
Today, I spent some quality time with my synth. The rack was
reorganised earlier in the week and I tidied the desk it stands on. I
still struggle a bit with doing several takes on multitrack recordings,
but some progress is being made: A new clock divider now makes it
possible to use the KeyStep 36 as a clock source. The KeyStep also
starts the recording, so with a bit of practise I should be able to sync
the different takes up directly.
The track I recorded today was initially by the new layout of the
modules, where a choice of voices (oscillators + filter/wavefolder +
envelope generator + vca) have been constructed. Aaaand, Rings is
playing a baseline ☺
Looking through the memory card, I found a few other tracks which
were recorded, but not edited. So, I got those done as well. I actually
do very little editing after recording. All effects and mixing is done
at the synth. All I really do is to even the levels a bit of different
parts of the track.
Since there was a few weeks since I recorded these, I cannot really
remember what inspired them. But you can listen to them here:
Actually, listening back to these, I remember that “Toy box” is in
fact just the Qu-bit surface, cycling through different modes.
As one might, I have been watching the fourth season of Stranger
Things, and in the fourth episode there was a moment – a little joke –
which I derived great pleasure from. Mostly because I imagine not a
whole lot of people would notice or have the prerequisite knowledge of
English garden landscaping to laugh at it.
So, for your benefit, so that you can also enjoy this little moment
of the episode, let me introduce the “ha-ha”:
A comparison between ha-ha and regular
walls. (842U / Wikipedia / Gnu Free Documentation
Licence)
As you can see, a ha-ha is kind of a wall, but the ground on one side
is as hight as the wall. A ha-ha is useful when you want a wall, but
don’t want to ruin the view from the inside. Here is a real world
example:
Hopetoun House ha-ha. (Andrew Shiva /
Wikipedia / CC BY-SA 4.0)
And here is one from one of my MineCraft castles:
A ha-ha keeps the monsters out of my
MineCraft home
Back to Stranger Things. In episode four of the forth season, Nancy
and Robin visit an asylum in an attempt to get one of the inmates there
to talk about how a demon killed his family fifty years ago. They
pretend to be psychology students, and while they are given a tour of
the place, we briefly see what looks like a ha-ha. So, like anyone with
an interest in obscure walls, I nodded to myself: “Ah, see now there is
a nice ha-ha, if ever I saw one.”
Nancy and Robin get to talk with the fellow, but in the end their
cover is blown, and they have to make a run for it. And as they do, we
get a great shot showing how ha-has are almost invisible from the
top:
Do you see that there is a wall
here?
For a moment I worried that they would not notice the drop and fall.
Indeed, one can imagine the origin of the term “ha-ha” to be “Ha,ha! You
fell and broke your leg!”. But they actually jumped down rather
gracefully:
Down the ha-ha!
And then, the creators had a brilliant idea, as a tip of the hat to
anyone enjoying the landscaping at the asylum, one of the inmates
exclaims “Ha ha ha ha ha ha!”.
In Stockholm for a meeting in the EuroProofNet COST action’s 6th
working group. Feels good to visit Kräftriket one last time before
the math department there moves to new facilities across the road.
Kräftriket is so beautiful in summer, and I have many fond memories from
my time there. Even got to say hello again to Per Martin-Löf who is
still active in attending seminars!