Jacques Carette @JacquesC2@types.pl

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.

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.

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.

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.

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.

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.