I study type systems and programming language theory at university, and I encourage friends studying CS to at least have some understanding of type theory, such as well-known type systems (simply-typed, System F) and properties like soundness or uniqueness of typing. Why? Because as programmers we argue to death comparing the expressiveness and properties of type systems of our favorite programming languages, or we're picking up a language with features like traits or type inference. Type theory really lets you learn the heart of such features in a small, idealistic setting and specifies things rigorously and uniformly, (since languages tend to come up with their own names and examples for things like ad-hoc polymorphism, AKA typeclasses/traits/protocols/concepts), and they appear no matter the paradigm.
What is a good an introductory text (or other resource) for learning? What's the relationship between programming language theory and type theory? Is type theory a special topic, or would it be considered a core topic in programming language theory (e.g., like integration in calculus)?
I found the first 6 chapters of "Type Theory and Formal Proof" to be amazing for covering the beginning math behind Type Theory. The authors (Nederpelt and Geuvers) don't gloss over assumptions and they build things up step by step. I didn't study this in university but have picked up many books along the way. I'm usually quite lost within the first 10 or 20 pages until picking up Type Theory and Formal Proof. This one took me somewhere between 100 to 200 pages before getting lost. They cover the entire lambda cube.
But then I was able to re-start Thompson's "Type Theory and Functional Programming" and it was clear that I started to understand a lot of it.
If you enjoy the nostalgia of older books like me, then pick up an original copy of "Intuitionistic Type Theory" edited by Per Martin-Löf.
I love “Types and Programming Languages” by Benjamin Pierce and always recommend it for people who want to dip their toes into formal type theory. To me it’s basically the K&R for type theory.
As others have said, I also recommend Types and Programming Languages.
> What's the relationship between programming language theory and type theory?
I'd say programming language theory is more broad than type theory, for instance topics such as compilation techniques and runtime systems are more distant from type theory (though you might prove some type-theoretic thing like type preservation).
There's also a range of type theory books because it's a field that spans pure logic to programming languages, so you can find books like Type Theory and Functional Programming by Thompson that elaborate things like dependent types early on.
Many introductory texts, such as Types and Programming Languages explain the notation thoroughly and start really simple, even starting from the inference rule notation, then talking about reduction of untyped arithmetic expressions, building up to the standard notation type theory.
I think it's easier to do if you work up to it gradually. I read Logic by Wilfrid Hodges a few years back on a whim from some recommendation on HN. I didn't think much of the book at the time, though I recently picked up Benjamin Pierce's Types and Programming Languages. Having seen notation like that before made digesting the book much easier (along with starting with other introductory texts like Friedman and Wand's Essentials of Programming Languages).
Looking at java, rust or assembly i find this argument hard to swallow ;) It's really worth it to learn some sequent calculus basics to be able to read typing rules. Its mostly the same thing as a grammar, or a weird inductive type ("enum").
The notation really isn't as bad as it originally looks, trust me. I was in the same boat recently, but after cracking open TAPL, on page 26 you basically get all the notation you need for the rest of the book.
Inference rules just transform the traditional format of
(A && B) -> C
into
A B
---
C
This format allows you to stack rules on top of each other when writing out the derivation of some term, without running out of page space.
It shows that is important to take soundness of type-systems serious. I like what they did with Scala: they boiled down the language into the fundamental parts and built a language from it that has a sound type-system (machine-checked). This has now finally become Scala 3.
Existential type syntax ("forSome") also got removed for the same reason. I still think it's better to build a sound typesystem than having a bad foundation with some extra features.
There is difference between bugs that make a type-system unsound and the actual fundamental design / specification that makes it unsound. The former is easily possible but also easy to fix. The latter is sometimes impossible to fix without breaking compatibility to a degree that makes it impossible to do so.
This is an excellent resource for learning about the finer points of type systems, precisely because it shows their potential breaking points an how things might go awry.
Constructing type systems that allow you to express the things that you need in your program while simultaneously constraining you to a safe way of doing that is one of those instances of theoretical research that have immense practical importance. It's good to see Rust slowly establishing itself in the industry, because there's hope that the ideas will gain popularity and better type systems will enter the mainstream in the coming decades.
The true liberation will be when your type system is just a set of libraries written in the same language that the type system applies to.
Which also means you'd be able to add new semantical type behavior specific to a project, not just specific to a language.
What we're doing right now it's highly redundant, it's basically two languages in one. One describes the static constraints, and another the runtime ones. There's no need for that.
I feel like we don't really need highly-evolved type systems for practical problem solving. On the contrary, I have found that the plethora of available ways in which to model a problem domain can cause more harm than if a more constrained set of tools were made available.
What problem domain is so complex that it cannot at least be modeled in SQL (or Excel)? What language does not provide sufficient abstractions for tables, columns, relations & basic data types? Why would you want to take a clean domain model that the business agrees upon and then start perverting it with things like polymorphism? Performance is often something thrown around as an excuse to de-normalize schemas, but typically when I ask someone to actually measure it we find that LINQ/SQL/etc is more than fast enough to get the job done for all practical intents & purposes.
Types like this mostly aren't about data modeling more complicated than basic sum and product types (SQL only poorly models discriminated sum types, eg ML's data or Rust's enum, which is one of my biggest gripes about it). They're about correctness, making invalid states inexpressible, and the like. Type sums and products (e.g. tuples/structs) really are a nice minimal but expressive system.
That said:
> What language does not provide sufficient abstractions for tables, columns, relations & basic data types?
A key part of the SQL data model is the primary key. I'd really love to see a programming language make PKs or something like them a first-class construct. So if we're looking for something neat to add to PLs that would actually help with business modeling, maybe we could start there?
> A key part of the SQL data model is the primary key. I'd really love to see a programming language make PKs or something like them a first-class construct.
This certainly seems like an excellent place to start. Every single one of my domain types starts like:
public class MySpecialType
{
public Guid Id { get; set; } = Guid.NewGuid();
//...
}
Having some notion of a first class identity that I could leverage without having to explicitly add a public Id property would be worth looking at.
But, what about the relational aspect? Identity is trivial to solve IMO. How do we canonicalize this idea of relations between types? The way I do this today is:
public class MyRelatedType
{
public Guid Id { get; set; } = Guid.NewGuid();
public Guid? MySpecialTypeId { get; set; }
//...
}
And then I just tie it all together with LINQ statements as appropriate.
Is there a better way to express this idea with some shiny new language constructs? I feel like I am running out of physical lines of code to golf with here.
The only thing I can think of that is more concise than my above code examples would be SQL.
I study type systems and programming language theory at university, and I encourage friends studying CS to at least have some understanding of type theory, such as well-known type systems (simply-typed, System F) and properties like soundness or uniqueness of typing. Why? Because as programmers we argue to death comparing the expressiveness and properties of type systems of our favorite programming languages, or we're picking up a language with features like traits or type inference. Type theory really lets you learn the heart of such features in a small, idealistic setting and specifies things rigorously and uniformly, (since languages tend to come up with their own names and examples for things like ad-hoc polymorphism, AKA typeclasses/traits/protocols/concepts), and they appear no matter the paradigm.
What is a good an introductory text (or other resource) for learning? What's the relationship between programming language theory and type theory? Is type theory a special topic, or would it be considered a core topic in programming language theory (e.g., like integration in calculus)?
I found the first 6 chapters of "Type Theory and Formal Proof" to be amazing for covering the beginning math behind Type Theory. The authors (Nederpelt and Geuvers) don't gloss over assumptions and they build things up step by step. I didn't study this in university but have picked up many books along the way. I'm usually quite lost within the first 10 or 20 pages until picking up Type Theory and Formal Proof. This one took me somewhere between 100 to 200 pages before getting lost. They cover the entire lambda cube.
But then I was able to re-start Thompson's "Type Theory and Functional Programming" and it was clear that I started to understand a lot of it.
If you enjoy the nostalgia of older books like me, then pick up an original copy of "Intuitionistic Type Theory" edited by Per Martin-Löf.
I love “Types and Programming Languages” by Benjamin Pierce and always recommend it for people who want to dip their toes into formal type theory. To me it’s basically the K&R for type theory.
As others have said, I also recommend Types and Programming Languages.
> What's the relationship between programming language theory and type theory?
I'd say programming language theory is more broad than type theory, for instance topics such as compilation techniques and runtime systems are more distant from type theory (though you might prove some type-theoretic thing like type preservation).
There's also a range of type theory books because it's a field that spans pure logic to programming languages, so you can find books like Type Theory and Functional Programming by Thompson that elaborate things like dependent types early on.
2 replies →
> What is a good an introductory text (or other resource) for learning?
The usual recommendation seems to be "Types and Programming Languages" by Benjamin C. Pierce.
The notation is an insurmountable barrier to many.
Many introductory texts, such as Types and Programming Languages explain the notation thoroughly and start really simple, even starting from the inference rule notation, then talking about reduction of untyped arithmetic expressions, building up to the standard notation type theory.
It's interesting how calling it insurmountable both panders to and insults the people you're talking about.
Maybe a better way to describe the notation is "off-putting"?
27 replies →
I think it's easier to do if you work up to it gradually. I read Logic by Wilfrid Hodges a few years back on a whim from some recommendation on HN. I didn't think much of the book at the time, though I recently picked up Benjamin Pierce's Types and Programming Languages. Having seen notation like that before made digesting the book much easier (along with starting with other introductory texts like Friedman and Wand's Essentials of Programming Languages).
1 reply →
Looking at java, rust or assembly i find this argument hard to swallow ;) It's really worth it to learn some sequent calculus basics to be able to read typing rules. Its mostly the same thing as a grammar, or a weird inductive type ("enum").
2 replies →
The notation really isn't as bad as it originally looks, trust me. I was in the same boat recently, but after cracking open TAPL, on page 26 you basically get all the notation you need for the rest of the book.
Inference rules just transform the traditional format of
into
This format allows you to stack rules on top of each other when writing out the derivation of some term, without running out of page space.
1 reply →
ah notation is such a subtle and often sad topic
when you click you never give a damn about notation but before you do it's such a drag
it's like monads
Great list!
It shows that is important to take soundness of type-systems serious. I like what they did with Scala: they boiled down the language into the fundamental parts and built a language from it that has a sound type-system (machine-checked). This has now finally become Scala 3.
Here are some more details: https://www.scala-lang.org/blog/2016/02/03/essence-of-scala....
Cries in removal of abstract types (e.g. `val x: A#T = ...`).
While Scala 3 filled a soundness hole, it opened a practical crater (and no, path dependent types are not a viable substitute).
Too bad, many nice improvements overall.
Existential type syntax ("forSome") also got removed for the same reason. I still think it's better to build a sound typesystem than having a bad foundation with some extra features.
> It shows that is important to take soundness of type-systems serious.
Does it show that? I see it more like a set of examples demonstrating there's no such thing as "a sound type system".
There is difference between bugs that make a type-system unsound and the actual fundamental design / specification that makes it unsound. The former is easily possible but also easy to fix. The latter is sometimes impossible to fix without breaking compatibility to a degree that makes it impossible to do so.
For the curious: the title seems to echo the excellent "Counterexamples in Topology"[1].
[1]: <https://en.wikipedia.org/wiki/Counterexamples_in_Topology>
Yeah it’s a bit of a theme. See also: https://files.eric.ed.gov/fulltext/ED536733.pdf
That is a fun book :-)
This is an excellent resource for learning about the finer points of type systems, precisely because it shows their potential breaking points an how things might go awry.
Constructing type systems that allow you to express the things that you need in your program while simultaneously constraining you to a safe way of doing that is one of those instances of theoretical research that have immense practical importance. It's good to see Rust slowly establishing itself in the industry, because there's hope that the ideas will gain popularity and better type systems will enter the mainstream in the coming decades.
The true liberation will be when your type system is just a set of libraries written in the same language that the type system applies to.
Which also means you'd be able to add new semantical type behavior specific to a project, not just specific to a language.
What we're doing right now it's highly redundant, it's basically two languages in one. One describes the static constraints, and another the runtime ones. There's no need for that.
Is the syntax highlighting broken for anyone else?
For me it is pure black on both Firefox and Chrome
Is it this issue for Firefox? https://bugzilla.mozilla.org/show_bug.cgi?id=1520157
See also https://github.com/adobe-fonts/source-code-pro/issues/250
I feel like we don't really need highly-evolved type systems for practical problem solving. On the contrary, I have found that the plethora of available ways in which to model a problem domain can cause more harm than if a more constrained set of tools were made available.
What problem domain is so complex that it cannot at least be modeled in SQL (or Excel)? What language does not provide sufficient abstractions for tables, columns, relations & basic data types? Why would you want to take a clean domain model that the business agrees upon and then start perverting it with things like polymorphism? Performance is often something thrown around as an excuse to de-normalize schemas, but typically when I ask someone to actually measure it we find that LINQ/SQL/etc is more than fast enough to get the job done for all practical intents & purposes.
Types like this mostly aren't about data modeling more complicated than basic sum and product types (SQL only poorly models discriminated sum types, eg ML's data or Rust's enum, which is one of my biggest gripes about it). They're about correctness, making invalid states inexpressible, and the like. Type sums and products (e.g. tuples/structs) really are a nice minimal but expressive system.
That said:
> What language does not provide sufficient abstractions for tables, columns, relations & basic data types?
A key part of the SQL data model is the primary key. I'd really love to see a programming language make PKs or something like them a first-class construct. So if we're looking for something neat to add to PLs that would actually help with business modeling, maybe we could start there?
> A key part of the SQL data model is the primary key. I'd really love to see a programming language make PKs or something like them a first-class construct.
This certainly seems like an excellent place to start. Every single one of my domain types starts like:
Having some notion of a first class identity that I could leverage without having to explicitly add a public Id property would be worth looking at.
But, what about the relational aspect? Identity is trivial to solve IMO. How do we canonicalize this idea of relations between types? The way I do this today is:
And then I just tie it all together with LINQ statements as appropriate.
Is there a better way to express this idea with some shiny new language constructs? I feel like I am running out of physical lines of code to golf with here.
The only thing I can think of that is more concise than my above code examples would be SQL.