We did it

I need a PL thesaurus specifically for all the terms that Conor McBride has coined

Today's out-of-context PL phrase is:

I went looking for inductive types and W types and I found myself facing category theory. It really is always all the time

Induction nonsense

Ok this is a screenshot of this paper (end of p. 3) and it's the typing rule for the eliminator famInd and its reduction rule
The indices of the recursive arguments \vec{v} are \vec{r}_i for each v_i
I don't see \vec{r}_i itself on the LHS of the reduction rule so I think you really need typed reduction to reduce the eliminator

re: t y p e s

I have it... the eliminator... at last...
But not for nested inductive types. I honestly don't know how to do that one and it seems like no one talks about them

I'm going back to bed I swear

Me: I don't think PL is really as cryptic as category theory
PL:

No... I don't dare
I can't do it

omfg the BOLDNESS
I've never seen things being left as an exercise to the reader in a PAPER

(Definitional Proof Irrelevance without K, Gilbert et al.)

Please stop naming things with the acronym ML, I'm already plenty confused with Meta Language (the language) and metalanguage (the concept) and Marxism–Leninisim (the ideology) and machine learning (the field) and markup language (the category of languages) and

You don't say

tiletiletiletile

I finally got around to installing a DrRacket directory browsing plugin and I regret to say that it ugly

this is me. nice

Throwback to when I was learning how to use slideshow on Racket and I started to make a presentation about pineapple on pizza but then ran out of shit to bull