Traits as types of types

From TWiR quote of the week

Generic types describe ranges of types, just like types describe ranges of values, and traits are to generic types what properties are to structs. So a new trait actually defines a new type of types, and can be combined with other traits to form a hierarchy of traits.

Wow, what does all that mean?

I am not exactly sure how accurate that is. But I am thinking about how to design a "meta type system", i.e. a type system for types. With generics, we are not dealing with single instances of types anymore, but sets of types. I am sure there is a lot of mathematical theory already behind this, which I haven't really studied much, so I am not willing to claim that I know exactly what I am talking about, but I got inspired to this view on types by the book "Modern C++ Design: Generic Programming and Design Patterns applied" by Alexandrescu, where "template templates" are used to program how classes get defined. Basically a template is an "uninstantiated" class definition, with compile time parameters such as class names and other templates:

template<typename A, typename B, template <typename, typename> Strategy>
struct Host {
    Host(A a, B b, Strategy<A, B> strategy) {}
    ...
}
template<typename X, typename Y>
struct StrategyA {
    ...
}
template<typename X, typename Y>
struct StrategyB {
    ...
}
...
Host<int, std::string, StrategyA> host_a(5, "Hello", StrategyA<int, std::string>());

So here we can pass a generic type definition (a template) to another template, and internally the arguments are substituted and a class instantiation will be generated, depending on the type arguments you passed to Host (I hope I still got the syntax right).

I am not 100% sure but I think something like this should also be possible in Rust.

What I have now come to believe is that type definitions themselves can be used as values at compile time, and it would be helpful to have a type system for types. Because since we have generic types, types do not only have one instance anymore, but multiple. They become sets of possible types, in fact the set of all types that are constructed when the generic type parameter is substituted with a valid type. So a generic type might actually be some kind of function for types? So concrete types like f32, u8, Foo are like concrete values and generic types transform types to other types? It seems to be that way.

So I am wondering what kind of "algebraic language" would be helpful for writing and understanding meta programs? But I have not yet shed a lot of light onto this concept.

I'm sure there is some deep mathematical reasoning going on with the idea of 'types'. But my simple mind is floored already by that initial statement.

I may have a 'type' that represents fruits. I may have another 'type' the represents aircraft.

What on Earth would it mean to have a 'generic type' that represents a range of types between my fruit type and my aircraft type?

How can one have a range of things that have no ordering relationship.

Or is this a different kind of type than the type of idea about types I'm used to?

Another way to think about generic types are type functions,

struct List<T> { ... }
// is the same as something like this
fn list(T: type) -> type { ... }

In fact this is how Zig handles generics!

7 Likes

Integer types can be ordered by their bit size.

They can?

In the Ada language for example you can define integer like types that are specified by their range of allowed values. Which need not be any relation to binary storage sizes.

A 'Height' could be 0 to 10000

A 'Temperature' could be -50 t +50.

These types are not things you can put in order.

I guess I mean, yes, they can. If you are talking about typical physical storage types. But what type of types are we talking about?

Ah yes, when Andrew Kelley describes how he got to generics in Zig it all made sense https://www.youtube.com/watch?v=Gv2I7qTux7g

In Rust, anything that implements std::cmp::Ordering has a defined total order, regardless of storage type.

I guess you're entering the realm of types of types of types. Go no further.

But anyway, even values are not necessarily orderable. Is i greater than 1?

I think L0uisc didn't literally mean "ranges" of types with defined orderings anyway, but rather sets.

I don't understand how 'equal' can define an order. Never mind storage type. How do I then know what is 'bigger' or 'smaller' such that I can put them in order?

You're right, it needs std::cmp::Ordering, not Eq. My mistake.

... and it has to satisfy the reflexive, associative, and transitive properties to define a total order. Ordering by itself is not enough.

Yes indeed, that was my point.

'i' lives in a different world than '1'.

Of course we can represent multiples of 'i' and '1' in 8 bits or 16 or 32 or whatever.

But they are not of the same type just because they take the same storage space.

They’re both complex numbers so they’re of the same type.

Hmm... In my maths class they were not. I was told:

'1' was a Real number.
'i' was am 'Imaginary' number.
'1 + i' Was a 'Complex' number.

You can't do that '+' there because they are different types. Like you can't add Mass and Velocity.

All real and imaginary numbers are also complex numbers, in the same way that all integers are also real numbers. So yes, 1 is real and i is imaginary, but you can add them because they are both complex.

That is not what I was led to believe in school. Which went more like this:

A Complex number is a composite thing. It has a Real Part and an Imaginary part.

You can add Complex two numbers by adding the Real part of each one together and, like wise for the Imaginary part. The result being a Complex number, a composite of Real and Imaginary parts.

What you cannot do is that last step of adding the Real part to the Imaginary part. Hence we get the Complex aggregate.

This is reflected in the fact that a complex number in C, for example, occupy twice the storage space of either part.

I don't see that as the same at all.

Integers and Reals all fall on the same one dimensional number line. Complex numbers exist in a space mostly not on that number line.

Granted the complex numbers (1 + 0i) and (0 + 1i) can be added together yielding the complex result (1 + 1i).

That is as far as it goes, you can't add that 1 to that 1i. Because Real and Imaginary are different types.

Of course my last maths class was decades ago and I was never a wiz at maths, so it's probably worth checking everything I say here.

But you can do (1 as Complex) + (1i as Complex). Mathematicians simply agreed to make this conversion almost always implicit where necessary.

Exactly.

With the result (1 + i). Which is a close as they get to adding a Real to an Imaginary. It is instead, Complex.

That's an oddly... computer-sciencey way of thinking about complex numbers. The average mathematician doesn't care about representation. They wouldn't think twice before saying that 2 and 2 + 0i are identical, and they would say that real numbers are a subset of the complex numbers. (i.e. if x is a real number, then it is also a complex number)

To call them different would be like saying (1 + 0 sqrt(5)) and 1 are not the same number, because you can't simplify 1 + sqrt(5). (In fact, it is almost exactly like that, because i = sqrt(-1)!)

Arguing by the difference in representation also leads to trouble, because there's other ways to write complex numbers. In physics we often deal with polar notation A exp(i phi), where A and phi are both real. To say that this should really be (A + 0i) exp(0 + i phi) would kind of be missing the point, because there's no utility in having those zeros ever be nonzero.

6 Likes

When A and B are two structures and there is a monomorphism φ: A→B, one can regard φ as an embedding of A into B. This generalizes the notion of substructure and subset. And when φ is canonical, one can define "A⊆B" as φ(A)⊆B.