survey paper title, free to good home 

Fifty Ways to Peeve Your Prover

re: fun with finiteness 

Job done. The above universe now has the finiteness property I described.

Show thread

"Starve a fever. Shave a yak." or something.

overly intensional piggery-jokery 

It's my habit to build ordinary + and * types from

data Two : Set where `0 `1 : Set
record _><_ (S : Set)(T : S -> Set) -> Set where ...

S * T = S >< \ _ -> T
S + T = Two >< (S <01> T)

I also have a tendency to cook "types with stuff" in "carrier field" style, e.g.

record Datoid : Set1 where
Data : Set
eq? : (x y : Data) -> Decide ...

And then I can show nice closure properties like

Bit : Datoid
Data Bit = Two
_><D_ : (S : Datoid)(T : Data S -> Datoid) -> Datoid
Data (S ><D T) = Data S >< \ s -> Data (T s)
_+D_ : Datoid -> Datoid -> Datoid
S +D T = Bit ><D (S <01> T)

but I then don't get (definitionally)

Data (S +D T) = Data S + Data T

because no commuting conversion

\ b -> Data ((S <01> T) b) /= (Data S <01> Data T)

Something's gotta give... not sure what.

You've got to understand how much the politicians are into AI. They have so much in common. They're both dangerously full of shit and they aim to marginalise people who notice.

Of course, dense doorstep defaecation is standard mathematical practice.

Every discipline should interrogate its standards of practice from time to time.

Show thread

There is a school of paper-writing which amounts to doing a very dense logical shit on your reader's doorstep and then running away.

These people want to tell us they understand things. They do not want us to understand things, or if they do, they do so only as an aspiration unenacted.

Show thread

People who know me a bit often say that they can hear me when they read me. And that's nice, because I write drama, not prose, and I'm imagining the audience I'm trying to speak to. The script improves with rehearsal.

re: fun with finiteness 

My current favourite universe of finite sets extends uninformative Boolean truth
So : 2 -> Set
with actual bits
and then closes under dependent pairing.

These are wonky binary trees with leaves that are either bits or witnesses to decidable properties. Given that equality for values in these types is decidable, we definitely get a - operator, by a "but not you" construction. (There are other ways to get - but this one makes the weakening map a mere projection.)

Functions from these types may readily be tabulated: a function from 2 is a pair; a function from a pair is a curried function. In particular, this universe already admits a notion of dependent function type, with lambda and application: beta and eta laws are intensionally provable (but defo not judgmental, for fear of a Ripley).

Where am I heading? Containers with finitely many positions, represented as dependent pairs of a shape and a tabulated function from positions. They're traversable. They're also differentiable, but you'll run out of positions before you run out of fingers.

Show thread

fun with finiteness 

Suppose you have a universe of types (U, El) equipped with an operation
- : (T : U)(t : El t) -> U
such that (T - t) + 1 <=> T

We may define inductively what it is to be a Finite type in U:

T is finite if El T -> 0
T is finite if there is an example t : El T, and for any x : El T, (T - x) is finite

That's to say, you can throw away elements in any order you like, not in the order the finiteness proof likes.

I have that any such type in any such universe is isomorphic to an initial segment of the natural numbers, but I don't like initial segments of the natural nmumbers very much.

I'm now trying to establish finiteness in this sense for a universe of types which are finite but structured, wearing the wrong spectacles, the while.

overly intensional piggery-jokery 

Working in plain Agda, I don't have enough extensionality to prove that any two refutations (f g : X -> Zero) are equal. With extensionality, I could assume some x : X, then use either f x or g x to obtain a contradiction.

I'm trying to cook up a useful notion of Datoid (set with decidable equality). If I say "equality is either refutable or provable", I get handed nasty relevant refutations.

The shit hack is to say that a Datoid equips a set with a proof irrelevant notion of apartness which implies refutation of equality, and then makes any two elements apart or equal.

re: lurgy 

I don't like being simultaneously sick and on strike. Whatever I've got, the picket doesn't want. I'll stay away in solidarity.

Show thread


Seems like it's no the rona, but it's no fun. Brain is soup.

Regretfully, the petition to remove #LGBT content from the #UK curriculum has 197,100 signatures.

The counter petition asking for that content to remain, is rapidly gaining ground. It now has 78,919 signatures!

Pls sign the counter petition if able. British citizens & UK residents have the right to sign. Pls boost otherwise!

Link to official petition to UK Gov & Parliament: Do not remove LGBT content from the Relationships Education curriculum

#LGBTQ #TransRights

Which reminds me...just checking everyone knows the c++ joke.

What does c++ mean?

Increment c; return original value.

i can't believe that my shitpost about inspecting the value of the expression `c / c++` to determine what compiler you're on turned out to _actually_ expose a difference between gcc and clang

int c = 1;
int d = c / c++;

in GCC, both ints are `2`; in clang, `d` is `1`

bidirectional typing 

You have

data Dir : Set where chk syn : Dir

Now use induction-recursion to declare-and-define

data Term (G : Context)(d : Dir)(i : In d) : Set
out : forall {G d i} -> Term G d i -> Out d

for suitably chosen In and Out.

re: bidirectional typing 

As a bonus bonus, whenever you define an "indexed inductive family", try saying in what category each index is an object, such that the family extends to a functor.

Show thread
Show older

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