type theory meme

submitted by
variation of the "I require context" Wojak meme; a drawing of a man with glasses and a beard pointing at a sign that says "I require context" and the Greek capital letter Gamma; he is wearing a box as a hat that says "type derivation rule hat" and a t-shirt that says "Λ the ultimate sequent calculus" (with the Greek capital letter Lambda, and "calculus" partly cut off at the bottom of the image); the hat, the shirt and the sign are all slightly green, while the man is sketched with lines on a white background
19
7
2

Log in to comment

Hot Top New Old

Comments in Programmer Humor@programming.dev

god dammit this is actually good 😭. i literally did semantics of programming languages last term too

 reply
12

Would you be up for explaining it please?

 reply
6
he/him

Γ 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.

 reply
14

Deleted by author

 reply
2
edited

What’s the easiest way to actually learn how the correspondence works? It always feels like there’s some kind of background they’re assuming I have, that my pure maths ass doesn’t.

 reply
2

Comments in 196@lemmy.blahaj.zone

Oooooohhh! That’s my field of study!

So, you know how in programming you have data types (like int, float, structs etc…) well, they are actually math.

In math, more specifically in logics, there’s these things called “judgement derivation systems”. They are basically sets of rules that tells you if you can derive a judgement, from a set of hypothetical judgement. The most notorious are sequent calculus and natural deduction. Both are used to determine if a logic formula is consequence of a set of hypothesis.

You see, one day Mr Howard wrote to Mr Curry: “I was working on a type system for lambda calculus, and I noticed it kinda look like natural deduction” and curry answered: “wow, that’s cool, I’ll tell you more, a type system for this other thing kinda looks like combinatory logics” and then they both went “could it be that every type system is actually a logic deduction system, and every logic deduction system is actually a type system?” And this is what modern type theory (and theorem provers) are based on.

Now, formal type systems are often defined as judgement systems. More specifically, they look like sequent calculus, and they use a “context” object, which is often identified with the letter gamma.

 reply
27

Not to be that person, but…

Don’t worry, it happens to the best of us.

Humour aside, I actually found it very interesting to read, despite not quite understanding it fully. I might give it a more thorough read later.

 reply
20

I think they said programming was math

 reply
10

I’m really good at math

 reply
3

I was aware of that, but I didn’t want to do a full write-up from zero knowledge to type theory…

Maybe I’ll do it later tho. Because I enjoy explaining this stuff.

Anyway, despite the comedic delivery, that comment should give a 1st year CS student all the keywords they need to research the subject. Especially the letters between Curry and Howard, which are referred to as the “Curry-Howard correspondence”

 reply
8
edited

I was joking, a bit. It’s not like you can explain all of it in one random comment.

Aghhh! I wanna get a cs degree, but I had to switch programs for r e a s o n s. Maybe I could get one after my associate’s degree.

 reply
4

For what it’s worth, you pushed me ever so closer to wanting to study for a maths degree.

 reply
1

everything hits the tokenizer at some point 💀 which is where all data meets their maker.

  • a palm tree? 🌴 oh u mean generic tree with fancy leaves? 🌳❇️
  • a chair? 🪑 oh u mean symbols arranged chair-wise?
  • a heartfelt message to your crush? 💖 oh u mean char[]? (characters stringed together in a sequence)
  • a wonderful picture? u mean a list of colors and a columns count?

everything loses detail after the tokenizer.

 reply
9

Behold, a man! - ChatGPT

a wonderful picture? u mean a list of colors and a columns count?

Isn’t that all digital photography anyway?

 reply
3

ye that was kinda the point i was trynna to make

what up with that chatbot?

 reply
2

The joke is a cross between a famous anecdote about Diogenes and the inner workings of vision-capable AI models.

Diogenes really liked to disrespect his social superiors, so when, in a lecture, Plato defined human beings as “featherless bipeds”, Diogenes plucked a chicken and presented it to him saying “Behold - Plato’s human being” (or something along those lines, the quote is slightly different in every source).

In order to “see” things from images and video, a garden variety LLM needs to integrate with another model that analyzes the picture it is given and gives a text description (source: HuggingFace). What I’m getting at is that, based on that idea of stripping things of context, ChatGPT could probably confidently tell you something in the vein of Plato taking the piss due to its inherently limited ability to see.

 reply
1

oh wowie no way someone did the reading on HUGGINGFACE!?!? wowie, never expected that link to make it to 196….

anyway: good joke, i get it now, thank u.

 reply
1

i have found my people. there are dozens of us!

 reply
3

reminds me of quantity calculus, which is when type theory meets physicists like Fourier and Maxwell and Kelvin https://en.wikipedia.org/wiki/Quantity_calculus

 reply
2
Insert image