Max S. New @maxsnew@types.pl

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?

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!

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)

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

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

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

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 !!!

I did it and immediately got a formal proof so ​

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??

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

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)

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

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

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