Joachim Breitners Denkblogade
Earlier this week a colleague of mine, Emilio Jesús Gallego Arias, shared a demo of something he built as an experiment, and I felt the desire to share this and add a bit of reflection. (Not keen on watching a 5 min video? Read on below.) What was that? So what did you just see (or skipped watching)? You could see Emilio’s screen, running VSCode and editing a Lean file. He designed a small…
In 2007, Martin Escardo wrote a often-read blog post about “Seemingly impossible functional programs” . One such seemingly impossible function is find , which takes a predicate on infinite sequences of bits, and returns an infinite sequence for which that predicate hold (unless the predicate is just always false, in which case it returns some arbitrary sequence). Inspired by conversations with and…
Back in March, with version 4.17.0, Lean introduced partial_fixpoint , a new way to define recursive functions. I had drafted a blog post for the official Lean FRO blog back then, but forgot about it, and with the Lean FRO blog discontinued, I’ll just publish it here, better late than never. With the partial_fixpoint mechanism we can model possibly partial functions (so those returning an Option )…
A few months ago I explained that one reason why this blog has become more quiet is that all my work on Lean is covered elsewhere. This post is an exception, because it is an observation that is (arguably) interesting, but does not lead anywhere, so where else to put it than my own blog… Want to share your thoughts about this? Please join the discussion on the Lean community zulip ! Background…
For many years I wished I had a setup that would allow me to work (that is, code) productively outside in the bright sun. It’s winter right now, but when its summer again it’s always a bit. this weekend I got closer to that goal. TL;DR: Using code-server on a beefy machine seems to be quite neat. Passively lit coding Personal history Looking back at my own old blog entries I find one from 10 years…
The setup Imagine you are living on a riverbank. Every now and then, the river swells and you have high water. The first few times this may come as a surprise, but soon you learn that such floods are a recurring occurrence at that river, and you make suitable preparation. Let’s say you feel well-prepared against any flood that is no higher than the highest one observed so far. The more floods you…
This blog has become a bit quiet since I joined the Lean FRO . One reasons is of course that I can now improve things about Lean, rather than blog about what I think should be done (which, by contraposition, means I shouldn’t blog about what can be improved…). A better reason is that some of the things I’d otherwise write here are now published on the official Lean blog , in particular two lengthy…
I like using one machine and setup for everything, from serious development work to hobby projects to managing my finances. This is very convenient, as often the lines between these are blurred. But it is also scary if I think of the large number of people who I have to trust to not want to extract all my personal data. Whenever I run a cabal install , or a fun VSCode extension gets updated, or…
After seven years of service as member and secretary on the GHC Steering Committee, I have resigned from that role. So this is a good time to look back and retrace the formation of the GHC proposal process and committee. In my memory, I helped define and shape the proposal process, optimizing it for effectiveness and throughput, but memory can be misleading, and judging from the paper trail in my…
It was pointed out to me that I have not blogged about this, so better now than never: Since 2021 I am – together with four other hosts – producing a regular podcast about Haskell, the Haskell Interlude . Roughly every two weeks two of us interview someone from the Haskell Community, and we chat for approximately an hour about how they came to Haskell, what they are doing with it, why they are…
Tomorrow is going to be a new first day in a new job for me: I am joining the Lean FRO , and I’m excited. What is Lean? Lean is the new kid on the block of theorem provers. It’s a pure functional programming language (like Haskell, with and on which I have worked a lot), but it’s dependently typed (which Haskell may be evolving to be as well, but rather slowly and carefully). It has a refreshing…
TL;DR: Squash your PRs with one click at https://squasher.nomeata.de/ . Very recently I got this response from the project maintainer at a pull request I contributed: “Thanks, approved, please squash so that I can merge.” It’s nice that my contribution can go it, but why did the maintainer not just press the “Squash and merge button”, and instead adds the this unnecessary roundtrip to the process?…
At this year’s ICFP in Seattle I gave a talk about my rec-def Haskell library, which I have blogged about before here. While my functional pearl paper focuses on a concrete use-case and the tricks of the implementation, in my talk I put the emphasis on the high-level idea: it beholds of a declarative lazy functional like Haskell that recursive equations just work whenever they describe a (unique)…
I sometimes write papers and part of paper writing is assembling the bibliography. In my case, this is done using BibTeX. So when I need to add another citation, I have to find suitable data in Bibtex format. Often I copy snippets from .bib files from earlier paper. Or I search for the paper on DBLP , which in my experience has highest quality BibTeX entries and best coverage of computer science…
I submitted a Functional Pearl to this year’s ICFP and it got accepted! It is about the idea of using Haskell’s inherent ability to define recursive equations , and use them for more than just functions and lazy data structures. I blogged about this before ( introducing the idea , behind the scenes , applications to program analysis , graph algorithms and minesweeper ), but hopefully the paper…