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.)
PL theorist, Category practitioner