cross-posted from: https://toast.ooo/post/14722634

type theory meme

all 14 comments

sorted by: hot top controversial new old
[–] 27 points 2 months ago (6 children)

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.

  • source
  • hideshow 6 child comments
  • [–] 20 points 2 months ago (5 children)

    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.

  • source
  • parent
  • hideshow 5 child comments
  • [–] 8 points 2 months ago (2 children)

    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"

  • source
  • parent
  • hideshow 2 child comments
  • [–] 9 points 2 months ago (4 children)

    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.

  • source
  • hideshow 4 child comments
  • [–] 3 points 2 months ago (3 children)

    Behold, a man! - ChatGPT

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

    Isn't that all digital photography anyway?

  • source
  • parent
  • hideshow 3 child comments
  • [–] 2 points 2 months ago (2 children)

    ye that was kinda the point i was trynna to make

    what up with that chatbot?

  • source
  • parent
  • hideshow 2 child comments
  • [–] 1 point 2 months ago (1 child)

    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.

  • source
  • parent
  • hideshow 1 child comment
  • [–] 3 points 2 months ago

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

  • source
  • [–] 2 points 2 months ago

    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

  • source