Liang-Ting Chen

Not assigning a specific topic directly for intern students always makes me excited about what students are capable of and the diversity of their interests. 🤩

Two years ago, one of interns proposed a research question about the equivalence of two fractal constructions as functional programs and it later becomes a cute paper (under revision) about the classic second duality theorem in program derivation.

And today, my new intern proposes to do some recently developed math in Cubical Agda. (There is some preliminary work but not much.) I’m not sure where it will end but this is something good for students to explore but I may not consider myself in a few years.

Thanks to @qbane@g0v.social and @banacorn@g0v.social, Agda now runs in *your browser* via VS Code for the Web — tested on Safari and Chrome, on both desktop and iPad!

A pre-release is now available in the VS Code Marketplace (library management not yet supported, though). You can open a remote repository on GitHub by pressing '.' to give it a try yourself.

A proper announcement will follow somewhere after a stable release — I’m just too excited not to share this now.

This project began during AIM XXXVII in Taipei two years ago, when the WASM backend for GHC became available. Both @banacorn and @qbane — the main developer of Agda Mode for VS Code and an experienced web developer & Haskeller — are based in Taiwan and enthusiastic about the idea, and I am very fortunate to be able to support their work with my startup funding (with minimal paperwork) and feedback during development.

This project involves a number of repositories:

https://github.com/agda-web/agda-wasm-dist
https://github.com/agda/agda-language-server
https://github.com/banacorn/agda-mode-vscode

Big thank to @banacorn@g0v.social and @qbane@g0v.social again.

I have been trying to see how capable of GPT 5.5 (Business plan, $20 per month) is by implementing an experimental language server for Agda after work.

So far, it kind of works but requires closer inspection and quite an intensive interaction between the agent / the chat mode to make the spec very detailed and to fix unexpected behaviour introduced when the spec is not clear enough.

I am not sure if it counts as "vibe coding", as I still have to figure out what VS Code, LSP, and Agda's API are capable of, and test quite closely to see if everything works as expected based on *my experience*. Most of my time is spent on writing incremental specs (with the help from ChatGPT), code review, and manual testing apart from unit tests. It speeds up the process but not as much as advertised. The up side is that the burden of context switching is lower, so I can still keep with my day-time research. (The first experiment failed epically, by generating a whole bunch of shit code that appeared working at first. The current second experiment is way slower, but at least it works.)

Strictness is fragile.

Today's episode is that I need to work in the internal language we just built to build another model internally. 🤯

Attending conferences is (perhaps) healthy for your mind but (definitely) unhealthy for your body – sleep deprivation, sitting still for hours and unlimited supply of food, sweet, and snacks during each break. I found I am not that young to enjoy it without worrying about my sugar intake etc., so this time I have brought my bike to do some exercise before and after.

The side effect is that I have visited places where I couldn't with just the public transportation with the total of 150km ride in a week. (Not sure if it is enough to offset the sugar intake, though.)

I just learned that the strong J (the SProp-to-Type elimination for the strict identity type) is actually okay and it is discussed already in the paper on definitional proof-irrelevance.

I should have read the paper more carefully..

Some experience about my on-going work: It is harder to get things done easily than in a complex way.

We started with a naive construction in a stronger meta-theory, but it kept asking stronger assumptions and did not really solve our problem.

Then, we retracted to a simpler setting with a more complicated construction (to replicate the intended construction in the previous step) and another even more complicated construction. It works but the construction consists of many mysterious steps.

Finally, we observed that these intermediate steps can be simplified or eliminated by changing the statements carefully and derive a short construction with stronger properties than expected in a weaker setting.

It might be easier to get things published if we had stopped at the second step without further simplification... But, anyway, we will see.

I recently found that the term "setoid" is like domain -- there are more than one precise formulation of setoid (in various settings) and one should always check which setoid they actually talk about.

My first accepted submission that I had no expectation to be accepted or rejected. See you at CPP.

RE: @fnf@mathstodon.xyz

Very happy to have @fnf@mathstodon.xyz visiting us and we did have very productive and exciting (!?) weeks for research. 🥳

Learned recently from Simon Boulier et al.’s paper on syntactic models and subsequent papers to give a model of type theory which refutes, for example, the function extensionality. The syntactic model is fairly easy to construct and instructive. I wonder if there are classical principles, such as LEM, that can be refuted easily this way. 🤔

RE: @amoine@discuss.systems

lol

Playing with 2LTT in Agda leads me to wonder if some form of relative canonicity holds in particular that if context, types, and both sides of the outer identity are inner terms, then these term are actually judgementally equal.

I’ve been very confused by the claim that the outer identity is the internalised judgemental equality, but IIUC this hold if the outer theory is extensional. 🤔

I wish there were other implementations of 2-level type theory, not just MLTT (outer) / HoTT (inner) but rather OTT / MLTT, as it is quite hard to track down which is which... 😵

Is Agda the only implementation that supports (indexed) inductive-recursive types?

Let’s forget about the extra flexibility of the recursion part allowed in Agda.