Reed Mullanix

When looked at the right way, init systems like systemd, launchd, etc are build systems; instead of building a piece of software, they build a working environment. This is more than just a vague metaphor: most reasonable init systems will have a way of expressing dependencies, expected outputs, etc.

What *is* legitimately different is that init systems keep running after the artifact is built, and have rules that dynamically fire; EG: a rule that fires when network configurations change, a rule that fires every hour, etc. In a sense, this means that init systems are build systems that are always in watch mode, and support dynamic rules.

It would be interesting to transfer these rules across our analogy, and experiment with a build-style system that supports dynamic watch rules. Most fancy build systems already support an ad-hoc form of this via hot-reloading, but a principled version seems very useful!

https://gist.github.com/TOTBWF/b3dbe1fb1b62018fe40870163a72e532

Basic problem is that positivity checking mutual definitions can be tricked by (a) preventing it from seeing the entirety of a Pi type and (b) adding a layer of indirection

Credit to @ncf@types.pl for the idea that things like (tt : ⊤) → ⊤-rec tt (Set → Set) could fool the positivity checker.

One mistake that almost every programming language seems to make is conflating files with compilation units with namespaces

Haskell association lists have to be the *worst* possible data structure imaginable...

@stschaef @amy @ncf

There are two things blocking Kan ops for Typeω. The first is a technical problem: for small hcomps, we can use universe polymorphism to have a single primitive primHComp : ∀ {ℓ} {A : Type ℓ} {φ : I} (u : ∀ i → Partial φ A) (a : A) → A. This trick does not work for Typeωᵢ. Possible solutions are:

(a) have universe polymorphism in Typeωᵢ which just kicks the problem up a dimension or (b) have users bind primitives for primHCompω₀, primHCompω₁, ...

The second blocker is a somewhat sillier one: the 1lab actually relies on the fact that Typeω does not have Kan operations for performance reasons! In particular, we put some indexed inductives in Typeω to avoid generating the extra cubical code. This is definitely a capital-H Hack, but it does make a huge difference for performance.

We have dropped support for rewrite rules (see https://codeberg.org/1lab/mikan/pulls/68) They are a really cool feature for transforming your proof assistant into another type theory, but they add a large amount of complexity and overhead.

Well this is pretty damning...

https://damrnelson.github.io/github-historical-uptime/