Zumi's Blog

#cooking #recipe #vietnamesefood

Just writing down what this video is doing for my own reference.

... is the GTK's default gtk-font-name settings.

What is system-ui?

You can change them in .config/gtk-4.0/settings.ini (or .config/gtk-3.0/settings.ini) like this:

gtk-font-name=Font Name 10

Read more to see how I found it.

This is a web version of my last semester project report.

Introduction

In functional programming, it is common that programmers describe the possible side effects of a function in its signature. This can be expressed by returning a monad, or by expressing the capability to use the side effects as a parameter of the function. Scala uses the notion of contextual parameters (“Contextual Parameters, Aka Implicit Parameters” n.d.) for such capabilities, allowing the programmer to delegate to the compiler the tedious work of explicitly writing down an (obvious) instance of the capability when calling that function:

def sqrt(x: Double)(using {*} CanThrow[Exception]) =
    if x >= 0 then builtin.sqrt(x)
    else
        throw new Exception("sqrt of negative number")

However, often, the capabilities exist only as a proof of existence for static type-checking purposes, and is never interacted with during the execution of the program (other than being passed around). Hence, this style of programming creates a runtime overhead that we wish to avoid. Erased definitions allows the programmer to explicitly mark a definition/parameter as unused at runtime, guaranteeing that they are optimized away during compilation. The compiler should also guarantee that erased definitions are not referenced to at runtime, and the observable behaviour of the program does not change after erasure of these definitions. Scala already has erased definitions as an experimental feature (“Erased Definitions” n.d.), however the feature is incomplete and has some soundness issues (“Unsoundness Due to ‘Erased‘ · Issue #4060 · Lampepfl/Dotty” n.d.).

Made some efforts to move kjudge to use Parcel 2.

#nix #hosting

Lately I have been switching my primary Linux PC from Arch Linux to NixOS, a Linux distribution with a functional twist: completely stateless configuration. It's been quite a pleasant ride, and Nix the expression language, though a bit lacking in friendly documentation, is actually not that hard to get used to (... but the nixpkgs.lib functions are not!)

With the help of home-manager, a Nix module/program that manages user-specific configuation in the same Nix language, I have a completely working .config with all the relevant programs installed (kak editor, fish with my bindings, ...) completely synchronized between my M1 MacBook Air and the Linux PC.

Of course, to expand the reach of Nix, I decided to move my DigitalOcean node, where I run my Discord bots, a personal email server, a git server and a small photo store, to NixOS as well.

This is a short overview of Philip Wadler and Robert Bruce Findler. 2009. Well-Typed Programs Can’t Be Blamed. In Programming Languages and Systems (Lecture Notes in Computer Science), Springer, Berlin, Heidelberg, 1–16.

#css #tailwind

I am working on an experimental Codefun frontend, codenamed Mashiro, written completely in Elm using the Tailwind.css “framework”.

The UI's main idea is to capture most content into card-like objects floating on a greeny background. Something like this:

You can see that the main “Problems” represent a floating card, while the left side navbar represents some more floating cards.