Hacker News with Generative AI: Type Theory

Sequent Calculus and Notation – Par Part 1 (ryanbrewer.dev)
This post is the first in a series on Logic. These ideas are very useful in understanding many important papers on programming language theory, especially papers on type theory and the lambda calculus. I will start with an explanation of sequents and Sequent Calculus as a system for doing logic, then I'll dive into linear logic in the next post. I'll finish the trilogy with a post on Par and computational interpretations of classical logic.
Good union types in Go would probably need types without a zero value (utoronto.ca)
One of the classical big reason to want union types in Go is so that one can implement the general pattern of an option type, in order to force people to deal explicitly with null values.
Sets, types and type checking (kaleidawave.github.io)
In the process of building a type-checker I have learnt a lot of the details about the theory of types and sets. With all this information I thought I would unpack all the details I have encountered along the way.
How the OCaml type checker works (2022) (okmij.org)
Data types as Lattices – Dana Scott [pdf] (github.com/CMU-HoTT)
Evolving languages faster with type tailoring (lambdaland.org)
A reckless introduction to Hindley-Milner type inference (2019) (reasonableapproximation.net)
Deriving Dependently-Typed OOP from First Principles (arxiv.org)