Grammars are types.

Regular grammars are types you can define with base types (the characters of the alphabet), 0, +, nullary and binary separating conjunction (i.e. epsilon and sequence) and a list type (kleene star)

Context free grammars are what you get when you add a general fixed point.

Do you get context sensitive by adding a form of dependent type?

typez rool 

Untyped lambda calculus is so dumb. Types make so many things easier to understand.

Y combinator is the proof of Lawvere's fixed point theorem.

Church encodings are representations of initial algebras of functors. Predecessor of church numerals is Lambek's lemma. There's a whole section of wiki explaining predecessor of church numerals without any of that. Such a waste of brain energy!

Formal Grammars 

I got so fed up with the dragon book's lack of actual theory I came up with a category theoretic formulation of formal grammars/parse trees/semantic actions:

Should I unleash a undergrad-level version of this on my compiler's students this Fall? (I do just a little parsing at the end of the semester so there's time to work it out)

4 days later I can write an actual program in my CBPV Agda edsl!

re: Cubical Agda 

Oh thank god I found the lemma I needed in the stdlib

Show thread

Cubical Agda 

Cubical Agda is fun because I can do wild stuff like define representable profunctors and functors preserving them, but then I can't figure out how to prove that the category of Sets has products because I need to construct a homotopy between functions between hSets because the way they defined unique existence is weird

Agda Tips 

When you get a brain dump from Agda "failed to solve the following constraints" it probably means you need to instantiate some implicit argument.

if this happens that argument probably shouldn't have been implicit !!!

re: HOTTEST Seminar 

I did it and immediately got a formal proof so :blobcatfingerguns:

Show thread

HOTTEST Seminar 

Is it crashing if I just go ask my Agda questions on the HOTTEST discord since that seems like the highest concentration of cubical Agda-ers online?


WTF!!!! what does any of this mean??

: {x y : Category.ob D} → isSet (Category.Hom[ D , x ] y) [ at /Users/maxsnew/code/agdasrc/cubical-cbpv/Profunctor.agda:53,58-72 ]

———— Errors ————————————————————————————————————————————————
Failed to solve the following constraints:
Category.isSetHom D
(transport (λ i₂ → Category.Hom[ D , snd x ] (snd y)) (snd x₁))
(snd y₁)
(λ _ →
transport (λ i₂ → Category.Hom[ D , snd x ] (snd y)) (snd x₁) ≡
snd y₁)
(snd ( (invIso (IsoΣPathTransportPathΣ x₁ y₁)) x₂)))
(snd ( (invIso (IsoΣPathTransportPathΣ x₁ y₁)) y₂)) i i₁
= _isSetHom_370
(transport (λ i₂ → Category.Hom[ D , snd x ] (snd y)) (snd x₁))
(snd y₁)
(λ _ →
transport (λ i₂ → Category.Hom[ D , snd x ] (snd y)) (snd x₁) ≡
snd y₁)
(snd ( (invIso (IsoΣPathTransportPathΣ x₁ y₁)) x₂)))
(snd ( (invIso (IsoΣPathTransportPathΣ x₁ y₁)) y₂)) i i₁
: Category.Hom[ D , snd x ] (snd y)
(blocked on _isSetHom_370)


Formalizing some math in Agda is a great way to come up with Yaks to shave (i.e., all the missing category theory in every lib you try)

Agda BS 

WTF is --experimental-lossy-unification and why did enabling it make type checking work lmao.

It's used in the library that made the type-checking slow so I tried it in my file and it worked lol

Oh no I changed 2 things in my agda file and now typechecking is brutally slow whyyyy

Max S. New boosted

So today I finished my reviewing load for my first NLP conference (AACL-IJCNLP). All... 3 papers. Two 8-page papers and one 4 pager, two narrow columns per page.

For OOPSLA 2018 I reviewed 18 papers at 25 pages each.

PL and SE reviewer loads are definitely too high, but I can't help but think that half of the "reviewer crisis" in ML and adjacent areas is because their review loads are absurdly low. (The default load at top NLP venues is 6 papers, a mix of long and short.)

If students had any idea how insecure I am about teaching...

Reddit post on UofM subreddit asking about how my compilers class is...

Just two comments that are both nice 🥰​


Really enjoying Jonathan Strange & Mr. Norrell

Max S. New boosted

You'd think people who formalized their results could write their papers in a less technical, more approachable style (the details are already sufficiently checked, after all). IME they tend to write super technical papers instead. What a waste.

Max S. New boosted

Hardcore math tweet: the importance of knowing lots of small facts.

Working with Todd Trimble on category theory I'm both impressed and also annoyed by how often he can prove things I merely conjecture. Annoyed at myself, that is: why can't I do it?


Show older

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