µ-Posts (What is this?)

The new online #EU legislation, the DMA, is a very good reason to be proud of the EU this time around. Although, it's not perfect, we're setting the right trend.

I'm usually against laws that aim to completely change some industries from ground up, instead of doing careful incremental improvements. However, this needed to happen at some point because the key global players failed to do the right thing over and over again, in exchange of some parts of their profit. Playing nice is not cool, so we have to make it mandatory.

Next target, repairability!

Well-written explanation of what Apple's policies do to the internet ecosystem. (All arguments supported by evidence.) The conclusion is quite clear, here are some key points:

... there's reason to think that Mozilla would not have suffered layoffs if Apple were an ally of engine choice. Apple's policies have made the web a less compelling ecosystem, and its anti-competitive behaviour has driven up costs for browser makers while starving them of revenue ...

Okay, so I've added also vim-startify to my NeoVim set-up and started playing with lazygit and fzf. This is precisely the reason why avoided plugins in the first place, there is no end to this. I will not do any customisations of my set-up for at least a month, I promise! 😅

Up until a week ago, the only Vim plugins that I was using were goyo.vim and lightline. It all changes suddenly and my no-plugin life I've been living since ever has changed upside down. Now I'm also adding vim-easymotion, vim-fugitive and vim-vsnip. I would also use telescope.nvim if had a higher version of NeoVim. 🙂

Why have I not used #Vim snippets earlier? I especially like that with vim-vsnip I can have snippets to write other snippets :-).

Also the command :VsnipOpen is really handy, to add/edit snippets on the go.

I admire when somebody perfects their set-up of something they do regularly. When I was writing my thesis I needed to draw a few images and I didn't want to spend whole days of making it in TikZ by hand. For that reason I found out that I can use Inkscape with svg2tikz to draw the diagrams in Inkscape and convert the resulting SVG into a TikZ source. The caveat of this is that if I wanted to have LaTeX formulas in the Inkscape image and svg2tikz script would escape them, making them rendered incorrectly. As a simple fix, I just patched svg2tikz by changing what characters need escaping. All that was needed was to change the definitions

SPECIAL_TEX_CHARS = ['$', '\\', '%', '_', '#', '{', r'}', '^', '&']
SPECIAL_TEX_CHARS_REPLACE = [r'\$', r'$\backslash$', r'\%', r'\_', r'\#', r'\{', r'\}', r'\^{}', r'\&']

to just

SPECIAL_TEX_CHARS = ['%', '#', '&']
SPECIAL_TEX_CHARS_REPLACE = [r'\%', r'\_', r'\#', r'\{', r'\}', r'\^{}', r'\&']

This worked beautifully. I added a couple of simple bash scripts to automate the whole process but it wasn't anything fancy. I used this set-up a couple of times when making slides and also in my thesis where I only had 9 images, so why bother perfecting it further? :-)

Today I discovered this fantastic blog post by Gilles Castel, who takes a very similar approach to the next level. He doesn't use svg2tikz but instead uses the internal Inkscape tool that creates a TeX template to be included in the document. But then he creates a really smart collection of Vim, Inkscape and other scripts to make the process of creating SVG images, storing them at the right place, generating the required LaTeX code, and importing it where it's needed really seamless. It is really wonderful and if I ever find myself needing to create dozens of TikZ images, I'll definitely copy a lot from that approach.

I also highly recommend looking at Gilles's other blog posts, where he also explains how he streamlines his other LaTeX and research related tasks. Also, on the topic of TikZ, I also recommend quiver helps with making TikZ diagrams. For converting svg to TikZ there's also pictikz but I haven't tried that one before.

Just learned about F*. Looks very interesting. I wonder how it compares to Coq, Agda, Lean, ...

A nice summary by an Iranian who was jailed for his blogging in the first decade of the 2000s. He then came back from prison, into the world of social media. Very interesting read. Especially, I like this paragraph about deplatforming voices.

In a free-market economy, low-quality goods with the wrong prices are doomed to failure. Nobody gets upset when a quiet Brooklyn cafe with bad lattes and rude servers goes out of business. But opinions are not the same as material goods or services. They won’t disappear if they are unpopular or even bad. In fact, history has proven that most big ideas (and many bad ones) have been quite unpopular for a long time, and their marginal status has only strengthened them. Minority views are radicalized when they can’t be expressed and recognized.

Microsoft has changed in recent years, however, still not enough: Windows 11 blocks Edge browser competitors from opening links

I've just ordered a new smartphone, with a 10-year warranty. Check it out too! https://10yearphone.com #10yearphone

And if it doesn't arrive before my current phone breaks apart, I'll get a #Fairphone with a 5-year warranty https://www.fairphone.com, which can be got now :-)

Just found out that "Learnability (in machine learning) can be undecidable, that is, independent of set theory". From the abstract:

Consider the following statistical estimation problem: given a family F of real valued random variables over some domain X and an i.i.d. sample drawn from an unknown distribution P over X, find f in F such that its expectation w.r.t. P is close to the supremum expectation over all members of F. We show that, in some cases, a solution to the ‘estimating the maximum’ problem is equivalent to the continuum hypothesis and is therefore independent of the set theory ZFC axioms.

Details (which I haven't read) are here and here.

I wish I read Jean Goubault-Larrecq's Quotients, colimits of dcpos, and related matters in the first year of my PhD studies. I had to reinvent a lot of these ideas from there (and then apply them transfinitely) in my papers on free constructions and quotients of d-frames...

Attending my first fully hybrid conference! (All thanks to the brave folks behind ACT 2021)

There are speakers, chairs, audience some attending in person and some online and in all possible combinations.

Dana Scott on category theory:

"The author himself does not always like or enjoy the discipline of category theory, which seems ofttimes to carry along very, very heavy machinery and odd terminology, but he long ago came to the conclusion that it is quite unavoidable."

From his 1993 paper "A type-theoretical alternative to ISWIM, CUCH, OWHY" (originally written in 1969).

I just found out about a new Haskell extension called DerivingVia. It looks incredibly powerful, especially when paired with DerivingStrategies and GeneralizedNewtypeDeriving. It would save me from writing a lot of boilerplate in the past! For details see this great YouTube video by Tweag.

Edit (on 29 July): Matt Parsons has written a blog post on how this might become a bit overwhelming in more complicated examples and how he proposes to fix that (also related proposal). An interesting read.

Edit (on 13 Feb 2021): Just found this blog post by Hans Hoeglund which beautifuly utilises DerivingVia in his iso-deriving package.

Edit (on 4 April 2023): Gabriella Gonzalez wrote a nice blog post explaining how DerivingStrategies and GeneralizedNewtypeDeriving can be used to tame deriving.

Edit (on 02 Sep 2023): There's another nice example of the usage of this on Sam Tay's blog.