2.6.3 has (finally) been released! Get yours now at hackage.haskell.org/package/Ag and get a complimentary performance boost to your Agda code FOR FREE!

ANN: 2.6.3 is out today! 🐔🎉
Get yours here: hackage.haskell.org/package/Ag

Here on types, I can make a longer post, rather than a tiny thread, about the headline changes:

⏩ A ton of performance improvements, which total to a ~30% improvement over 2.6.2.2 in time spent for the standard library;

🧊 Erased Cubical Agda, which marks all marks all Cubical Agda definitions (primitives and imports from other --cubical modules) as @​0, quantity-0. The upshot is that you can reason about your programs using cubical machinery (funext!
HITs! univalence!), but nothing cubical "survives to runtime" — because unlike plain Cubical Agda, Erased Cubical can be compiled, using any of our backends (Haskell, JS) or agda2hs.

🇰 For a while during 2.6.3's development, --without-K also meant "generate support code for Cubical Agda". This was widely regarded as a bad move and made a lot of people very unhappy, so we rolled it back: Your --without-K code will no
longer suffer from cubical breakouts, and especially no longer enjoy surprise hcomps in error messages. The trade-off is that, if you want your modules to be usable from Cubical Agda (--cubical), you need to use the new
--cubical-compatible flag. Since --cubical-compatible does a ton extra (required!) internal work, modules using it will generally take longer to check, and generate larger interfaces files than, the same modules --without-K.

⚠️ Note that --cubical-compatible and --without-K should accept the exact same programs; This means you could develop against --without-K, then change to --cubical-compatible for release, for example. If you find something that one
accepts and the other rejects, please do file a bug report! On GitHub. Not on my DMs.

🪞 Reflection can now generate data types, as long as you pre-declare the names of the type and all the constructors, using the declareData and defineData primitives, together with the unquoteDecl data syntactic form. These even work for
inductive-recursive and inductive-inductive definitions!

🙏 A massive thanks to everyone who contributed to this release. Git tells me that, since the last tag, these lovely folks authored commits on the master branch:

Moisés Ackerman, Andrej Bauer, Jacques Carette, Evan Cavallo, Felix Cherubini, Jonathan Coates, Lucas Escot, Robert Estelle, Alexandre Esteves, Naïm Favier, Sean Gloumeau, Oleg Grenrus, Marcin Grzybowski, Matthias Hutzler, Tom Jack, Andre Knispel, Thomas Lamiaux, Shea Levy, Viktor Lin, Vladimir Lopatin, Sandy Maguire, James Martin, Orestis Melkonian, Fredrik Nordvall Forsberg, Andreas Nuyts, Kyle Raftogianis, Prabhakar Ragde, Christian Sattler, Peter Selinger, Artem Shinkarov, Mike Shulman, Alissa Tung, Andrea Vezzosi, Szumi Xie, Tesla Zhang, Fangyi Zhou; Favonia, lawcho, Maštarija, oskeri, person-with-a-username, Riccardo, tensorknower69, and thorimur.

Some of them are here on Fedi, but I don't want to bother them all with pings, so I won't.

🧑‍💻 Our tireless main developers (🤓❤️) also deserve a great big round of applause, not only for finishing the release, but for all they do for the language,
especially since most have real jobs, too!

Andreas Abel, Guillaume Allais, Nils Anders Danielsson, Liang-Ting Chen, Jesper Cockx, Matthew Daggitt, Ulf Norell, and Andrés Sicard-Ramírez.

If you want to get involved, please reach out! We always welcome pull requests and issue reports, be them to Agda itself, the Emacs mode, both their documentations, the standard, cubical, and categories libraries. We promise nobody will get
bitten for submitting a pull request 🙂

Sometimes it type checks. And then I’m reminded that I actually have to write some terms.

The January 2023 release of Functional Programming in Lean is now out! This release adds a chapter on monad transformers and some of the fancier features of do-notation in Lean.

leanprover.github.io/functiona

The Craft of Emacs: a guide to Emacs Lisp at craft-of-emacs.kebab-ca.se/

It's written in Racket with Pollen (using Emacs, of course!) and contains interactive, accessible code snippets.

levels of overengineering required to publish mathematics on the web...

  1. making your own static site generator
  2. rewriting your programming language's HTML backend

---------- barrier of insanity ---------

  1. making your own font

  2. forking someone else's text macro implementation

  3. reimplementing TeX following “Tex The Program” ← you are here

@arclight
Excel is not a spreadsheet. Excel is a full-featured virtual machine running a smalltalk-inspired REPL whose display layer happens to resemble a spreadsheet.

Something like a third of the world’s money goes through Excel every single day, and the reason you don’t think Excel is a Real Programming Language is because if we admitted that, we’d have to admit that most of the most important software in the world was written by underpaid women in pink collar jobs, and we can’t have that.

Isn’t it kind of absurd that professors do major event planning? Like what part of our training or skill set suggests we would be good at this. #academicchatter

