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.
We present a calculational approach to the design of type checkers, showing how they can be derived from behavioural specifications using equational reasoning.
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.
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.
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.
Recursive types and bounded quantification are two prominent features in many modern programming languages, such as Java, C#, Scala, or TypeScript.
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.
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.
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.
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.