89
type theory meme (leminal.space)
submitted 1 month ago by to c/programmer_humor@programming.dev
8 comments fedilink hide all child comments
 
you are viewing a single comment's thread
view the rest of the comments
[–] 12 points 1 month ago (1 child)

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

  • permalink
  • fedilink
  • source
  • hideshow 2 child comments
    •
  • [–] 6 points 1 month ago (2 children)

    Would you be up for explaining it please?

  • permalink
  • fedilink
  • source
  • parent
  • hideshow 4 child comments
    •
  • [–] 14 points 1 month 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.

  • permalink
  • fedilink
  • source
  • parent