Hacker News with Generative AI: Type Theory

The Calculated Typer (bahr.io)
We present a calculational approach to the design of type checkers, showing how they can be derived from behavioural specifications using equational reasoning.

Type Theory, Programming Languages, Software Engineering, Formal Methods

75 points by matt_d 16 days ago | 5 comments

The State of Coherence in the Land of Type Classes (programming-journal.org)
Type classes are a popular tool for implementing generic algorithms and data structures without loss of efficiency, bridging the gap between parametric and ad-hoc polymorphism.

Programming Languages, Functional Programming, Type Theory

21 points by mpweiher 24 days ago | 2 comments

Recursive Subtyping for All (cambridge.org)
Recursive types and bounded quantification are two prominent features in many modern programming languages, such as Java, C#, Scala, or TypeScript.

Programming Languages, Software Development, Type Theory

4 points by matt_d 32 days ago | 0 comments

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.

Logic, Programming Languages, Type Theory, Lambda Calculus, Linear Logic

38 points by hoping1 71 days ago | 10 comments

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.

Go, Programming Languages, Data Structures, Type Theory, Null Values

89 points by ingve 121 days ago | 105 comments

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.

Programming, Type Theory, Sets

118 points by kaleidawave 154 days ago | 33 comments

How the OCaml type checker works (2022) (okmij.org)

Programming, Type Theory, OCaml, Compilers

219 points by mooreds 228 days ago | 42 comments

Data types as Lattices – Dana Scott [pdf] (github.com/CMU-HoTT)

Data types, Mathematics, Programming Languages, Type Theory

34 points by ozb 237 days ago | 5 comments

Evolving languages faster with type tailoring (lambdaland.org)

Programming, Language Design, Software Development, Type Theory

5 points by ashton314 250 days ago | 1 comments

A reckless introduction to Hindley-Milner type inference (2019) (reasonableapproximation.net)