This morning's ponder: maybe 'finite' should not be something that is imposed (for example: when considering arities) but rather is something that we should let emerge naturally (such as when looking at free constructions).

Brought to you by formalizing lots of stuff in Agda, where the assumption 'finite' is seldom needed.

A further hint that 'finite' is not a good property: constructively, there are many different non-equivalent ways of defining something that means 'finite' classically.

~~Category Theory as Generalized Logic (Limits)~~

As discussed previously (types.pl/@maxsnew/109912101112), a presheaf can be viewed as a categorified notion of a predicate, and universal properties correspond to unique existence of a solution. This also means we can take any definition in category theory and get back a (possibly trivial) definition in ordinary logic.

For instance, take limits. A diagram in C is a functor D : I -> C for some "shape" category I. A cone from D to an object c \in C is a natural transformation from the konstant functor (K(c) : I -> C) to D. This definition gives us a presheaf (cone D) : C^op -> Set for each D. More generally we can think of it as a profunctor covariant in (I -> C) and contravariant in C. A limit of a diagram D is an object with the data that it represents cone D.

What does this mean when we "de-categorify" to sets? Well, a D-cone over c is a family of morphisms from c to D i for each i \in I that commutes with all of the D f : D i -> D j. When de-categorifying to sets, functors become functions and morphisms become equalities. So a diagram is just a function (D : I -> X) and a D-cone is an element x \in X such that for every i \in I. x = D i. So we get that a cone is an element that is equal to every element in the codomain of the diagram D. D has a limit if there is a *unique* element of X that is equal to every element in the codomain of D. So if I is non-empty, a limit exists if and only if D is a constant function and the limiting element is the unique element in the codomain. If D is empty, a limit exists if and only if X is a singleton (maybe that's the right definition of when a function 0 -> X is constant?).

Exercise: from this de-categorification perspective, what is the analog of the theorem that Right adjoints preserve limits?

Another good one:

> Agda uses call-by-need technique for evaluation. This means that the expressions are not
evaluated until they are needed. Agda follows strict evaluation, the arguments of the function is
evaluated before evaluating the function itself.

Show thread

You know something's fishy when you read

It [Agda] also helps programmers to automatically check their
work using a sound type system and a rich library of proof tactics.

Show thread

Anyone know how I'd be able to tell if someone was written by GPT-3/4 ? I'm reviewing something that uses a lot of the right words, is written in cogent English (by someone whose English is weak), but is ridiculously false every second sentence or so.

It reads like it's been back-patched to include references to real things - but the real things don't make the false claims attributed to it.

Picard engineering tip: Maintenance of existing systems is just as important as building new capabilities.

So I got into a conversation recently (on here, but I'll keep this thread separate) where I failed to express myself clearly. I won't reprise that here, but instead talk about something that was definitely part of my motivation in trying to engage in that conversation.

Wow, quite the prelude!

I was doing some work on operations on theories and someone pointed out "Oh, that's just a pushout." The problem?
1. they were 100% correct, and
2. that was completely useless!
Why?
Because it was even easier to show that there could be no canonical pushout. In other words, to write down the pushout, you needed to make some choices, and these choices were necessarily dependent on the input. So?

The issue was the result of the operation was supposed to be understandable by humans (aka machine generated names are awful) and compositional. In fact, one of the requirements of the framework was that you shouldn't be able to tell the 'path' that was used to create a certain theory -- because one can prove that it is path independent. And, in fact, the pushouts involved did have the right commutativity and associativity properties, so this isn't a silly thing to be asking.

In other words, the mathematics (correctly!) said the choices didn't matter, and very basic UI principles said (correctly!!) that the choices mattered a lot.

I've seen some people resolve this by creating complex name-generation algorithms (which I guess that you're supposed to run in your head to predict how to compose things?) Instead, I solved it by always requiring the user to provide a disambiguation means whenever their pushout had no canonical answer.

[Oh, I read the other thread, and this is completely different, some onlooker might think. Of course it is - I said so at the start. This isn't an analogy story, it's a what-motivated-me story!]

This should be in the literature somewhere, but I'm having a really hard time finding it:

When are two morphisms of polynomials equivalent? Another phrasing would be, when are two morphisms of containers equivalent? I think I could ask again using (lawless) lenses a la @julesh and it would again be essentially the same question.

And, of course I don't want some kind of strict equality!! I really do mean equivalence.

A category with K objects is a square matrix C \in Set^{K x K} equipped with elementwise functions
I -> C
C^2 -> C
satisfying the monoid rules.
A presheaf is a vector P \in Set^K equipped with elementwise functions
CP -> P
satisfying monoid action rules.
A copresheaf Q is a vector Q \in Set^K with elementwise functions
Q*C -> Q* (with * the transpose)
satisfying monoid action rules.
A profunctor is similarly a matrix in Set^{K x L}.
A dagger category is a matrix C that is isomorphic to C*.

Looking for one more person: Nathan van Doorn. I'd like to give him credit for some of his work, but first I have to ask him if that's what he wants! I can't find a way to get in touch with him.

Anyone know if Tiark Rompf hangs out somewhere on Mastodon? [Does anyone know if he usually answers his emails...]

Aha, @samth I think I know why I wasn't seeing your replies. I thought I was following you, but apparently not? It looks like there are two copies of you, as far as my Mastodon is concerned!

My 'server' (i.e. types.pl) appears to censor mastodon.social. Do we know why? Are there ways that I can get around it, i.e. are there some settings that I can change so that I can see the posts that people from that server post?

What should programs actually denote? Old work in denotational semantics starts from a PL whose operational semantics may not be sane, works really hard, and finds a post-facto "explanation" for it. Very little sense of elegance seems to pervade some of that work.

It's been long enough to look the other way around: there are things that we want to actually say -- can we reverse engineer some decent PLs that actually created from scratch to say elegant things, instead of being merely designed to order computers around?

[Note that I'm not putting down early work on denotational semantics - it is often a mathematical tour de force, with rich insights! I'm merely questioning if maybe it's time to turn things around.]

Hey people: please, when you use agda--categories, don't just link to it, cite the paper! Proper academic credit is important, and citations are the way you do it. Maybe in the future, links to github repos will count as citations, but right now they don't.

I've see two recent papers on the arxiv which could be thus 'augmented'. I won't @ the authors (yet?)

Reading other people's good-but-undocumented code always nudges me towards putting even more into my own.

Unfortunately, that hasn't quite reached the level where I want to go back to old code and add lots of comments, but I can feel that that day will come!

TFW you're reading a paper posted in March 2023 that has in its introduction "My journey in this saga began in 1965, when ... as a Ph.D. student..."

Does anyone know of a non-email method to get in touch with Klaus Ostermann? He has not replied to several important emails in the last 10 days.

Here is the next feature every other language should copy:

Deriving via

This feature alone has made Haskell a lot more enjoyable for me and I miss it in other languages

Show older
types.pl

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.