#gay in the soft effeminate limp-wristed sense

[anomalocariscanadensis]

super cool in-progress programming language: DCS, a functional programming language with a totality checker but not dependent types (unlike the proof assistants that usually have totality checkers). the idea is to allow divergence via a Div effect monad (cf Haskell's IO) while having the bulk of the language guaranteed to terminate. one of the big selling points is that the totality checker works for divide-and-conquer strategies, which Coq etc generally don't.

it can do this because it's based on some very complex type-level machinery where recursive functions are actually (i hope i'm using these words correctly) Mendler-inductive functor algebras. totality checkers require that arguments to recursive calls be smaller than the original argument, but normally enforce that purely based on the syntax of constructors which means they can't go through the function calls required for divide and conquer splits. here, the idea is whenever there would be recursion, it instead uses an opaque type variable and an extra function parameter to enforce that the call can only be to something "recursable", and takes a fixed point so that it ends up back at the original recursive type. (i might try and write more about these if anyone is interested, or to figure out if i actually understand it or if i'm just nodding my head along.)

i don't know if it's possible to pour enough syntactic sugar onto that concept to make it actually usable as a language. but the examples of programs in the language are way more readable than the version displayed in the paper, so it honestly might be. the list file in the stdlib has both quicksort and mergesort, and if you look past the silly decision to use greek letters instead of keywords and the limited pattern-matching it doesn't look that far off a normal recursive function.

my biggest question, though, is how it's possible to take a fixed point of the algebra without risking nontermination. if your totality checker isn't total what's the point?!

[anomalocariscanadensis]

under socialism, we will place all computer systems and education under the strict direction of a planning committee composed entirely of stringent programming language theorists, who will reorient the relationship between concrete and abstract so that physical computers are merely mechanisms to incarnate transcendent mathematical principles. a great flowering of new programming languages will take place; Haskell and Coq will be considered aeolipiles to the true programming languages yet to come; C will be retained as a historical curiosity with an esolang subculture that uses it for fun; C++ will be subject to damnatio memoriae. this state of affairs will last six years before the entire committee is executed in a Thermidorean coup led by the Scriptists, who will institute JavaScript as the only legal programming language, banning all others and purging their erstwhile allies the Delphists.

[anomalocariscanadensis]

the thing with category theory for programming is that it's mostly useless for actually writing code - it's such an overgeneral abstraction for any real use case, you're better off just learning how to program with whatever specific tools a language has and applying concrete knowledge of whatever you're trying to do. it's infinitely easier to understand the type signature of the Monad typeclass in Haskell than to understand what a monad is in the abstract. where category theory is genuinely useful, however, is programming language design/theory, because coming up with good and very general abstractions is important there: you're not constrained by what any given language already contains, and you can't apply concrete knowledge of the problem bc you need it to be applicable to all sorts of problems.

the problem, then, is that naming is hard. so if you're a pl theorist designing a language with some cool new abstractions influenced by category theory, maybe you just name them after their inspirations, instead of coming up with names that inform new users how they work in your language. and then a lot of people like your cool new abstractions so they start talking about them a lot, in the same intimidating terms you used. and then a million people who also suck at metaphors think they have to explain them in terms of burritos

[anomalocariscanadensis]

every time I understand a new concept in category theory my perspective on it shifts away from "it's just a branch of math" towards both "this is the deep sorcery in the bones of the world" and "this is so vague it could apply to everything without meaning anything" at the same time. if I'm lucky someday I'll understand enough to end up at "it's just a branch of math and here's when it's useful"

[anomalocariscanadensis]

simplest possible translation of girard's paradox (plus a couple usages) to "music" - just reading a file with the proof and mapping characters to notes, almost no effort - not even close to what i hope to achieve, but a first step at imagining what the output could be - the little recurrent fragments of melodies as names and such repeat. "forall" is a low burble that rises at the end, a particular pair of two high notes (the first slightly lower) is a lambda, etc. source text below the cut in a little toy dtlc language

let setsOf = (\ t -> (t -> *)) :: * -> *;

let U = forall (X :: *) . (setsOf (setsOf X) -> X) -> setsOf (setsOf X);

let tau = (\ t X f p -> t (\ u -> p (f ((u X) f)))) :: setsOf (setsOf U) -> U;