@comex I have this idea that compilers represent data incorrectly for modern platforms. Currently we have a vast ocean of tiny nodes full of pointers, and we just follow pointers all day. what we need is regular, tabular internal representations that we can throw onto tensor cores

One of my professors during PhD used to say “You can drive a truck through the holes in any given paper. So you look for what you *can* learn instead.” And being the smartass grad students we used to think driving that truck was fun. After so many years, I now appreciate her wisdom more than ever. All scholarly work has limitations but it’s refreshing when people critically evaluate what’s the actual value of the research. It's about humility, honesty, rigorous intellectual work.

Listening to the Type Theory Forall podcast with Kevin Buzzard (@xenaproject). Really interesting view on how theorem provers are viewed in mathematics and where formal mathematics is heading. It's making me think about what the Agda community could learn from this. Strongly recommended you give it a listen!

typetheoryforall.com/2023/01/1

First post here. I defended my thesis last Friday. You might want to check it out: andraskovacs.github.io/pdfs/ph

Now that my thesis is submitted to the external, I'm trying to learn category theory, again.

I'm only really interested in categorical logic/models of type theory (LCCCs, CwF) plus enough to understand the things @pigworker and @gallais talk about in the Scope and Type Safe Universes paper.

Current plan is to start with Algebra Chapter 0 and Topology via Logic, but neither of those really get into model theory.

So, what's the next step after this?

The world is moving too fast I'm slowing it down. Slow Fourier Transform

Type-Theory as a Language Workbench (EVCS 2023) 

@gallais, @edwinb, and I received the word 'unconditionalised' yesterday.

Our paper, submitted to Eelco Visser Commemorative Symposium was fully accepted.

Sad, but happy.

A link to the github (containing source + paper) is available:

github.com/jfdm/velo-lang

ArXiV version coming soon.
DOI'd artifact is doi.org/10.5281/zenodo.7573031

In tribute to Lawvere, here is one of his ideas that is simple enough to explain in one post.
The original paper is "Diagonal arguments and cartesian closed categories" (tac.mta.ca/tac/reprints/articl)

Lawvere's fixed point theorem is the positive constructive content of many diagonalization arguments.
Here I'll show how it unifies Cantor's theorem that there's no surjection from a set to its powerset and the construction of the Y combinator.

Lawvere's fixed point theorem in type theory:
If r : X -> (X -> D) is surjective (forall f: X -> D. exists x. r x = f), then for every function h : D -> D there exists d : D. a fixed point of h , i.e., h d = d.

Proof:
Given h : D -> D, by surjectivity there exists l:X such that r l = λ x. h(r x x).
Then r l l is a fixed point of h:
r l l = (λ x. h(r x x)) l = h (r l l)

Corollary: Cantor's theorem. There is no surjection X -> (X -> Prop).
Proof:
If there were, then every h : Prop -> Prop would have a fixed point, but not : Prop -> Prop does not have a fixed point (exercise).

If we strengthen the hypothesis we can get something which makes sense purely in the equational theory of the lambda calculus (i.e., no existential quantifiers) and therefore interpretable in all Cartesian Closed Categories.

Variant of Lawvere's fixed point theorem in STLC:
if r : X -> (X -> D) is a retract of s : (X -> D) -> X (i.e., (λ x. r(s(x))) = (λ x. x)), then we can construct a fixed point combinator Y : (D -> D) -> D, i.e., Y = λ h. h(Y h).

Note that in the presence of the axiom of choice, this variant is equivalent to the previous, but the most interesting applications are in settings without choice.

Proof:
Y = λ h. r (s (λ x. h(r x x))) (s (λ x. h(r x x)))
Here s (λ x. h(r x x)) is the l in the previous proof, where our strengthened hypothesis gives us a choice of element rather than its mere existence.
Then
Y
= λ h. Y h
= λ h. r (s (λ x. h(r x x))) (s (λ x. h(r x x)))
= λ h. (λ x. h(r x x)) (s (λ x. h(r x x)))
= λ h. h(r (s (λ x. h(r x x))) (s (λ x. h(r x x)))))
= λ h. h(Y h)

Which is the Y combinator in STLC, which more typically is constructed using a recursive type X =~ (X -> D) with r, s the isomorphism, or in untyped lambda calculus which is equivalent to having a single type D where if only β is assumed then D is a retract of (D -> D) and with η then D is isomorphic to (D -> D).

Related expository material:
- arxiv.org/abs/math/0305282
- math.andrej.com/2007/04/08/on-
- cs.bham.ac.uk/~mhe/agda-new/La

RIP to Bill Lawvere, right as I'm teaching my categorical logic/type theory class, a field he invented.

Excited that "Is sized typing for Coq practical?", @ionchy's work, with Yufeng Li and me, has finally appeared in JFP:
doi.org/10.1017/S0956796822000

In this work, we extended some past work on sized typing for CIC to Coq, extend Coq with sized typing with complete size inference, prove some stuff about size inference, study a set theoretic model, and analyze the performance of the implementation (which is bad).

You can find @ionchy's original summary on the bird site: twitter.com/ionathanch/status/

Show older
types.pl

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