Reader

Made some efforts to move kjudge to use Parcel 2.

1. What's “module” mode?

Basically it's the adoption of ES modules-style imports to the browser. They look nice, but they are now strongly isolated. That means, code modifying global variables like window are no longer possible. Sounds great, until you realize that it's one of the “normal” way for HTML-inlined JS to work with “imported” JS.

What we have instead is an export mechanism, which does what you think, just like how ES modules work in Node.js, TypeScript and the like. You can even import them from the browser, like this:

<script type="module">
  import { func } from "./module.js";
  
  // call func
  func();
</script>

However I'm not yet sure on how those things work yet. One thing I know is that I've been abusing globals like window for most interaction with go-generated HTML and independent TypeScript code in kjudge.

And that did not go well with Parcel 2...

2. Parcel 2

Parcel 2 decided to push the standard to the extreme, requiring all TS/JS code with imports to be imported (from HTML) as modules. This means that as long as you import anything (not just other JS/TS files but also images, audio, ... anything you can think of with a Parcel magic import), you live with an isolated JS/TS file. Why is this a strong requirement? I get it for code import, but for resources they don't make a lot of sense, especially when they also are making it explicit that what you get is just an URL...

Even worse, Parcel has some logic to inline the script content into the HTML once imported, making static global variables totally impossible (yay?).

3. Pain

I haven't found a nice way out of this yet. Perhaps changing inlining rules? Perhaps a way to compromise with the import algorithm?

We'll see once I have time for this again :)

Things should work now as they should. Or so I hope.

Giving some code a try...

str :: String
str = "Hello World!"

main :: IO ()
main = putStrLn str

See ya :3

#welcome

#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.

What are the goals of a remote NixOS configuration?

• Well, for a starter, it should be able to run all the stuff I have been running. This is actually not trivial. I run most of my stuff on the old DigitalOcean node as a bunch of Docker Compose containers, each with their own docker-compose.yml file (but sharing the same reverse proxy and PostgreSQL database!) However with NixOS I want all of them to run “bare-metal” on the system, where I can declaratively update them at will and not through a hacked-up docker-compose wrapper.
• The configuration process should be done remotely and preferrably automated. Right now my deploy tool of choice is deploy-rs, which I have chosen for its native Nix Flakes support and seemingly careful deployment process. Also, the project is used internally by Serokell, who is also basing their business off of the growth of Nix ecosystem; which means, this project should be maintained well for the foreseeable future! However I have a small gripe that it requires evaluating the Nix configuration of the remote machine on the local machine, which I cannot do from my MacBook because of different environment (aarch64-darwin vs x86_64-linux).

And... that should be good for now! I am still in the process of setting things up. Expect follow up posts in the future!

You can find my entire configuration tree on nix-home (which will be public soon, I promise...!)

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.

1. What is Blame Calculus and what is it for?

Blame calculus is an extension of a mixed-typed lambda calculus (i.e. containing both typed terms and untyped terms working on the catch-all type Dyn).

The purpose is to create a language where:

• Both untyped terms and typed terms co-exist, and typed terms are well-typed.
• There exists a decidable well-form check, and a semi-decidable well-typedness check.
• All well-typed terms (both typed and untyped) have a single type.

Additions to mixed-typed calculus

It features the following extensions to the type system:

• Refinement types: $\text{Nat} = {x : \text{Int} \mid x \ge 0}$, with runtime casting.
• A fully dynamic type Dyn, with compile-time upcasting and runtime downcasting.

It features the following extensions to the expression list:

• Casting operation: $\left\langle S\Leftarrow T\right\rangle ^{p} s$ is a cast from $s: T$ to $S$ (when $S \sim T$ – $S$ is compatible to $T$) , either
  • succeeding returning $s: S$, or
  • failing, returning $\Uparrow p$. We call this blaming on $p$.
• An internal transformation expression: $t \triangleright^p s_B$ where $t: \text{Bool}$, either
  • succeeding with $s: {B \mid t}$ when $t = \text{True}$, or
  • failing with $\Uparrow p$ otherwise.

A blame on $p$ can either be

• positive, where the cast fails due to the inner expression having an incompatible type with the destination type.

• negative, where the cast fails due to the surrounding context failing to comply with the destination type.

  • This is possible only from the delayed casting behavior of Blame Calculus:

\[ (\left\langle S \rightarrow T \Leftarrow S' \rightarrow T'\right\rangle ^p f)(v : S) \longrightarrow \left\langle T \Leftarrow T'\right\rangle ^p\left(f \left(\left\langle S' \Leftarrow S\right\rangle ^{\overline{p}}v\right)\right) \]

(notice the flip from $p$ to $\overline p$ on the cast of $v$)

Subtyping in Blame Calculus

Instead of the standard subtyping relation, which is undecidable in Blame Calculus (due to refinement types), it opts to an equally powerful system called positive (safe casts without positive blames) (denoted as $S <:^+ T$), negative ($S <:^– T$) and naive ($S <:_n T$) (which means $S <:^+ T$ and $T <:^– S$).

Unlike standard subtyping which is contravariant on the argument and covariant on the return type, naive subtyping is covariant on both sides.

Well-formednes

Two additional syntax extensions are made in order to mix typed and untyped expressions:

• $\lfloor M \rfloor$ casts the typed expression $M$ into an untyped expression. This is well-formed if and only if $M : \text{Dyn}$ (so a cast is most likely to happen somewhere).
• $\lceil M \rceil$ casts the untyped expression $M$ into a typed expression returning $\text{Dyn}$. This is well-formed if and only if
  • all free variables in it has type $\text{Dyn}$, and
  • all of its subterms have type $\text{Dyn}$.

2. Remarks

The central result of the paper, the Blame Theorem, states that:

Let $t$ be a well-typed term with a subterm $\left\langle T \Leftarrow S\right\rangle ^p s$ containing the only occurrences of $p$ in $t$. Then: – If $S <:^+ T$ then $t \not\longrightarrow^* \Uparrow p$. – If $S <:^– T$ then $t \not\longrightarrow^* \Uparrow \overline p$. – If $S <: T$ then $t$ will not blame on either $p$ nor $\overline p$.

In other words, from the decidable positive/negative subtyping relations, we can safely deduce which casts will not create a positive or negative blame.

This solidifies the intuition of upcasting/downcasting in the simple OOP sense, and allows us to extend this blame calculus with more structures, as long as the subtyping relations are still decidable.

3. Semantics

Please refer to the paper.

#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.

Let's make a Sticky card header!

In a moment I had a bright idea of keeping that Problems header on top of the card, inside the view while it is being scrolled.

This made sense: the navigation bar is right to the right (!) of the header, so it should be accessible from any scrolling. OK, so how about making it sticky?

Here's the basic layout of the page:

body:
	nav#topBar.sticky.top-0.h-14:
		... # the basic top bar
	main.mt-14.relative:
		nav#sideNav.fixed: The side navigations
		content:
			# The actual body
			card:
				card-title.sticky.top-0

Now as some of you might have already figured out, this layout actually does not provide what we want at all.

To see why, let's look at the description of position: sticky on MDN:

The element is positioned according to the normal flow of the document, and then offset relative to its nearest scrolling ancestor and containing block (nearest block-level ancestor), including table-related elements, based on the values of top, right, bottom, and left. The offset does not affect the position of any other elements.

Note that the offset is relative to the “nearest scrolling ancestor”. What is the nearest scrolling ancestor? It's basically anything that gives a scrolling bar. At the base level, it's the body element itself, when its height exceeds the screen (this is why the top bar sticks to the top).

So what we've done here is just sticking the card header to under the top bar. Not what we wanted.

We want to make a “scrolling ancestor” out of the main element, since it's what we want the card header to stick to. OK, let's do it. Note that the simplest way to make something a “scrolling ancestor” is just to stick an overflow value to it:

- main.mt-14.relative:
+ main.mt-14.relative.overflow-auto:

Is it working yet?

Why wouldn't you scroll?

Unfortunately we've come closer, but not yet done. Now that we've locked the card header to the top of main, we've actually made the behavior worse: the header now scrolls away with the main element.

Why is this happening? Note that, when we scroll the page, it's not the main element that was scrolling: it's actually body. This does not interact with the logic of sticky, so we are just scrolling over the element now.

To fix this, we will need to completely move the scrolling from body to main. This can be done by limiting the height of main:

- main.mt-14.relative.overflow-auto:
+ main.mt-14.relative.overflow-auto.max-h-screen

Is it working yet?

🎉