let sigma = (\ s -> (s U) tau) :: U -> setsOf (setsOf U);

let delta = (\ y -> Not (forall (p :: setsOf U) . sigma y p -> p (tau (sigma y)))) :: setsOf U;

let preomega = (\ p -> (forall (x :: U) . sigma x p -> p x)) :: setsOf (setsOf U);

let omega = tau preomega :: U;

let lem0 = (\ p h1 -> h1 omega (\ x -> h1 (tau (sigma x)))) :: forall (p :: setsOf U) . (forall (x :: U) . sigma x p -> p x) -> p omega;

let D = forall (p :: setsOf U) . (sigma omega p) -> p (tau (sigma omega)) :: *;

let lem2 = lem0 delta (\ x h2 h3 -> h3 delta h2 (\ p -> h3 (\ y -> p (tau (sigma y))))) :: Not D;

let lem3 = (\p -> lem0 (\ y -> p (tau (sigma y)))) :: D;

let girard = lem2 lem3 :: False;

prove quodlibet : forall (x :: *) . Fin 0 -> x; intros; exfalso; assumption; qed;

let trivial = (\ x -> quodlibet x girard) :: forall (x :: *) . x;

let plus = natElim ( \ _ -> Nat -> Nat ) -- motive ( \ n -> n ) -- case for Zero ( \ p rec n -> Succ (rec n) ); -- case for Succ

let addition_is_commutative = forall (n :: Nat) (m :: Nat) . Eq Nat (plus n m) (plus m n);

let commute = trivial addition_is_commutative :: addition_is_commutative;

let zero_equals_1 = Eq Nat 0 1;

let ze1 = trivial zero_equals_1 :: zero_equals_1;

[anomalocariscanadensis]

okay so the New Math was a total failure for obvious reasons, you can't teach kids that 3+5=5+3 "because addition is commutative", that's completely the wrong way around - addition is commutative because a+b=b+a for all a, b. it's a property you have to define and prove true of the particular relation, you can't just tell kids it's true without getting them to understand why it's true.

these days, otoh, we've made further advances in mathematics and we're setting it on better foundations. it's time to reconfigure elementary mathematical education around the forms of mathematics that underlie real modern mathematical practice and meet the demands of today's workforce: dependent type theory*.

it's quite easy to learn: 3 + 5 = 5 + 3 because we can compute plus(S(S(S(0))), S(S(S(S(S(0)))))) to be S(S(S(S(S(S(S(S(0)))))))) and likewise the other way around. unlike the New Math, kids can do this, since it's basically just counting; you can even do it with physical objects by sliding them between groups or w/e. and it reaches kids to think computationally which prepares them for life in today's computational world. and to teach kids to draw a general principle from these specific examples, we can explain that addition is commutative because

add_comm (m n : MyNat) : add m n = add n m := by induction' n with n ih · rw [zero_add] rfl rw [add, succ_add, ih]

*category theory can wait until they hit middle school, by which time they'll be familiar with more of the concrete things that categories abstract

[anomalocariscanadensis]

aestheticization of politics:

fascism

socialist realism

curry-style type systems

politicization of aesthetics:

communism

suprematism and constructivism

church-style type systems

[anomalocariscanadensis]

making my way through Category Theory for Programmers and so far it's mostly been pretty simple and/or familiar - thinking through the pure category theory bits, nodding along with the Haskell examples, and skipping the C++. i'd had trouble remembering how natural transformations worked before but they're pretty simple really. anyway i just got to limits and colimits and what the fuck

[anomalocariscanadensis]

everyone in pl theory is all about "verifying" "correctness" of "software" or some shit like that. i don't care about any of that shit, i just want to find elegant ways to express things that currently have to be said in annoying and ugly ways. correctness comes as a side effect of saying what you mean instead of having to talk around the issue

[anomalocariscanadensis]

why the fuck is russell's paradox so simple and then girard's paradox is completely insane and incomprehensible. the "simplification" per hurkens is based on the universe of "functions that take a type X and map (functions that map sets of sets of X to elements of X) to sets of sets of X". and that's not even the complicated part either

[anomalocariscanadensis]

