Elisabeth and I are on vacation in Gotland this week. We are staying at her family cabin, suitably far from civilisation. A cow. [Zoom in 🔍] Avoiding platitudes about the scenery, I will just report that is a wonderful break, and that there has even some Agda code written at the cabin! Gotland. [Zoom in 🔍]
∞-Categories at Mittag-Leffler Visiting the Mittag-Leffler institute this week. A pleasant stay thus far, with lots of great researchers gathered to push towards formalisation of ∞-categories. Surprising amount of progress is being made here. Especially in the synthetic methods. Agda, with its flexible type system and liberal collection of extension (not unlike GHC), is at an advantage here. I…
Bouldering 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…
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…
Light & Shadows 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…
Firefox styling 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: Firefox on…
Crows 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? Crow on top of Løvstakken
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…
Thinking hard about capability based security these days. More on this later.
Late night synthing 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.
Tenure track: [██████████] 100% complete! As of today, I am a professor at the University of Bergen. The sign on my office door! (Still feel like it says “ 404 – Håkon not found”) Zoom in 🔍
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…
Lecturing Advanced Functional Programming, again! 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…
Last day at the cabin, before heading back home. Atom feed! 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…
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. The mountain is beautiful! [Zoom in 🔍]
New Year 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…
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…
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…
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. There is a more complete write-up here on my website, and I…
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. Approaching Brussels. [Zoom in 🔍]
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…
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.…
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…
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,…
Vacation 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…