this post was submitted on 25 Jun 2026
63 points (92.0% liked)

Programmer Humor

31972 readers
853 users here now

Welcome to Programmer Humor!

This is a place where you can post jokes, memes, humor, etc. related to programming!

For sharing awful code theres also Programming Horror.

Rules

founded 3 years ago
MODERATORS
Feyter@programming.dev
anzo@programming.dev
BurningTurtle@programming.dev
pylapp@programming.dev
63
type theory meme (leminal.space)
submitted 22 hours ago by cm0002@toast.ooo to c/programmer_humor@programming.dev
7 comments fedilink hide all child comments
 
you are viewing a single comment's thread
view the rest of the comments
[–] davidgro@lemmy.world 3 points 15 hours ago (2 children)

Would you be up for explaining it please?

[–] renzhexiangjiao@piefed.blahaj.zone 9 points 13 hours ago

Γ is typically used to denote the context, or the type environment for an expression. It is a mapping from variables to types. for example we could have

Γ = x:A, y:B, z:C

then

Γ |- y: B

is a typing judgment. Means "In the context of Γ, y has type B."

Type derivation is a process where you start with an expression and an empty context and then figure out what the type of that expression is by building it up from scratch using typing rules. It's what compilers do to figure out whether your program is correct.