cross-posted from: https://toast.ooo/post/14722634
type theory meme
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
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.
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.
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"
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.
I think they said programming was math
I'm really good at math
everything hits the tokenizer at some point 💀 which is where all data meets their maker.
char[]? (characters stringed together in a sequence)everything loses detail after the tokenizer.
Behold, a man! - ChatGPT
a wonderful picture? u mean a list of colors and a columns count?
Isn't that all digital photography anyway?
ye that was kinda the point i was trynna to make
what up with that chatbot?
i have found my people. there are dozens of us!
Community Rules
You must post before you leave
Be nice. Assume others have good intent (within reason).
Block or ignore posts, comments, and users that irritate you in some way rather than engaging. Report if they are actually breaking community rules.
Use content warnings and/or mark as NSFW when appropriate. Most posts with content warnings likely need to be marked NSFW.
Most 196 posts are memes, shitposts, cute images, or even just recent things that happened, etc. There is no real theme, but try to avoid posts that are very inflammatory, offensive, very low quality, or very "off topic".
Bigotry is not allowed, this includes (but is not limited to): Homophobia, Transphobia, Racism, Sexism, Abelism, Classism, or discrimination based on things like Ethnicity, Nationality, Language, or Religion.
Avoid shilling for corporations, posting advertisements, or promoting exploitation of workers.
Proselytization, support, or defense of authoritarianism is not welcome. This includes but is not limited to: imperialism, nationalism, genocide denial, ethnic or racial supremacy, fascism, Nazism, Marxism-Leninism, Maoism, etc.
Avoid AI generated content.
Avoid misinformation.
Avoid incomprehensible posts.
No threats or personal attacks.
No spam.
Moderator Guidelines