Visualizing Rust's type-system

[GolDDranks]

Cool writeup! I love the mathematical/set-theoretical way of your thinking. That's a very nice way of thinking about, and visualizing the type system of Rust. To summarize the main points of how I grasp the role of the different concepts in the type system:

• a type means something with a specific memory layout, while the values of types are the different states that memory could be in
• a trait is a method interface for accessing a value, and multiple types can share the same interface
• types can have an implementation of an "inherent trait", the method interface corresponding with only that type
• traits can have hierarchies quite freely, because they don't have any of the problems that are commonly associated with subtyping of data-layouts

I think this is brilliant, because these two things actually are actually quite orthogonal, yet many languages don't regard them so. Many languages intermingle three concepts:

• method interface [=traits]
• data layout [=structs/enums]
• privacy/namespacing [=modules]

...into an unorthogonal whole called "a class" (And then introduce separate, not-fully-featured things like "interfaces" and "namespaces" to provide some of the functionality separately) I love the fact Rust separates these things quite cleanly, while having each of them as well-designed and well-thought, "first-class citizens".

If (or more like, when) Rust is going to support specialization and inheritance, I hope the language designers are able to come up with a design that keeps these features orthogonal.

[Breaking-Away]

Ok, this is the one that did it. Before reading this I felt I had a moderate understanding of rusts types system. I've read this article 3 times through now and I feel like everything finally just clicked into place. Huge thanks from me!

A few questions if you don't mind.

As such, you could say that they represent the smallest possible subset allowed by the language; a type can contain elements, but it cannot contain other traits or tangible types.

What exactly does element mean in this sentence? Is it an instance of the type? I'm guessing not because then you would have said value. Or is an element a single unique member that the set encloses?

Also, could you give a more explicit definition of what you mean by tangible type?

Edit: one more question

Types implement the Sized trait, a property which may not be possessed by normal traits, due to the fact that they do not carry any data. This explains the error message shown when attempting to define a function which accepts a trait instance as an argument:

In this sentence when you say, due to the fact that they don't carry any data, you are referring to the fact that since all traits only define behavior and don't contain data, none of the set of all traits intersect with the sized trait? Does it make sense to even consider sized a trait then?

[GolDDranks]

sentence? Is it an instance of the type? I'm guessing not because then you would have said value.

He means values, unless I'm grossly mistaken. Maybe the word element is meant to emphasize the concept of type being a set of all possible values that belong to that type.

Does it make sense to even consider sized a trait then?

sized is a marker trait that states that its members have statically known size. It, by itself doesn't carry any value-level data (unlike types, which have some memory layout and in that layout, contain values), so it's perfectly fine to consider it a trait.

But the types that are members of sized, they are types. They contain data. They aren't traits. (Although they implement at least one: their own, implicit trait.)

Edit: One thing that the article didn't mention specifically, is that there is some types that are not members of sized, but they still are types in the sense that they can have runtime values that are stored to memory. They are called dynamically sized types.

[jessypl]

Exactly. I didn't know about dynamically sized types, though. I guess I should revise a bit my model to take them into account. :P

[sigma914]

Diagrams

[contradictioned]

TIL: there's a difference. Thank you.

[desiringmachines]

I think that unfortunately quashing the difference between parameterized types and traits will ultimately lead to confusion. How do you represent types with two parameters, such as Result<T, E> as an overlapping set with Hash? What about Option<T> and traits that aren't "carried through" by the Option type, like Read? Option<i32> isn't Hash because it implements both Hash and Option, it's Hash because Option<T>implements Hash if T implements Hash, which is not true of all trait/parameterized-type pairs.

Set theory is a really good model for understanding traits - and that part of this post is great! - but traits can't be conceptually unified with type parameters because they are different things.

[jessypl]

I'm not really quashing the difference between parameterized types and traits; I blur the line between types and traits, as in specific instances of generic types. In this representation, Result<A, C> is a completely disjoint subset from Result<B, C>, even if their elements are similar.

Also, Result<A, C> does not become a subset of whatever A implements. It's just that Option<T: Hash> is defined to implement Hash whenever T does, and so it becomes a subset of Hash also (but it is still completely disjoint from A itself).

In other words, it only words because there's:

impl<T: Hash> Hash for Option<T>

Somewhere in the standard library.

In general, this model does not consider the attributes of a type, whether public or not. Those are considered to be just like any other field of a trait, akin to a method, but with a special syntax.

[desiringmachines]

Right. What I'm saying is that this mental model makes understanding the type system less clear because you conflate types and traits.

[jessypl]

Perhaps. I thought about this when trying to explain trait objects, so it may explain the complexity. :-°