grammar

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: https://github.com/maxsnew/grammars-and-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)

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

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

_isSetHom_370

: {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

(λ _ →

transport (λ i₂ → Category.Hom[ D , snd x ] (snd y)) (snd x₁) ≡

snd y₁)

(snd (Iso.fun (invIso (IsoΣPathTransportPathΣ x₁ y₁)) x₂)))

(snd (Iso.fun (invIso (IsoΣPathTransportPathΣ x₁ y₁)) y₂)) i i₁

= _isSetHom_370

(transport (λ i₂ → Category.Hom[ D , snd x ] (snd y)) (snd x₁))

(snd y₁)

(transport

(λ _ →

transport (λ i₂ → Category.Hom[ D , snd x ] (snd y)) (snd x₁) ≡

snd y₁)

(snd (Iso.fun (invIso (IsoΣPathTransportPathΣ x₁ y₁)) x₂)))

(snd (Iso.fun (invIso (IsoΣPathTransportPathΣ x₁ y₁)) y₂)) i i₁

: Category.Hom[ D , snd x ] (snd y)

(blocked on _isSetHom_370)

re: Agda BS

Ok it's not so scary: https://agda.readthedocs.io/en/v2.6.2.2/language/lossy-unification.html

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.)

- website
- http://maxsnew.com/

- pronouns
- he/him or they/them

PL theorist, Category practitioner

Joined Apr 2022