Categories
I’ve wanted to write an informal (but technical!) post 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.
More …
Overview
Work |
Summary |
Nakano |
STLC + recursive types + guarded types |
Birkdeal, Møgelberg, Schwinghammer, Stovring |
dependent types + recursive types + guarded types |
Atkey and McBride |
STLC + recursive types + guarded types + clocks |
Birkedal and Møgelberg |
dependent types + guarded types |
Møgelberg |
dependent types + guarded types + clocks |
GDTT |
dependent types + guarded types + clocks + delayed substitution |
CloTT |
dependent types + guarded types + ticks + clocks |
GCTT |
cubical type theory + guarded types + delayed substitution |
TCTT |
cubical type theory + guarded types + ticks |
CCTT |
cubical type theory + guarded types + ticks + clocks |
More …
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 browsers 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.)
More …
This was originally posted on cohost.
On the Market–Frankford trains of SEPTA in Philadelphia,
the designation signs indicating the line and the next stop
are very simple 18-panel 3×5-segment displays.
More …
More …
Part 1: U+237C ⍼ RIGHT ANGLE WITH DOWNWARDS ZIGZAG ARROW
This is part 2.
Part 3: Monotype Mathematical Sorts
Part 4: U+237C ⍼ is (also) S9576 ⍼
Many thanks to Barbara Beeton, James David Mason, Anders Berglund, David Bolton, Andy Whyte,
Claire Welford-Elkin, and Bob Richardson.
More …
This was originally a two-part post on cohost.
One thing that bothers me about bopomofo is that words ending in ㄛ get an extra vowel ㄨ
(essentially just /w/) in the middle sometimes when spoken but it’s never written down.
More …
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 …
This was originally
two
posts
on cohost.
More …
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 …