The natural numbers encoded as types

You won't be able to find a generalized solution to this problem because you can't do normalization at the type level. That means you're stuck normalizing at the value level (or cheating and hard-coding this stuff in which is... ew). If you're interested in a solution, I did this a while back. The relevant part is here:

struct Plus<N : ℕ , M : ℕ> : ℕ {
    static func construct() -> Plus<N, M> {
        return Plus()
    }
    static func value() -> Int {
        return N.value() + M.value()
    }
}

Thanks,

So I guess it's impossible then. My non-existing type theoretic insights won't let me see exactly why, but I will take your word for it, feel a little disappointed and move on.

(Normalizing at the value level is not an option in my actual use case. Hard-coding will of course work ... but only in a tedious practical sense : ).)

OK, I'll bite. What on earth do you mean by "natural numbers"? Yes, I know what natural numbers are, but I'm not sure what you're trying to do here.

It's clearly impossible to represent natural numbers in Swift because:

a. Numbers are abstract entities, Swift values are concrete entities.

b. The set of natual numbers in infinite, the set of Swift values is finite.

So you're doubly out of luck before you start splitting hairs. I'm also unsure what kind of "normalization" you're talking about. There's no such thing (AFAICT) as an unnormalized natural number.

What you actually have in Swift is a mechanism for representing numerals, not numbers. No wonder things go pear-shaped if you start from numerals.

So what is you "actual use case"?

I recommend you take a stroll through the Peano numbers sometime. It's not "numbers" or "numerals" we're after, it's analogs of the inductive structure of the same. That it desugars to a value in Swift is an implementation detail.

It's clearly possible to encode a representation of each* natural number as a type in Swift's type system. The evidence is plain to see in the code of my original post. Read about Peano arithmetic and you'll see how it works.

(* Ok, not each and every one of the infinitely many, but also not hard coded like eg

struct Zero {}
struct One {}
...

but rather by defining them recursively, with relations between them, as the code above does.)

So why would one want a type for each* natural number?

I wanted it because I was trying to make a generic static array type implemented by using recursive structs at a lower level, but at a higher level parameterized by two type parameters, one for its Element type, and one for its Length type, something like this:

protocol StaticArrayType {
  typealias Element
  typealias Length: Nat
  subscript (index: Int) -> Element
}
struct StaticArray<Element, Length: Nat> : StaticArrayType {
  ...
}

I'm leaving out a lot of "details" here, like the recursive struct type(s) that makes for their "static storage", etc. But you can see something like that in this thread.

The reason for why I wanted to make it parameterized by Element and Length was to be able to write eg map and zip for them (funcs with parameters and/or return values that are StaticArrayTypes with eg different Element types but the same Length type).

When the length / count is represented "only" as a value (rather than a type) the compiler does not know and/or check that eg two lengths are the same.

Also, the storage of these StaticArrayTypes would be right there in the memory layout of their (recursively defined) struct, and not dynamically allocated and referenced to by some reference type (the std lib Array struct has a reference type that is responsible for the actual storage). What I mean can be shown like this:

sizeof(StaticArray<UInt8, Four>) == 4
sizeof(StaticArray<Double, 3> == 24 ((sizeof(Double) == 8) * 3)
sizeof([Double](count: 3, repeatedValue: 1.0))

Note that you cannot tell the compiler / type system anything about the number of elements of a std lib Array. The sizeof(Array<Something>) will always be 8, which is the size of the reference to its dynamically allocated storage (which I guess can be optimized to not be dynamic if the array has a small knowable size etc, but anyway).

And to answer your a and b:

a. Numbers are abstract entities, Swift values are concrete entities.

Yes, but types are somewhat more abstract entities. : )

b. The set of natual numbers in infinite, the set of Swift values is finite.

Again, I'm not talking about values, I'm talking about types. Here is the type representing 42 using the code from the original post:

typealias TypeRepresenting42 = Zero.Succ.Succ.Succ.Succ.Succ.Succ.Succ.Succ.Succ.Succ.Succ.Succ.Succ.Succ.Succ.Succ.Succ.Succ.Succ.Succ.Succ.Succ.Succ.Succ.Succ.Succ.Succ.Succ.Succ.Succ.Succ.Succ.Succ.Succ.Succ.Succ.Succ.Succ.Succ.Succ.Succ.Succ
print(TypeRepresenting42.self) // Prints the type signature.
print(TypeRepresenting42.intValue) // Prints 42 using the intValue static property of the type, can be used to return the count of a StaticArray type for example.

