⟨ortho|normal⟩

Categories

🙚 Computer Touching
🙚 Miscellany
🙚 Outside
🙚 Type Theory
🙚 Unicode

What's in a GIF?

This was originally a multi-part post on cohost.

I wanted to inspect the structure of an animated GIF, so I created a 1 px × 1 px monochrome animation that switches from white to black every 1024 milliseconds in GNU IMP, exported it as an animated GIF with disposal method “combine”, and hexdumped it. Here’s the GIF below, at the center of this 1rem box so you can see it.

More …

Ice Cream Shops in Philadelphia

When I arrived in Philadelphia, I started a Tweet thread of ice cream shops that are or aren’t as good as Rain or Shine back in Vancouver, which was the ice cream place I frequented most often since they have a location on the UBC campus. (I don’t have a thread or a list for ice cream shops in Vancouver, but you really can’t go wrong with Rain or Shine or with Earnest.)

Here I collect a list of the shops that are as good as Rain or Shine, ordered from west to east. Prices are for the smallest (non-kid’s) scoop in a cup, including 8% tax, excluding tip.

More …

LaTeX for Jekyll from GitHub Pages to GitLab Pages

About a year ago I posted about using K A T E X in a Jekyll site for GitHub Pages. This had been an unsatisfying solution to me, since GH Pages restricts Jekyll plugins to their allowlist, meaning that if I didn’t want to manually add precompiled HTML pages, LaTeX rendering would have to be done client-side using JavaScript. Furthermore, I found out that kramdown, the Markdown compiler that GH Pages uses, has built-in support for KaTeX without needing to explicitly include additional Liquid tags, but GH Pages, too, has overridden configurations needed to enable using KaTeX as well!

More …

U+237C ⍼ RIGHT ANGLE WITH DOWNWARDS ZIGZAG ARROW

For updates on the hunt for ⍼, see the new post.

Known as right angle with downwards zigzag arrow, angle with down zig-zag arrow, \rangledownzigzagarrow, and ⍼, no one knows what ⍼ is meant to represent or where it originated from. Section 22.7 Technical Symbols from the Unicode Standard on the Miscellaneous Technical block doesn’t say anything about it.

More …

U+23BE..U+23CC DENTISTRY NOTATION SYMBOLS

The Unicode Standard has its fair share of mysterious and sometimes unexplained characters. The story of the Farsi symbol (U+262B ☫ farsi symbol) is one of the more well-known ones. Many blocks, especially the “miscellaneous” blocks, have smatterings of rather arbitrary character sets grouped together only by history. One such block is Miscellaneous Technical, which contains completely unrelated groups of characters, including keyboard symbols, APL symbols, electrotechnical symbols, UI symbols, drafting symbols, and of particular interest in this blog post, dentistry notation symbols. Here they are, all 15 of them:

⎾⎿⏀⏁⏂⏃⏄⏅⏆⏇⏈⏉⏊⏋⏌

The first two and last two are part of Palmer notation for denoting human teeth by their position. What are the rest for?

More …

An Analysis of An Analysis of Girard's Paradox

While it’s rather difficult to accidentally prove an inconsistency in a well-meaning type theory that isn’t obviously inconsistent (have you ever unintentionally proven that a type corresponding to an ordinal is strictly larger than itself? I didn’t think so), it feels like it’s comparatively easy to add rather innocent features to your type theory that will suddenly make it inconsistent. And there are so many of them! And sometimes it’s the interaction among the features rather than the features themselves that produce inconsistencies.

More …

It's not all it's cracked up to be

Friday, 22 October 2021, 10:30 am. Cold, rainy, wet. From inside Joyce–Collingwood station I spotted the R4, just as it was closing its back doors. My first mistake was hope: The front door was not yet closed. My second mistake was hubris: I will make it to the bus if I run. And so I ran, but my normally-grippy sneakers slipped on the sidewalk slick with rainwater, and I ended up landing hard on my ass right in front of the bus driver.

It was a miracle I ended up mostly physically unscathed. I instinctively shot out my arms underneath me and I could have broken a wrist or two. I could’ve landed on my tailbone wrong and broken that too. But it seemed the only damage was a light bruise on my sacrum (had to look up the word for that) and to my ego. Not even a scratch on my palms! Then I sat down, took out my laptop, opened it, and discovered the large crack from the bottom left corner, reaching longingly to conquer the entirety of the screen.

More …

How to Use Sized Types?
Let Me Count the Ways

This post is inspired by this thread from the Agda mailing list.

Because Agda treats Size like a first-class type, there’s quite a bit of freedom in how you get to use it. This makes it a bit unclear where you should start: should Size be a parameter or an index in your type? What sizes should the constructors’ recursive arguments’ and return types have? Here are two options that are usually used (and one that doesn’t work.) The recommended one is using inflationary sized types and Size<.

More …