µ-Posts (What is this?)

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.

Something I've been noticing for some time, nicely summarised by Alex Russell. He gives a wonderful overview of how Apple is intentionally degrading the user experience on the web and forces users to use native apps instead of web apps (and hence makes more profit from their App Store). The full article can be found on Alex's blog infrequently.org/2021/04/progress-delayed/.

The thing I hate about this the most is that it shows how Apple is affecting all users indirectly, no matter if they use their products or not.

Why some developers are avoiding app store headaches by going Web-only: https://www.fastcompany.com/90623905/ios-web-apps​

With FLoC being deployed to Google Chrome automatically, browser fingerprinting (and therefore tracking users across the internet) becomes even more powerful than it was before.

At least there are some tools that help us fight it, namely EFF's amifloced.org and the DuckDuckGo's wonderful privacy extension now blocks FLoC.

The irony of this is that these tools will be mostly used by power users only. So the regular users will be tracked even better because of FLoC and power users probably can't easily defend themselves against fingerprinting because their settings are so unique that fingerprinting their browser is a piece of cake. A great example of divide and conquer!

The people working in Univalent Type Theory (also known as Homotopy Type Theory) will tell you that its advantage is that you can work with equivalent objects as thought they were equal. But I think the opposite is true. Since you need to compose the proofs of equality everywhere, you're effectively working with equality as if it was just an equivalence 🙃.

A great video by TechAltar on what has the GDPR achieved in the 3 years of its existence https://www.youtube.com/watch?v=v_W0wR4AClk.

Google banning Element.io from their Play Store because of suspicious content on Matrix network. This is the same as if they banned some e-mail client because they noticed that people share misinformation that way.

Meanwhile Element.io have written a blog post about the story.

There's a growing case being made with each passing year that if there's hope for the social web, it's in small communities. It's built on protocols like ActivityPub, rather than on one-stop “gated” (i.e. proprietary) platforms. Whereas our social giants are built from the start for unaccountable inequity, a web of small, connected communities has the ability to give us true “town squares” run by humans and organizations that are closer to their users, and answer directly to them.

Big news: My friend William DeMeo has announced that he's formalised Birkhoff HSP Theorem in Martin-Löf type theory using Agda. Details on ualib.gitlab.io.

A lot of people are switching from #WhatsApp to #Signal these days. I don't like where it's going. Messaging should be as decentralised as e-mail is, otherwise we're heading to the same problem as we had with WhatsApp. Who guarantees that Signal won't be acquired by somebody we dislike in the future? For example, Matrix is a better alternative as its decentralised protocol guarantees that it can't be fully owned by anyone. (And there are possibly more options.)

Just received a YubiKey from CZ.NIC (in exchange for writing about it with #overenomojeid). After setting up the two-factor authentication in mojeid.cz I can easily manage my citizen profile. It's great to see some progress in Czech "e-governance".

While being stuck in England because my flights were cancelled, I watched a Moshe Vardi's talk that aptly argues against Cyber Libertarianism, why we can't reach (economic) equilibria and more. His OWLS talk is here youtu.be/BipEbkdbVNc.

IT'S OFFICIAL: @gitchat@twitter.com now natively speaks Matrix!! Read all about what it takes to add native Matrix support to a large existing chat app, and bask in the glow of a world where FOSS chat is increasingly FOSS, open & interoperable once more :D 🎉🥳🍾🌉🚀 https://matrix.org/blog/2020/12/07/gitter-now-speaks-matrix​