Yes, I understand the axiomatic basis of the natural numbers. I misread Jens's original post, so you can ignore what I said, but formulating a better response isn't easy (so I didn't).

— I think you're correct that the Swift type system can't do on its own what was requested (deriving operations like addition).

— I think that, aside from Swift's capabilities, the Peano postulates are the wrong place to start, because their definition of addition is recursive in terms of the successor function, and is therefore not computationally feasible. Neither we nor our computers add that way, because it takes too long to get to big numbers.

— I think that it's more promising to try something in terms of the logarithmic representation of numbers (that is to say, in terms of digits or bits), as we do in real life. In terms of Jens's approach, this would mean using types with multiple generic parameters, each parameter representing one bit of the represented number. Any solution would involve a cooperative group of static functions that served as an "adder" unit, producing new types as results. I played around with this in a playground for a while, but without really getting anywhere. I'm not sure Swift can solve this one either.

— I think that the idea of deriving fixed-length "inline" (i.e. stack-based) memory allocations is interesting, but I can't see the point. Favoring stack-based allocation seems to depend on a processing/memory overhead cost metric that belongs to 1960s-era computing, and is irrelevant to current hardware.

— I think Jens's idea of enforcing array length compatibility requirements at compile time is a strange enterprise in Swift, since Swift explicitly dropped fixed-length arrays when it left its C-based ancestry behind.

Just thought about a similar problem, and even of writing a preprocessor... but for unknown reasons, I can declare

struct Vector

but no

Matrix⫷4,4⫸

In fact, I didn't find a single mathematical symbol that was allowed (no braces or signs, just emogys...), so it's hard to generate good names for type variants.

I think actually we don't want the numbers encoded as types, but features from a template system like C++, where you can use any static datatype as parameter.

The difference of the C++ approach is that templates can't be compiled to libs, which is possible with generics:

Generics are just metadata for the compiler, templates create custom code.

Imho it would be easy to incorporate possibilities of templates without changing compilation:

Right now, it is no problem to declare a 4x4 matrix or vector of three elements; there's just no elegant way to make that construct a special type.

All that would be needed is something like "compile-time currying", where declaring a type like Vector<3> creates an implicit parameter ("size", "dimensions"...) that would be used like a constant property of the vector.

I don't know if there still are some misunderstandings here.

I simply want to do be able to do more at compile time/statically and less at runtime/dynamically, and I want flexible/powerful ways of declaring and working with "zero cost abstractions" like eg a type

Vector<Four, Float>

which will end up having the exact same (runtime) processing/memory overhead as this

struct Vector4Float { let x : Float, y: Float, z: Float, w: Float }

which is the same as this:

typealias Vector4Float = (x: Float, y: Float, z: Float, w: Float)

which is the same as this:

typealias Vector4Float = (Float ,(Float, (Float, (Float))))

only with a lot more (compile time) flexibility/power. I want the compiler to be able to know/check stuff like "Is this something which has as many elements as this?" and "I know this and this must result in something with this many elements of this type". Resulting in more optimizable, cache-friendly code and data with less derefencing, less dynamic dispatch, less jumping around to different places in memory, etc.

Using simd, the Accelerate Framework and Metal, together with this kind of abstractions (types and protocols) is not something I would call irrelevant to current hardware.

I do think your idea of representing natural number types and operations on them using one type parameter per bit sounds interesting though.

Perhaps it's also worth pointing out that the hackyness of these things is not something I value in its own, it's just something that is necessary because there's no other way of doing it in current Swift, afaics.

Yes, if we could use integers as type parameters and there were some kind of compile time evaluated functions whose return values could be used as types and type parameters, then none of this would be a problem. But I assume there are good reasons for why such things are not in the language.

>> I want the compiler to be able to know/check stuff like "Is this something which has as many elements as this?"

Yes, after several iterations of thinking about this, I figured out that this is the essence of your interest. (The memory allocation thing still seems pointless to me. Space on the stack isn't allocated at compile time — the stack only exists at run time — so this really is about performance metrics. Incrementing a stack pointer is cheaper than allocating a heap block in current hardware — provided you don't also have to reallocate the stack larger, which is a danger if you start throwing arrays onto the stack — but obsessing about it in the abstract does strike me as quaintly 1960s-ish.)

On the one hand, solving the "Is this something which has as many elements as this?" question is an extremely interesting Swift question, and that was going to be my first response. But then it occurred to me that the capability exists in C (in a limited way, sure, because the array type degrades into a mere pointer type in most situations), and that it's not in Swift because it was intentionally left out. You're trying to put back in what was thrown out. If your goal is just an intellectual exercise, then I'm interested to see what you come up with. If you're trying to fill in a hole in Swift, then I think you have a deeper philosophical debate to resolve before you dive into implementation details.

Regarding 1960-ish or not: When working with lots of vectors (lets ignore simd etc for now) I would prefer having some vector type like this:

struct Vector4<Element> { let x : Element, y: Element, z: Element, w: Element }

over something like this:

struct Vector4<Element> { let elements: [Element] }

for obvious performance related reasons (it's easy to microbenchmark these things and arrive at 2015-ish conclusions). Other reasons include being able to use a block of those with Metal, or as eg simd float4 etc. So using Arrays to represent individual vector types is not an option. (It contains a reference to its storage rather than "being" its storage, so eg sizeof(SomeArray) will always just be 8 (a reference to its ManagedBuffer instance) no matter how many elements.)

I'm not particularly interested in taking this part of the discussion any further. I have enough concrete applications and measurements of these things to be sure that I'm not obsessiong over something irrelevant.

Anyway, a higher abstraction of such a type could, as already mentioned, look something like this:

struct Vector<Element, Count: Nat> { ... as previously outlined, using recursive struct ... }

Regarding implementing bit arithmetics at the type level: Here's a (working) compile time Nand "function":

protocol Bit {}
protocol IsSet {}
protocol IsClr {}

struct Set : Bit, IsSet {}
struct Clr : Bit, IsClr {}

protocol  NandOp { typealias Result }
extension NandOp { typealias Result = Set }

struct Nand<B0: Bit, B1: Bit> : NandOp {}
extension Nand where B0: IsSet, B1: IsSet {
    typealias Result = Clr
}

print(Nand<Clr, Clr>.Result.self == Set.self) // true
print(Nand<Clr, Set>.Result.self == Set.self) // true
print(Nand<Set, Clr>.Result.self == Set.self) // true
print(Nand<Set, Set>.Result.self == Clr.self) // true

EDIT: Turns out that it's not possible to extend it though : ( since Result is actually two different things:

struct Not<B0: Bit> {
    typealias Result = Nand<B0, B0>.Result // Error: Ambigous type name 'Result' in Nand<B0, B0>
}

The concept is much simpler - there is no need for a special type "3" (or any other struct) or functions that are evaluated at compile time:

Just have a look at C++ templates, which are not restricted to types, but can contain plain values as well.

Of course, the C++ templates are infamous for their complexity (you can do any kinds of calculations with them), but for many problems, it would be fine to have an restricted subset.

Maybe an example helps:

class FloatVector<SIZE: Int> {
     var elements: [Float]
     init() {
          elements = Array<Float>(count: SIZE, repeatedValue: 0.0)
     }
     subscript(index: Int) -> Float {
          get {
               return elements[index]
          }
          set {
               elements[index] = newValue
          }
     }
}

(mh, there's even a matrix example in the Swift docs... but they aren't doing any operations on it, so there's no need for type safety ;-)

I'm not sure what you mean. I know about (and have used/written a lot of) C++ templates, and they are something entirely different than Swifts generics (parametric polymorphism?).

All I was saying is that I guess there are good reasons for why Swift has not included that kind of template system, constexprs, etc.

Also, the StaticArray<Count, Element> types that I want to have must be value types (structs) with the obvious storage&layout, ie sizeof(StaticArray<4, Float>) == 4*4 = 16, so I'm not interested in using anything that builds on Array, since Array is a struct whose only stored prop is a reference to its storage, so sizeof(Array<AnythingAtAll>) = 8 always, no matter how many elements and what Element type (its storage is just the reference which is 8 bytes), and I would certainly not want a class for the StaticArray/Vector type itself. The reason for this is simply to be able to use them as elements in blocks of memory, where they can be eg pixels, positions, forces, shared vertex or texture data with Metal etc. I could of course use the simd types but there are situations where you'd like to have more flexibility (without sacrifying type safety and compile time knowledge).

But these things will probably have to wait until Swift supports higher kinded types or hygienic macros or something.

I think real value types wouldn't be possible with the presented approach, because afaics Swift doesn't allow to override alloc... let's hope some day in far future Apple is bold enought to build a complete new OS with Swift 😀 - guess in that case, they would add some low-level extensions.

I really don't understand what you mean. What I'm looking for has nothing to do with alloc, in the same sense that this has nothing to do with alloc:

protocol StaticArrayType { / ... */ }
// ...
struct Three {}
struct Four {}
// ...
struct StaticArray3<T> : StaticArrayType { typealias Count = Three; typealias Element = T; let value: (T, T, T) }
struct StaticArray4<T> : StaticArrayType { typealias Count = Four;  typealias Element = T; let value: (T, T, T, T) }
// ...
print(sizeof(StaticArray3<Float>))  // Prints 16 == 4 * 4 == 4 * sizeof(Float)
print(sizeof(StaticArray4<Double>)) // Prints 24 == 3 * 8 == 3 * sizeof(Double)
print(StaticArray4<UInt8>.Count.self == StaticArray4<Float>.Count.self) // Prints true since both types has count Four.

This is runnable code. But it's just an overly simplified example of the concept. And instead of doing somethng like this, we can use recursively defined structs (as shown for Nat in the OP) to make a more general implementation of both the Count/Nat types and the Static Array types, it's possible to add subscripts etc without having to hard code everything. But in the end it doesn't seem possible to write it in a way that will allow us to declare these types like this:

StaticArray<Four, Float>

rather than eg this:

StaticArray<Float>.CountPlus3

which makes it hard to implement for example zip and map (functions with a return type that is a StaticArray type whose Count type and Element type depends on the input types in various ways).

And btw, current Swift can already do all low level stuff necessary for building eg an OS, (all pointer arithmetics and memory managemnt can be done through UnsafeMutablePointer et al (and you've got all the usual low level C stuff from eg import Darwin)).