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

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

Show thread

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

Show thread

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

No... I don't dare
I don't know enough about anything to even joke about it
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

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

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

Show older
types.pl

A Mastodon instance for users who like the study of programming languages, formal semantics, types, or linguistics.