koka seems super cool on a theoretical level but there's something really offputting about the syntax to me. like they dumped a gallon of syntactic sugar onto lambda calculus to make it look mostly like python (not a bad goal) but it feels like mentally modeling a given piece of code in more detail than pseudocode would take five layers of unwrapping it out into functions. the "trailing lambda" thing in particular seems insane to me. maybe in practice it's actually fine and you can just write whatever and have it work with effects?

[anomalocariscanadensis]

i love that delany is into category theory, at least enough to name drop it. part of what really struck me with trouble on triton was the similarity between the "customized metalogics" the protagonist creates for a living and my interest in pl theory. category theory is a really natural place to go from there. the "naming, listing, and counting theory" mentioned as a subfield of category theory seems to be made up*, and the phrase suggests an idea of category theory that's more related to the natural-language concept of categories than the mathematical one, but either way it's fun to imagine.

*(though there's an offhand mention in an ieee mailing list archive; i assume it's a delany reference but i'm really not sure what's meant by it there. assigning variable names?)

[anomalocariscanadensis]

okay i'm as guilty of this as anyone but what the hell is up with all the double entendres in pl stuff. everyone knows coq and succ and so on but the professor for the logical frameworks class i'm taking keeps talking about "ho-ass"

[anomalocariscanadensis]

trying to define the hyperoperation sequence in a programming language so experimental that its creator told me evaluating expressions would be added "in a few weeks", and the extremely powerful type/totality checker seems to be fine with everything except trying to check whether the operation level is 2 (multiplication) or >2. casing on 1 (addition) vs >1 is fine, but 2 goes too deep in the pattern matching apparently

[anomalocariscanadensis]

the simple version of the notation is basically "f[g] <=> h", where f is the function to be applied, g is the function defining the property of the result, and h is the function which relates the property on the inputs to the property on the output. it's basically a simplified way of writing "for all x0, ..., xn, g(f(x0, ..., xn)) = h(g(x0), ..., g(xn)))".

"and[not] <=> or" says "if you negate the result of an And, it's equivalent to taking an Or of the negation of the inputs", and "concat[len] <=> add" says "if you take the length of a concatenation of lists, it's the sum of the lengths of the inputs".

in its full generality you can do stuff like "f[g1 x g2 -> g3] <=> h" which I'm p sure is "g3(f(x, y)) = h(g1(x), g2(y))", the notation f[g] is syntactic sugar for f[g x g x ... x g -> g]. the functions in the brackets, which define the properties we're concerned of are called "paths" and you can add further paths which apply by function composition, f[g1][g2] <=> f[g2.g1].

i think the motivation for trying to build a whole logic from scratch around this is that it's genuinely tricky to define what, exactly, f[g] is. if the type of f is (a x a -> a) and g is a -> b, then f[g] needs to be a function of type (b x b -> b), and there's not a simple way of constructing that from f and g afaict (though it's easy to check whether f[g] matches some specific h on any given input). in fact, i suspect there shouldn't be - functions are complicated and it's undecidable in general how they'll affect any properties of their input. but the person who invented the notation is very focused on defining functions without having a specific input in mind.

[anomalocariscanadensis]

just spent a couple days talking with a math crank on reddit who has invented, as it turns out, what is actually a coherent notation for properties which are preserved by the application of functions (or related between inputs and outputs in a structured way, e.g. the length of a concatenated list is the sum of the lengths of the inputs, etc). this might actually be useful if they presented it in a comprehensible way. the problem is that they're trying to invent their own logic from scratch to ground this notation because they think it needs to be a first-order concept instead of just a notation for things that can absolutely be expressed in normal systems.

the fundamental grounding of this logic is that, to define type membership, every single object is a function which takes its type and returns itself and is undefined on everything else. so e.g. "true(bool) = true", "2(integer) = 2", and they can't take any other inputs. they claim this is not a circular definition. they think this is deeply connected to "Continental philosophy" because some other guy with two PhDs (neither in philosophy, math, or computer science) wrote a completely incoherent paper about how this is somehow connected to the "Alpha male father" and Hegel's master/slave dialectic. also there's some weird thing they call a "qubit operator" which i can't make heads or tails of but which apparently doesn't work anything like a real qubit.

they are building this system in Rust.