frog hop - from non-linearity to linearity

I've been studying a family of programming language work I've had a hard time naming, until recently. By browsing the delightful ATTaPL, I've learned that this family of work is called "substructural types", which means "type systems which intentionally omit a structural rule from the simply typed lambda calculus" (exchange, weakening, or contraction). These restrictions essentially mean that some form of resource accounting is injected into the type system, or (in more subtle systems) a semilattice or finite automaton of valid "type-state" or "role" transitions is described. Concretely: you don't get to reuse (or fail to use, or copy, or mutate) a variable willy-nilly, only in permitted circumstances. It has a lot of direct implications in terms of designing languages which are free from concurrency problems or garbage collection, or in permitting users to describe resource-use protocols. In general, it's about "making programs typefully-aware of resources".

Most of these systems are research-y, but I'm hopeful the idea will wend its way into mainstream languages someday. Variations on the theme include imperative linear types, object typestates, role types, unique pointers, linear-typed assembly language, time regions, alias types, a couple of race-free dialects of java, and -- making abysmally clear the agonizing pace of research transfer -- an absolutely lovely typestate-checking (and garbage-collection-free) language from the early 90s called hermes, which I only recently ran across.

I also got a little MIDI cable to connect my miserable ugly synthesizer to the computer. This means I can now use seq24, which is an absolute riot, and strongly embraces my preference for intentionally limited musical instruments, which force you to make concrete decisions.