9 ms·

Counterexamples in Type Systems

172 points by tempodox 5y ago

tempodox 5y ago
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.
yakubin 5y ago
For the curious: the title seems to echo the excellent "Counterexamples in Topology"[1]. [1]: <https://en.wikipedia.org/wiki/Counterexamples_in_Topology https://en.wikipedia.org/wiki/Counterexamples_in_Topology>
- deleted 5y ago
  [deleted]
- mcphage 5y ago
  That is a fun book :-)
- dan-robertson 5y ago
  Yeah it’s a bit of a theme. See also: https://files.eric.ed.gov/fulltext/ED536733.pdf https://files.eric.ed.gov/fulltext/ED536733.pdf
antihero 5y ago
Is the syntax highlighting broken for anyone else? For me it is pure black on both Firefox and Chrome
- giraffe333 5y ago
  Is it this issue for Firefox? https://bugzilla.mozilla.org/show_bug.cgi?id=1520157 https://bugzilla.mozilla.org/show_bug.cgi?id=1520157 See also https://github.com/adobe-fonts/source-code-pro/issues/250 https://github.com/adobe-fonts/source-code-pro/issues/250
siraben 5y ago
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.
- duped 5y ago
  The notation is an insurmountable barrier to many.
  - lapinot 5y ago
    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").
    - duped 5y ago
      It shouldn't be hard to swallow. Monospaced ascii text that is (usually) unambiguous with extensive documentation is night and day from formal notation. At least BNF grammars are legible
    - klibertp 5y ago
      Look at APL, K, and J. The notation based on keywords is not a problem; the problematic notations are the ones which abuse strange characters or ideograms, because they require you to re-learn the process of reading.
  - steego 5y ago
kubb 5y ago
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.
- slver 5y ago
  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.
valenterry 5y ago
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.html https://www.scala-lang.org/blog/2016/02/03/essence-of-scala....
- virtualwhys 5y ago
  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.
  - valenterry 5y ago
    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.
- slver 5y ago
  > 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".
  - valenterry 5y ago
    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.
bob1029 5y ago
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.
- andrewflnr 5y ago
  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?
  - bob1029 5y ago
    > 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.

172 points by tempodox 5y ago

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.

yakubin 5y ago

For the curious: the title seems to echo the excellent "Counterexamples in Topology"[1]. [1]: <https://en.wikipedia.org/wiki/Counterexamples_in_Topology https://en.wikipedia.org/wiki/Counterexamples_in_Topology>

deleted 5y ago
[deleted]
mcphage 5y ago
That is a fun book :-)
dan-robertson 5y ago
Yeah it’s a bit of a theme. See also: https://files.eric.ed.gov/fulltext/ED536733.pdf https://files.eric.ed.gov/fulltext/ED536733.pdf

antihero 5y ago

Is the syntax highlighting broken for anyone else? For me it is pure black on both Firefox and Chrome

giraffe333 5y ago
Is it this issue for Firefox? https://bugzilla.mozilla.org/show_bug.cgi?id=1520157 https://bugzilla.mozilla.org/show_bug.cgi?id=1520157 See also https://github.com/adobe-fonts/source-code-pro/issues/250 https://github.com/adobe-fonts/source-code-pro/issues/250

siraben 5y ago

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.

duped 5y ago
The notation is an insurmountable barrier to many.
- lapinot 5y ago
  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").
  - duped 5y ago
    It shouldn't be hard to swallow. Monospaced ascii text that is (usually) unambiguous with extensive documentation is night and day from formal notation. At least BNF grammars are legible
  - klibertp 5y ago
    Look at APL, K, and J. The notation based on keywords is not a problem; the problematic notations are the ones which abuse strange characters or ideograms, because they require you to re-learn the process of reading.
- steego 5y ago

kubb 5y ago

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.

slver 5y ago
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.

valenterry 5y ago

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.html https://www.scala-lang.org/blog/2016/02/03/essence-of-scala....

virtualwhys 5y ago
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.
- valenterry 5y ago
  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.
slver 5y ago
> 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".
- valenterry 5y ago
  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.

bob1029 5y ago

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.

andrewflnr 5y ago
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?
- bob1029 5y ago
  > 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.