⟨ortho|normal⟩

Categories

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

Specialty Coffee Roasters in Philadelphia

Get your beans here! This is a list of specialty coffee roasters local to Philly that do single-origin light roasts whose coffeeshops are in or close to Centre City. This list is tailored to my preferences: I make coffee with an Aeropress at home, and I enjoy getting pourover coffee when I’m out.

More …

ECIC is Inconsistent

…probably. To be clear, ECIC1 refers to Monnier and Bos’ Erasable CIC2, with erasable in the sense of erasable pure type systems (EPTS)3. I’ll argue that even with erased impredicative fields, Coquand’s paradox of trees4 is still typeable.

  1. Not to be confused with their eCIC, the erasable CIC. 

  2. Stefan Monnier; Nathaniel Bos. Is Impredicativity Implicitly Implicit? TYPES 2019. doi:10.4230/LIPIcs.TYPES.2019.9

  3. Nathan Mishra-Linger; Tim Sheard. Erasure and polymorphism in pure type systems. FOSSACS 2008. doi:10.5555/1792803.1792828

  4. Thierry Coquand. The paradox of trees in type theory. BIT 32 (1992). doi:10.1007/BF01995104

More …

Respooled Film Stocks

This was originally posted on cohost.

While looking up the various colour films my local photo shops carry, I found that a lot of them are actually respools and repackagings of other film (most Kodak), so I’ve tried to compile that information here to keep track of them all. I’m personally not looking for “experimental” colour films or films that aren’t “true colour”, so I’ve excluded a number of those here, which are mostly:

  • LomoChrome from Lomography
  • RETOCOLOR from RETO Project
  • various from KONO!
  • various from Film Photography Project
More …

Designing Stratified Type Theory

I’ve wanted to write an informal (but technical!) post1 about my current research in progress on Stratified Type Theory (StraTT), but we’ve been occupied with writing up a paper draft for submission to CPP 2024, then writing a talk for NJPLS Nov 2023, then being rejected from CPP, then I’ve just been randomly distracted for two weeks but I’m so back now.

That paper draft along with the supplementary material will have all the details, but I’ve decided that what I want to focus on in this post is all the other variations on the system we’ve tried that are either inconsistent or less expressive. This means I won’t cover a lot of motivation or examples (still a work in progress), or mention any metatheory unless where relevant; those can be found in the paper. Admittedly, these are mostly notes for myself, and I go at a pace that sort of assumes enough familiarity with the system to be able to verify well-typedness mentally, but this might be interesting to someone else too.

  1. A draft of this post was first published on Cohost. 

More …

Notes on Guarded Types

Overview

Work Summary
Nakano [0] STLC + recursive types + guarded types
Birkdeal, Møgelberg, Schwinghammer, Stovring [1] dependent types + recursive types + guarded types
Atkey and McBride [2] STLC + recursive types + guarded types + clocks
Birkedal and Møgelberg [3] dependent types + guarded types
Møgelberg [4] dependent types + guarded types + clocks
GDTT [6] dependent types + guarded types + clocks + delayed substitution
CloTT [7] dependent types + guarded types + ticks + clocks
GCTT [8] cubical type theory + guarded types + delayed substitution
TCTT [9] cubical type theory + guarded types + ticks
CCTT [10] cubical type theory + guarded types + ticks + clocks
More …

Lossless Image File Formats

This was originally a two-part post on cohost.

Recently I needed to convert a large TIFF scan of a duochrome page into something reasonable, i.e. a web-supported image format that was still lossless since it seemed a shame to ruin such a nice high-definition scan with lossy compression. In terms of lossless formats, all browsers1 support PNG, WEBP, and AVIF, while I really hope JXL support is imminent.

I therefore wanted to see which file format would perform the best in terms of file size by converting my ~183 MiB TIFF to each of them using ImageMagick. For PNG, WEBP, and JXL, there’s an effort setting: lower effort means faster compression but larger size, while higher effort means slower compression but smaller size. I used the highest three settings for these, yielding sizes from ~50 MiB to ~20 MiB. (As a treat, I’ve also converted to JPG, WEBP, AVIF, and JXL at -quality 0, i.e. lossy with the worst settings.)

  1. Except Edge doesn’t support AVIF, but who cares about Edge? 

More …

UPDATE: U+237C ⍼ ⍼

This post is a continuation of the investigation into U+237C ⍼ RIGHT ANGLE WITH DOWNWARDS ZIGZAG ARROW.
For new photos of relevant documents held at St Bride Library, see Monotype Mathematical Sorts.
Many thanks to Barbara Beeton, James David Mason, Anders Berglund, David Bolton, Andy Whyte, Claire Welford-Elkin, and Bob Richardson.

More …

Little Shops in Philadelphia

I’ve previously posted about my favourite ice cream shops in Philadelphia, but there’s a ton of other great little shops to visit. Here’s a few that I’ve really liked, sorted into two categories: used bookstores and vintage/oddities. I’ve excluded all food places, including coffeeshops, roasteries, bakeries, dessert shops, grocers, markets, food trucks, and so on, because there are just too many of them.

More …