Hacker News with Generative AI: Type Theory

Programming in Martin-Lof's Type Theory: An Introduction (1990) (chalmers.se)
This book was published by Oxford University Press in 1990. It is now out of print.

Programming Languages, Type Theory, Computer Science

59 points by todsacerdoti 6 days ago | 6 comments

Hasochism: The pleasure and pain of dependently typed Haskell programming [pdf] (2013) (strath.ac.uk)

Programming Languages, Haskell, Functional Programming, Type Theory

94 points by fanf2 46 days ago | 13 comments

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 67 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 75 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 83 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 121 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 171 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 205 days ago | 33 comments

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

Programming, Type Theory, OCaml, Compilers

219 points by mooreds 278 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 287 days ago | 5 comments

Evolving languages faster with type tailoring (lambdaland.org)

Programming, Language Design, Software Development, Type Theory

5 points by ashton314 301 days ago | 1 comments

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